@(#) $Id: README,v 1.5 1999/01/10 22:44:42 leavens Exp $

This directory contains the shapes examples from the following paper.

	Gary T. Leavens.
	An Overview of Larch/C++: Behavioral Specifications for C++ Modules.
	In Haim Kilov and William Harvey (eds.),
	Specification of Behavioral Semantics in Object-Oriented Information
	Modeling (Kluwer Academic Publishers, 1996), pages 121-142.

Hence some of the examples are:
	Copyright (c) Kluwer Academic Publishers, 1996.  Used by permission.

However, the version of the examples given here are revised, corrected,
and simplified to correspond to the latest release of Larch/C++.
A revised version of the paper that reflects (most of) this update
is ISU CS Dept. TR #96-01d. This is available in the Larch/C++ release,
and from the following URL.
	ftp://ftp.cs.iastate.edu/pub/techreports/TR96-01/TR.ps.Z

These examples were treated as a case study in the following book.

	Susan Stepney, Rosalind Barden, and David Cooper, editors.
	Object Orientation in Z.
	Workshops in Computing. Springer-Verlag, Cambridge CB2 1LQ, UK, 1992.

The trait FourSidedFigure gives some basic mathematical abbreviations
used in these specifications.
The theory of vectors can be found in the trait PreVector,
which is included by FourSidedFigure.

The class QuadShape is at the top of the specified class hierarchy.
It has subclasses Quadrilateral and ParallelShape;
the class Parallelogram is a subtype of both of these.
The classes Rectangle and Rhombus are both subclasses of ParallelShape;
the class Square is a subclass of both of these.
All of these, being public subclasses, are also
behavioral subtype relationships.

Addtiional traits used in the examples can be found here, or in
the LSL handbook of Guttag and Horning, or in the following.

	Gary T. Leavens. LSL Math traits.
	http://www.cs.iastate.edu/~leavens/Math-traits.html

You will need to get the math traits in order to use the LSL checker
on this example.  These traits must also be in your LARCH_PATH
in order to run the Larch/C++ or lsl checker on the examples.