@(#)$Id: README,v 1.2 1997/07/25 03:06:28 leavens Exp $

The example in this directory is adapted from J.P. Lejacq's paper in
SIGPLAN 26(10), Oct, 1991.  The example is found in the files
Counter.lh and SmallCounter.lh.

This example shows something that claims to be a
behavioral subtype, but is not.
That is, although SmallCounter is a public subclass of Counter,
SmallCounter is not a subtype of Counter.
One reason is that the precondition of Counter::increment
doesn't imply the precondition of SmallCounter::increment.

For further discussion of rules of thumb like this about behavioral subtyping,
see, for example, the papers of Pierre America (e.g. in Lecture Notes in
Computer Science vol. 489), or Barbara Liskov and Jeannette Wing
(in proceedings of ECOOP '93 and OOPSLA '93).

"But wait a minute," you may say.  "I thought from reading the manual,
or from reading some of your papers like...

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

... that in Larch/C++, every public subclass *is* a behavioral subtype
of the type specified in its public superclasses.  So how can it be that
SmallCounter is not a behavioral subtype, because it's a public subclass?"

Not to confuse the issue, but when interpreted by the Larch/C++ semantics,
a SmallCounter is a behavioral subtype of Counter.
By specification inheritance it must obey the specification of Counter,
as well as the behavior specified for SmallCounter.
However, SmallCounter can't be implemented.  To see this, look in the file
SmallCounterDesugared, where the specification of SmallCounter is desugared
(slightly) to reveal the effects of specification inheritance.
In this, one can see that the member function increment has to terminate
with the specification variable self incremented by 1, even when value
is between SmallLimit and Limit.  But by the invariant for SmallCounter,
this can't be done for such values.

The moral of the story of this counterexample is that in Larch/C++
subclasses can only strengthen the specification of their public superclasses,
but they can strengthen them too much.