The Larch Family of
Specification Languages
John V. Guttag, Massachusetts Institute of Technology
James J. Horning, Digital Equipment Corporation
Jeannette M. Wing, Carnegie-Mellon University
Larch specifications are T he use of suitable formalisms in extensive checking of specifica-
two-tiered. Each one I the specification of computer tions as they are being con-programs and parts of computer pro- structed. An important aspect of
has a component grams offers significant advantages.' our approach is the use of a
written in an algebraic Although there is considerable theo- powerful theorem prover for
language and another retical interest in this area,2 practical semantic checking to supplement
tailored toa experience is rather limited. The Larch the syntactic checking commonlytailored to a Project, a research project intended to defined for specification lan-
programming language. have practical applications in the next guages.
few years, is developing tools and * Localizedprogramming language
techniques to aid in the productive dependencies. Each Larch inter-
application of formal specifications. A face language encapsulates the
major part of the project is a family of features needed to write concise
specification languages. Each specifi- and comprehensible specifications
cation has components written in two for a particular programming lan-
languages. The Larch interface lan- guage and incorporates Larch
guages are particular to specific pro- Shared Language specifications
gramming languages, while the Larch in a uniform way.
Shared Language is common to all The Larch interface languages spec-
languages. ify program modules, providing in-
formation needed to write programs
Some important aspects of the that use these modules (Figure 1)' A
Larch family of specification languages critical part of the interface is how the
are module communicates with its envi-
* Composability. The Larch lan- ronment, yet communication mecha-
guages are designed for the incre- nisms differ from programming lan-
mental construction of specifica- guage to programming language,
tions from other specifications. sometimes in subtle ways. We have
* Emphasis on presentation. The found it easier to be precise about
Larch languages are designed to communication when the specification
be readable. Among other things, language reflects the programming
Larch's composition mechanisms language. Such specifications are gen-
are defined as operations on spe- erally shorter than those written in a
cifications, rather than on theories "universal" interface language. They
or models.3 also seem clearer to programmers who
* Suitability for integrated inter- implement modules and to program-
active tools. The Larch languages mers who use them.
are designed to facilitate the inter- Each Larch interface language deals
active construction and incre- with what can be observed about the
mental checking of specifications. behavior of programs written in a
* Semantic checking. The Larch particular programming language. It
languages are designed to enable provides a way to write assertions
24 0740-7459/85/0900/0024$O1.OO ' 1985 IEEE IEEE SOFTWARE