Date: Fri, 10 Sep 93 11:18:49 EDT From: garland@larch.lcs.mit.edu (Stephen Garland) To: clt@sail.stanford.edu Subject: Larch Tool Set Last March, the following announcement was distributed to the mailing list larch-interest@pa.dec.com. Apparently, some people who had corresponded with us earlier about their interest in Larch are not on that mailing list. If you are one of these, we apologize for not sending you this announcement earlier, and we request that you send e-mail to larch-interest@pa.dec.com to have your name placed on that list. If you have already received this announcement, we apologize for the duplicate. 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, 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..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..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..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 ..Z". 3. Retrieve the run-time library for each tool you will be using by typing "get .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: