Forcing Behavioral Subtyping Through Specification Inheritance
				  by
		Krishna Kishore Dhara and Gary Leavens

			       Abstract

A common change to object-oriented software is to add a new type of
data that is a subtype of some existing type in the program.
However, due to message passing unchanged parts of the program may now
call operations of the new type.  To avoid reverification of unchanged
code, such operations should have specifications that are related to
the specifications of the appropriate operations in their supertypes.
This paper presents a specification technique that uses inheritance of
specifications to force the appropriate behavior on the subtype
objects.  This technique is simple, requires little effort by the
specifier, and avoids reverification of unchanged code.  We present
two notions of such behavioral subtyping, one of which is new.
We show how to use these techniques to specify examples in C++.


Keywords: object-oriented programming, behavioral subtype,
abstract data type, mutation, simulation function, 
modular verification, supertype abstraction, interface specification, 
Larch/C++, class, C++, subclass.

1994 CR Categories:
D.1.5 [Programming Techniques] Object-oriented Programming;
D.3.1 [Programming Languages] Formal Definitions and Theory --- semantics;
D.3.2 [Programming Languages] Language Classifications
	--- object-oriented languages;
D.3.3 [Programming Languages] Language Constructs
	--- Abstract data types, modules, packages;
F.3.1 [Logics and Meanings of Programs]
	Specifying and Verifying and Reasoning about Programs ---
                pre- and post-conditions, specification techniques.


Copyright 1996 IEEE. A shorter version and slightly dated version is
published in the Proceedings of the 18th International Conference on
Software Engineering (ICSE-18), March 25-29, 1996, Berlin, Germany.
Personal use of this material is permitted.  However, permission to
reprint/republish this material for advertising or promotional
purposes or for creating new collective works for resale or
redistribution to servers or lists, or to reuse any copyrighted
component of this work in other works, must be obtained from the IEEE.