[Prev][Next][Index]

Re: (Support) Tools for Formal Software Development ?

Robert,

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
code checks.

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
3-540-94006.

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
of Iowa.

Jim H.

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.