Add ``such that'' syntax for declarations from the refinement calculus.
(This can already be simulated by using behavior statements.)
Extend syntax so can replace an lsl-op in a replace.
Examples of how to specify existing code, with examples.
(Some of this is starting to appear.)
A suite of VDM traits.
Other documentation: 1 page advertisment (what Larch/C++ is and how it works),
introductory booklet (for first-time users), tutorial.
Work examples! For example, Interviews.
(Update MFC examples.
Do some data structure examples.)
Gary T. Leavens