Larch Shared Language (LSL) Checker

The Larch family of specification languages supports a two-tiered, definitional style of specification for program module interfaces. 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 called Larch interface languages, and the latter is the Larch Shared Language (LSL).

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.

The LSL Checker checks for syntax and type errors in LSL specifications. It can also be used to translate LSL specifications into two files of input suitable for use with LP, the Larch Prover. The first file contains an LP axiomatization for an LSL specification. The second contains LP proof obligations associated with logical claims made by specifiers about the logical properties of their specifications.

Instructions for getting and installing the LSL Checker are here.

Larch FTP directory.

Please send suggestions to