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.