Re: (Support) Tools for Formal Software Development ?
To: firstname.lastname@example.org (Robert Stabl)
Subject: Re: (Support) Tools for Formal Software Development ?
Date: Mon, 27 Sep 93 16:42:20 -0700
Delivery-Date: Mon, 27 Sep 93 16:42:29 -0700
In-Reply-To: Message of Mon, 27 Sep 1993 22:44:04 GMT
There are a number of tools available from MIT (and a few from elsewhere)
available to support the Larch family of languages. Tools include syntax
checkers, a serious theorem-prover, and (for C) a lint-like tool that uses
additional information from partial specifications to do stronger static
The best description is in "Larch: Languages and Tools for Formal
Specification," by Guttag, Horning, et al., Springer-Verlag Texts and
Monographs in Computer Science, New York, 1993, ISBN 0-387-94006 or
The main updates on tool availability are:
- The LCLint checker, referred to in the future tense in the book, was
implemented over the summer. MIT expects to make it available as soon as
some performance tuning is completed. It has already discovered problems
in real production C code here at SRC.
- There has been a new release (2.3) of the Larch/C++ tools by University
PS If you were in Munich, you could find out a lot about the Larch Prover
from Prof. Dr. Manfred Broy of TUM, who has been a serious user, in the
course of preparing to design his own.