Re: PD specification tools?
To: email@example.com (David Taylor)
Subject: Re: PD specification tools?
Date: Wed, 13 Oct 93 13:16:23 -0700
Delivery-Date: Wed, 13 Oct 93 13:16:38 -0700
In-Reply-To: Message of Wed, 13 Oct 1993 17:45:17 GMT
The Larch Tool Set
MIT/LCS Distribution Site
March 26, 1993
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).
The Larch Tool Set contains tools that can be used to analyze and reason
about Larch specifications. The following tools are available by anonymous ftp
from the directory pub/Larch on larch.lcs.mit.edu. For each tool, <platform>
is one of the following supported system architectures:
decmips DECstation running Ultrix
sparc Sparcstation running SunOS
vax DEC VAX running Ultrix or Berkeley Unix 4.3 with NFS
lsl: Larch Shared Language Checker.
Checks syntax and sorts in LSL specifications.
Release 2.4 fixes several bugs in the previous release.
Run-time library: lsl2.4.lib.tar.Z
lcl: Larch/C Interface Language Checker.
Checks syntax and types in LCL specifications.
Release 2.4 completed supersedes all prior releases.
Run-time library: lcl2.4.lib.tar.Z
lp: The Larch Prover.
Assists with proofs in a subset of first-order logic with equality.
Release 2.4 fixes several bugs in Release 2.2.
Run-time library: lp2.4.lib.tar.Z
For documentation about Larch, and for descriptions of the Larch tools and
their use, see
 ``Larch: Languages and Tools for Formal Specification,''
John V. Guttag and James J. Horning (editors), with
Stephen J. Garland, Kevin D. Jones, Andres Modet and Jeannette M. Wing,
Springer-Verlag, Texts and Monographs in Computer Science, 1993.
 Stephen J. Garland and John V. Guttag,
``A Guide to LP, The Larch Prover,'' Research Report 82,
DEC Systems Research Center, 130 Lytton Avenue, Palo Alto, CA 94301.
A hardcopy can be ordered by sending e-mail to firstname.lastname@example.org.
PostScript files containing an addendum to, and an updated version of,
this report are part of the LP distribution.
The distribution also contains man pages for the Larch tools, grammars for
the Larch languages, on-line help for the Larch Prover, and a file
larchDocs.tar.Z that contains a constantly updated version of the bibliography
in , a list of errata for , and a LaTeX style for displaying Larch
How to get the Larch tools
1. Type the following commands to initiate an anonymous ftp session:
csh> ftp larch.lcs.mit.edu
ftp> cd pub/Larch
2. Retrieve a compressed executable for each tool you desire by typing
3. Retrieve the run-time library for each tool you will be using by typing
How to install the Larch tools
1. Create a directory to hold the tools and their run-time libraries, e.g.,
/u/Larch. Create a subdirectory to hold the tools, e.g., /u/Larch/bin.
2. Move the files you retrieved to /u/Larch and uncompress them (by typing
3. Install the executables in /u/Larch/bin, removing the version number and
platform as you do this (e.g., by typing "mv lsl2.4.sparc bin/lsl"). Type
"chmod +x bin/*" to make the tools executable.
4. Enable the tools to be invoked by Unix shell commands, either by putting
/u/Larch/bin on your search path or by putting symbolic links to the tools
in some directory (e.g., /usr/local) that is on your search path.
5. Install the run-time libraries by using tar to extract their contents,
e.g., by typing "tar xf lsl2.4.lib.tar". This will create subdirectories
named LSL, LCL, and LP of the Larch directory. The subdirectory for each
tool has the following subdirectories:
docs/ Contains a man page and a grammar.
lib/ Contains run-time support.
samples/ Contains sample specifications or proofs.
6. If you will be using both the LCL and the LSL checkers, issue the following
shell command (or put the following line in your .login file):
setenv SPEC_PATH .:/u/Larch/LCL/lib:/u/Larch/LSL/lib
If you will be using only the LSL checker, use the following instead:
setenv SPEC_PATH .:/u/Larch/LSL/lib
7. If you will be using LP, make /usr/local/lib/lp a symbolic link to
/u/Larch/LP/lib. If you cannot do this, alias the command "lp" to
"lp -d /u/Larch/LP/lib".
8. Copy the man pages (/u/Larch/LSL/docs/lsl.l, /u/Larch/LCL/docs/lcl.l, and
/u/Larch/LP/docs/lp.l) to /usr/man/manl. To see the man page for LP, users
need to type "man l lp".
Using the Larch tools
Type: "lsl xxx" to check the LSL trait named xxx in the file named xxx.lsl.
"lcl xxx" to check the LCL specification in the file named xxx.lcl.
"lp" to initiate an interactive session with LP.
See the man pages for more details.
Please report any bugs or problems with the Larch tools by completing the
following form and mailing it to email@example.com.
Name: _______________________________ Date: __________________
E-mail address: _________________________
Tool: ___ LCL ___ LSL ___ LP
Version: ___ [Type "lcl -version", "lsl", or "lp" to find out.]
Hardware: ___ Sparc ___ DECmips ___ Vax
___ Other: __________________________
Operating System and Version: _____________________________
Is the problem preventing you from making progress with the Larch tools?
___ Yes ___ No
Which of the following symptoms occurred (check all that apply):
__ system level error (OS crashes or hangs, unrelated data is lost)
__ program crashes (segmentation fault, core dump, etc.)
__ program reports a fatal error
__ program hangs
__ program exhibits __ incorrect, __ mysterious, or __ unfriendly behavior
__ program destroys data
__ poor or incorrect error messages
__ incorrect or missing documentation
__ missing feature (please elaborate)
__ other (please elaborate)
Problem description (please append any source files, after narrowing them down
to a small example):
Any workarounds you've found: