@(#)$Id: README,v 1.8 1997/07/25 15:47:25 leavens Exp $

In this directory are samples relating to the Graph example from the paper:

	Yoonsik Cheon and Gary T. Leavens,
	A Quick Overview of Larch/C++.
	Journal of Object-Oriented Programming, 7(6):39-49, October 1994.

There are three template graph classes: Graph, DirectedGraph,
and UndirectedGraph.  You can find their specifications in the corresponding
".h" files.  There is an interesting use of implementation inheritance
to implement UndirectedGraph.

You will find besides graphs, specifications and implementations of
two template classes, List (as in LISP) and Set, and also two auxiliary
functions on lists, member and remove1st.  The specifications for these
are also found in the ".h" files.

Since we haven't verified, or even tested these,
so we don't make any guarantees or warranty about the code!

The version found in this directory is quite different from that in the paper
referenced above.  This version has been corrected and improved
for the current version of Larch/C++.

One correction is that the destructors no longer say
	modifies self;
or
	ensures trashed(self);
because trashing self is the job of delete, not the destructor.

A major difference is that, because of various changes,
the abstract values for the types were reformulated.
In particular, the main classes, Graph, DirectedGraph, and UndirectedGraph
now make use of specification variables (named nodes, edges, see Graph.h)
to define the abstract values of the types.  Note also,
in the DirectedGraph.pri file, the dependency and invariant clauses that
give the relation between the specification variables and the concrete
data members.

(Note also some differences in the types listed for quantified variables,
the use of the trait container_objs, and the omission of some renamings.
We also make use of parameterized sorts in some of the traits now.
The syntax has changed to use the keyword "behavior" and annotations.
And due to a semantic correction, we must also either explicitly declare that
no exceptions are thrown, as is done, or use the returns keyword.)