[Prev][Next][Index]

Re: PD specification tools?

			      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.

     Executables:      lsl2.4.<platform>.Z
     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.

     Executables:      lcl2.4.<platform>.Z
     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.

     Executables:      lp2.4.<platform>.Z
     Run-time library: lp2.4.lib.tar.Z

     For documentation about Larch, and for descriptions of the Larch tools and
their use, see

[1]  ``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.
     ISBN 0-387-94006-5

[2]  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 src-report@src.dec.com.
     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 [1], a list of errata for [1], and a LaTeX style for displaying Larch
specifications.

How to get the Larch tools
--------------------------

1.  Type the following commands to initiate an anonymous ftp session:
     csh>       ftp larch.lcs.mit.edu
     Name:      anonymous
     Password:  your_email_address
     ftp>       cd pub/Larch
     ftp>       bin

2.  Retrieve a compressed executable for each tool you desire by typing 
    "get <tool>.<platform>.Z".

3.  Retrieve the run-time library for each tool you will be using by typing
    "get <tool>.lib.tar.Z".

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 
    "uncompress *.Z").

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.

Reporting bugs
--------------

Please report any bugs or problems with the Larch tools by completing the
following form and mailing it to larch@lcs.mit.edu.

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: