The Larch/C++ semantics for specification inheritance resembles that in Fresco [Wills92b], in that both impose the specifications of member functions on subtypes. However, Fresco does not have as general a notion as the simulation functions in Larch/C++, because all abstract values in Fresco look like tuples. In Leino's thesis [Leino95], methods are given a single specification which must be satisfied by implementations of subtypes. All specifications of objets are given using specification variables, so, as in Fresco, all abstract values support the same abstract fields, thus there is no problem in interpreting such specifications for subtype objects. A similar kind of specification inheritance is also found in LM3 [Jones91] (and Chapter 6 of [Guttag-Horning93]) and in Eiffel [Meyer92b], but neither LM3 nor Eiffel forces the subtype to be behavioral. That is, in LM3 and in Eiffel, the programmer can choose not to inherit specifications.
The semantics of weak behavioral subtyping, and simulation functions that take state into account are new with this work (January 1995). See our other work [Dhara-Leavens96] for an extended account.
Go to the first, previous, next, last section, table of contents.