Current Priorities

1.

Type checking in specifications,

2.

Add virgin?

3.

Is the semantics of invariants and history constraints as adding to the specification right?

4.

More discussion on classes, templates, specification modules in manual.

5.

More examples for teaching how to use Larch/C++ and how to specify existing code.

6.

Better semantics for subtyping with objects in abstract values.