Larch

Larch is a multi-site project exploring methods, languages, and tools for the practical use of formal specifications. Much of the early work was done at MIT in the Systematic Program Development Group in the Laboratory for Computer Science and at Digital Equipment in the Systems Research Center in Palo Alto, California.

The Larch family of languages supports a two-tiered, definitional style of specification. Each specification has components written in two languages: one language that is designed for a specific programming language and another language that is independent of any programming language. The former kind are Larch interface languages, and the latter is the Larch Shared Language (LSL).

Interface languages are used to specify the interfaces between program components. Each specification provides the information needed to use an interface. A critical part of each interface is how components communicate across the interface. Communication mechanisms differ from programming language to programming language. For example, some languages have mechanisms for signalling exceptional conditions, other do not. More subtle differences arise from the various parameter passing and storage allocation mechanisms used by different languages.

It is easier to be precise about communication when the interface specification language reflects the programming language. Each interface language deals with what can be observed by client programs written in a particular programming language. Larch interface languages have been designed for a variety of programming languages, including Ada, C, C++, CLU, CORBA, ML, Modula-3, and Smalltalk. There are also "generic" Larch interface languages that can be specialized for particular programming languages or used to specify interfaces between programs in different languages.

Interface specifications rely on definitions from auxiliary specifications, written in LSL, to provide semantics for the primitive terms they use. Specifiers are not limited to a fixed set of notations, but can use LSL to define specialized vocabularies suitable for particular interface specifications or classes of specifications.