Re: Where to get FAQ??


I don't think anyone has written a Larch FAQ yet.  Any volunteers to
create/publish one?

There are a couple of WWW home pages that can probably answer quite a few
of your questions:



Among other things, the latter contains the following specific information
about Larch:

Larch is a multi-site project exploring methods, languages, and tools for
the practical use of formal specifications. Much of the early work was done
in the Systematic Programming Development Group at MIT's Laboratory for
Computer Science and at Digital's Systems Research Center in Palo Alto,

Known sites with Larch home pages, and some of the active

      Massachusetts Institute of Technology, Laboratory for Computer
      Science, Systematic Programming Development Group, John Guttag, Steve
      Garland, Yang Meng Tan, David Evans

      Digital Equipment Corporation, Systems Research Center, Jim Horning

      Carnegie Mellon University, School of Computer Science, CMU Larch
      Home Page, Jeannette Wing

      Iowa State University, Department of Computer Science, Gary Leavens

      Research unit INRIA Lorraine (Nancy), France, Pierre Lescanne

      Danish Technical University, Hardware verification using LP, Jorgen

      Aarhus University, Denmark, TLP (The TLA Proof Checker), Urban Engberg 

Tools available

      LP, the Larch Prover; a description in the Stanford Prover database 
      LSL, the Larch Shared Language checker 
      LCL, Larch/C interface language checker 
      LCLint, C program checker that exploits LCL specifications, if provided 

Larch books

      Larch: Languages and Tools for Formal Specification, John V. Guttag
     and James J. Horning, with S.J. Garland, K.D. Jones, A. Modet, and
     J.M. Wing, Springer-Verlag Texts and Monographs in Computer Science,
     1993, ISBN 0-387-94006-5, ISBN 3-540-94006-5.

      First International Workshop on Larch, Dedham 1992, Ursula Martin and
     Jeannette M. Wing (Eds.), Springer-Verlag Workshops in Computing,
     1993, ISBN 30540-19804-0, ISBN 0-387-19894-0.

The Larch family of languages

The Larch family of languages supports a two-tiered, definitional style of
specification. 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 Larch interface languages, and the latter is the Larch
Shared Language (LSL).

Interface languages are used to specify the interfaces between program
components. Each specification provides the information needed to use an
interface. A critical part of each interface is how components communicate
across the interface. Communication mechanisms differ from programming
language to programming language. For example, some languages have
mechanisms for signalling exceptional conditions, other do not. More subtle
differences arise from the various parameter passing and storage allocation
mechanisms used by different languages.

It is easier to be precise about communication when the interface
specification language reflects the programming language. Each interface
language deals with what can be observed by client programs written in a
particular programming language. Larch interface languages have been
designed for a variety of programming languages, including Ada, C, C++,
CLU, CORBA, ML, Modula-3, and Smalltalk. There are also "generic" Larch
interface languages that can be specialized for particular programming
languages or used to specify interfaces between programs in different

Interface specifications rely on definitions from auxiliary specifications,
written in LSL, to provide semantics for the primitive terms they
use. Specifiers are not limited to a fixed set of notations, but can use
LSL to define specialized vocabularies suitable for particular interface
specifications or classes of specifications

A brief chronology of Larch

These notes are condensed from the Preface of Larch: Languages and Tools
for Formal Specification.

This project has been a long time in the growing. The seed was planted by
Steve Zilles on October 3, 1973. During a programming language workshop
organized by Barbara Liskov, he presented three simple equations relating
operations on sets, and argued that anything that could reasonably be
called a set would satisfy these axioms, and that anything that satisfied
these axioms could reasonably be called a set. John Guttag refined this
idea. In his 1975 Ph.D. thesis (University of Toronto), he showed that all
computable functions over an abstract data type could be defined
algebraically using equations of a simple form. He also considered the
question of when such a specification constituted an adequate definition.

As early as 1974, we realized that a purely algebraic approach to
specification was unlikely to be practical. At that time, we proposed a
combination of algebraic and operational specifications which we referred
to as "dyadic specification." By 1980 we had evolved the essence of the
two-tiered style of specification; the term "two-tiered" was introduced by
Jeannette Wing in her 1983 Ph.D. thesis (MIT).  A description of an early
version of the Larch Shared Language was published in 1983. The first
reasonably comprehensive description of Larch was published in 1985. But
many readers complained that Larch in Five Easy Pieces should have been
called Larch in Five Pieces of Varying Difficulty.

In the spring of 1990, software tools supporting Larch were becoming
available, and we began using them to check and reason about
specifications. We decided that it was time to make information on Larch
more widely available. We originally thought of an anthology of existing
papers, but the editors we contacted urged us to provide a more coherent
and integrated presentation of the material. The resulting book appeared in

The First International Workshop on Larch, organized by Ursula Martin and
Jeannette Wing, was held in Dedham, Massachusetts, July 13-15, 1992, and
the proceedings were published in 1993.

Jim H.