An Introduction to Larch

Presented by Eric Eide

Larch is a system for formal specification and verification of program modules. Larch is not a single language; rather, Larch is a family of languages, each tailored to the requirements of a particular programming language. There are Larch specification languages for C, C++, Modula-3, Ada, ML, Smalltalk, CLU, and CORBA IDL.

Larch supports two-tiered specification because each Larch language consists of two sublanguages: a Larch Shared Language (LSL) component and a behavioral interface specification language (BISL) component. The Larch Shared Language component defines a mathematical model --- a set of types and operators on those types --- that will be used to reason about a program module. The BISL component connects pieces of the program module (e.g., functions and methods) with the mathematical abstractions defined in the LSL specification.

Larch is interesting to the Flux project, Flick in particular, for a number of reasons. First, Larch provides a formal way to document and reason about program modules in a number of languages. Flick could use the Larch languages as the basis for (1) flexible specification of presentation and (2) automatic creation of specialized implementations driven by interprocedural code analysis, resource management constraints, or security concerns.

Presentation Materials

• The slides in PostScript.
  
  
• The slides with annotations, also in PostScript.
  
  
• The LaTeX sources for the above.
  
  
• Larch/C++ specifications for portions of the Microsoft Foundation Class (MFC) Library were photocopied from David Egle's technical report, cited below.

Reference Materials

• The Larch home pages at MIT, CMU, and DEC SRC, and Jim Horning's Larch Page.
  
  
• Home pages for Larch systems and tools:

  LCLint (Larch/C)	Larch/C++	Larch/Smalltalk
  The Larch Shared Language (LSL) Checker	The Larch Prover (LP)	The Larch Development Environment
  LSL Handbooks	lsl2html	lcpp2html

• The comp.specification.larch newsgroup and the Larch FAQ list.
  
  
• The Larch interest mailing list <larch-interest@pa.dec.com>. Send subscription requests to <larch-interest-request@pa.dec.com>. An archive of the mailing list is available. The results of a July 1994 survey of the participants is also online.
  
  
• Papers and other publications:
  Note that local copies of the papers are available only to local (cs.utah.edu) users.
  • Publications about Larch from MIT/LCS.
    
    
  • David M. Egle. Evaluating Larch/C++ as a Specification Language: A Case Study Using the Microsoft Foundation Class Library. Technical Report #95-17. Iowa State University. July 1995. (PostScript from Iowa; PostScript from local server)
    
    
  • David Evans. Using Specifications to Check Source Code. SM Thesis, Technical Report MIT/LCS/TR-628. MIT. June 1994. (abstract; PostScript from MIT; PostScript from local server)
    
    
  • David Evans, John V. Guttag, James J. Horning, and Yang Meng Tan. ``LCLint: A Tool for Using Specifications to Check Code.'' Symposium on the Foundations of Software Engineering. December 1994. (abstract; PostScript from MIT; PostScript from local server)
    
    
  • John V. Guttag et al. ``A Larch Shared Language Handbook.'' Online version of Appendix A of Larch: Languages and Tools for Formal Specification, Springer-Verlag, 1993. (HTML from DEC SRC; PostScript from DEC SRC; PostScript from local server)
    
    
  • John V. Guttag and James J. Horning, with S. J. Garland, K. D. Jones, A. Modet, and J. M. Wing. Larch: Languages and Tools for Formal Specification. Springer-Verlag Texts and Monographs in Computer Science, 1993, ISBN 0-387-94006-5, ISBN 3-540-94006-5.
    
    
  • Kevin D. Jones. LM3: A Larch Interface Language for Modula-3: A Definition and Introduction, Version 1.0. Technical Report 72. DEC SRC. June 1991. (PostScript from DEC SRC; PostScript from local server)
    
    
  • Kiyotaka Kuroda. ``Specifying Device Types in Larch.'' August 1995. (HTML from CMU)
    
    
  • Gary T. Leavens. An Overview of Larch/C++: Behavioral Specifications for C++ Modules. Technical Report #96-01b. Iowa State University. February 1996, revised March, April 1996. (PostScript from Iowa; PostScript from local server)
    
    
  • Gary T. Leavens. ``LSL Handbooks.'' June 1996. (HTML from Iowa)
    
    
  • Gowri Sankar Sivaprasad. Larch/CORBA: Specifying the Behavior of CORBA-IDL Interfaces. MS Thesis. Technical Report #95-27a. Iowa State University. November 1995. (PostScript from Iowa; PostScript from local server)
    
    
  • Mark T. Vandevoorde. Exploiting Specifications to Improve Program Performance. Ph.D. Thesis. Technical Report MIT/LCS/TR-598. MIT. February 1994. (abstract; PostScript from MIT; PostScript from local server)
    
    
  • Mark T. Vandevoorde and John V. Guttag. ``Using Specialized Procedures and Specification-Based Analysis to Reduce the Runtime Costs of Modularity.'' Symposium on the Foundations of Software Engineering. December 1994. (PostScript from MIT; PostScript from local server)
    
    
  • Amy Moormann Zaremski. A Larch Specification of the Miro Editor. Technical Report CMU-CS-91-111. CMU. February 1991. (PostScript from CMU; PostScript from local server)

• People:
  • John V. Guttag at MIT.
  • Stephen J. Garland at MIT.
  • James J. Horning at InterTrust Technologies, previously at DEC SRC.
  • Jeannette M. Wing at CMU.
  • Gary T. Leavens at Iowa State University.