Larch Shared Language Checker and Handbook -- Distribution
The Larch Shared Language (LSL) is a language for specifying properties of
abstract data types in multisorted first-order logic. The LSL Checker is a
tool for checking LSL specifications for syntax and static semantic errors.
The LSL Handbook contains axiomatizations for a number of common datatypes.
To use the LSL Checker and Handbook, you need to retrieve and install the
This file is available both over the WWW and by anonymous ftp. To
obtain it by anonymous ftp, type the following commands.
csh> ftp ftp.sds.lcs.mit.edu
ftp> cd pub/Larch/LSL
ftp> get lsl.tar.Z
Unpack the distribution by typing the command tar xfz
lsl.tar.gz. This will create a directory named lsl3.1beta3.
Compile the checker by typing make depend and then
make in the directory lsl3.1beta3/Code.
Copy the executable file, named lsl, to some directory on your search
path, for example, /usr/local/bin.
If possible, make /usr/local/lib/LSL a symbolic link to the directory
lsl3.1beta3/LSL, or copy the contents of this directory to
If possible, copy the man page for the checker,
lsl3.1beta3/Doc/lsl.l, to /usr/man/manl. This makes it
possible for users to see the man page by typing man l lsl.
To prepare to use the LSL Checker, issue the following shell
command (or put the following line in your .login file), with
dir replaced by the full path name of the lsl3.1beta3
directory (or by /usr/local/lib):
setenv LARCH_PATH .:dir/LSL
To check a trait named xxx, put it in a file named
xxx.lsl and type the command lsl xxx. Any trait
yyy referenced by xxx should be found in a file
named yyy.lsl in one of the directories on
LARCH_PATH. See the man page for more details.