Useability

• 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.)