The papers in this volume were presented at the First International
Workshop on Larch, held at MIT Endicott House near Boston on 13-15 July
1992. Larch is a family of formal specification languages and tools, and
this workshop was a forum for those who have designed the Larch
languages, built tool support for them, particularly the Larch Prover,
and used them to specify and reason about software and hardware systems.
The Larch Project started in 1980, led by John Guttag at MIT and James
Horning, then at Xerox/Palo Alto Research Center and now at Digital
Equipment Corporation/Systems Research Center (DEC/SRC). Major
applications have included VLSI circuit synthesis, medical device
communications, compiler development and concurrent systems based on
Lamport's TLA, as well as several applications to classical theorem
proving and algebraic specification. Larch supports a two-tiered
approach to specifying software and hardware modules. One tier of a
specification is wrillen in the Larch Shared Language (LSL). An LSL
specification describes mathematical abstractions such as sets,
relations, and algebras; its semantics is defined in terms of
first-order theories. The second tier is written in a Larch interface
language, one designed for a specific programming language. An interface
specification describes the effects of individual modules, e.g. state
changes, resource allocation, and exceptions; its semantics is defined
in terms of first-order predicates over two states, where state is
defined in terms of the programming language's notion of state. Thus,
LSL is programming language independent; a Larch interface language is
programming language dependent.
