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.

Getting LSL

To use the LSL Checker and Handbook, you need to retrieve and install the file lsl.tar.gz. 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
     Name:      anonymous
     Password:  your_email_address
     ftp>       cd pub/Larch/LSL
     ftp>       bin
     ftp>	get lsl.tar.Z
     ftp>	quit

Installing LSL

Using 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):

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.