@(#) $Id: README,v 1.11 1997/07/30 15:54:56 leavens Exp $

This directory contains some examples of class specifications in Larch/C++.
They illustrate the idea of behavioral subtyping (both strong and weak)
and how inheritance of interface specifications works in Larch/C++.

There are five classes and a client function specified here.

The class Money is a new "fundamental class" that models US currency.
It is specified in Money.h.
It has a weak behavioral subtype specifed for it, MutableMoney,
which is specifed in MutableMoney.h.
The meaning of specification inheritance for such classes
is presented in the file MutableMoney2.h.

The specification of the template class String<C> shows how to
associate an LSL sort, in this case String[char], from Guttag and Horning's
Handbook, with a class name, without any obligation to implement it.
In this case, the class, String<char> is not, in fact, implemented.

The class BankAccount is the base class for PlusAccount.
PlusAccount is specified as a strong behavioral subtype of BankAccount
in the file BankAccount.h.

These classes shows how to use specification variables
when specifying classes.  Unlike the specification of Money and MutableMoney,
this style of specification is more common in Larch/C++.
In the specification of BankAccount,
the two specification variables used are types Money and String<char>.

There are two specifications of the class PlusAccount.
The first, in PlusAccount.h uses specification inheritance.
The second, in PlusAccount2.lh, shows the effect of specification inheritance.
It is interesting to compare them.

The C++ function transfer uses supertype abstraction, in that it should
work on arguments of either class BankAccount or PlusAccount.
Its specification is found in the file transfer.h.
(Note that there is information loss with the C++ function transfer,
as when a transfer is made, nothing stops the program from moving money
between the checking and savings accounts of PlusAccount arguments.
This is currently an open problem in Larch/C++.)

The examples here use the semantics of specification inheritance
explained in the Larch/C++ Reference Manual.
Something like this semantics, but with a different example specification
and a focus on specifications like Money and MutableMoney,
is described in the following paper.

	Krishna Kishore Dhara and Gary T. Leavens.
	Forcing Behavioral Subtyping Through Specification Inheritance.
	In Proceedings of the 18th International Conference on 
	Software Engineering, Belin, Germany, 1996, pages 258-267.
	(Also Department of Computer Science, Iowa State University,
	TR #95-20b, August 1995, revised August, December 1995.)

For more details on weak behavioral subtyping, see the following.

	Krishna Kishore Dhara and Gary T. Leavens.
	Weak Behavioral Subtyping for Types with Mutable Objects.
	In S. Brookes and M. Main and A. Melton and M. Mislove (eds.),
	Mathematical Foundations of Programming Semantics,
	Eleventh Annual Conference,
	http://www.elsevier.nl/locate/entcs/volume1.html
	Volume 1 of Electronic Notes in Computer Science, Elsevier, 1995.

	Krishna Kishore Dhara.
	Behavioral Subtyping in Object-Oriented Languages.
	Ph.D. Thesis, Department of Computer Science, Iowa State University.
	Technical Report TR #97-09, May 1997.
	Available from the following URL.
	ftp://ftp.cs.iastate.edu/pub/techreports/TR97-09/TR.ps.gz

The latter is where the MutableMoney example originates.