Larch/C++ is still in development. As you can see, this reference manual is still a draft, and there are some holes in it. [[[And some notes for the author by the author that look like this.]]] Most of the small scale parts of the language are adequately documented now. The documentation of classes is in pretty good shape, but still needs work. A lot of work is needed on the documentation of templates and specification modules. Current work on the manual focuses on details of class specifications.
The major work remaining on the design of Larch/C++ is related to: aliasing, subtyping for mutable types, and subclassing. The idea with subclassing is to record enough information in the specification of a class so that someone can program a derived class without looking at the code of the base class. (This work was supported in part by NSF grant CCR-9593168.)
Influences on Larch/C++ that may lead to changes in its design include the evolution of LCL [Tan94] [Chalin95] [Chalin-etal96] and the evolution of C++ itself. Another influence is the ongoing effort to use Larch/C++ on examples, in designing the Larch/C++ tools, and to (ultimately) give a formal semantics to Larch/C++.
The current release of Larch/C++ is not all we would hope for, especially with respect to the tools. It contains just a checker for Larch/C++ and a tool for making HTML files from specifications. The checker does checking that the used LSL traits exist, and checks their syntax, but does not yet use that information to do sort checking within Larch/C++ specifications. (That is coming, however.)
In [Cheon-Leavens94] we had described the automatic generation
of a header file (the `.lh' file) from a specification,
as was done in LCL
(see [Guttag-Horning91b] and Chapter 5 of [Guttag-Horning93]).
However, we have abandoned that plan, and now follow
the latest version of LCL
[Evans96b], by allowing Larch/C++ to be used as an annotation language.
The current release allows one to use special comments (of the form //@
and /*@ ... @*/ that enclose specification constructs.
This allows specifications to be added directly to C++ header files
(the `.h' files) if desired.
See section 2.4 Modules and Files, for more information.
Our highest priority project now is a sort-checker for Larch/C++ specifications, and tools to generate LSL traits that Larch/C++ implicitly creates (such as those used in inheritance of specifications, and those implicitly generated by mentioning C++ types). In the more distant future, we plan some tools to aid formal verification. However, tools to aid formal verification would need to come after a formal semantics for Larch/C++ and probably more research into verification of (a subset of) C++ programs.
Included in the current release of Larch/C++ is a document `TODO.ps' which gives more details on our plans.
Go to the first, previous, next, last section, table of contents.