Behavioral Subtyping in Object-Oriented Languages
				  by
			Krishna Kishore Dhara

Abstract

Modularity and code reuse are two important features of
object-oriented programming.  Modularity means that adding new
components does not require reverifi- cation or respecification of
existing components. A common form of reuse in objectoriented programs
is to add new subtypes to existing types and to invoke already
existing procedures with objects of these new types. In such cases,
behavior of programs that contain these procedures also depend on the
behavior of the new subtype objects. Reverifying the code that uses
existing procedures whenever new types are added is not practical and
is not modular. Thus, a notion of behavioral subtyping that allows
sound modular reasoning is important for object-oriented programming.

In this dissertation, we study behavioral subtyping for arbitrary
abstract data types in the prescence of mutation and aliasing. We
propose two notions of behavioral subtyping. Strong behavioral
subtypes have objects that act like supertype objects in all cases,
whereas as weak behavioral subtypes have objects that only need to act
like supertype objects when manipulated as supertype objects. Both
these notions allow sound modular reasoning based on the static types
of variables in programs.  Weak behavioral subtyping allows
conclusions about programs based on the effects of individual
procedures but restricts certain forms of aliasing. Strong behavioral
subtyping allows all forms of aliasing but permits conclusions based
only on the history constraints of the types. History constraints are
the reflexive and transitive properties preserved by objects of a type
across different states of a program. We prove that both these
behavioral subtype notions are sufficient for sound modular reasoning.

Keywords: object-oriented programming, behavioral subtype, abstract
data type, mutation, aliasing, modular verification, supertype abstraction

1996 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 Porgrams -- logics of programs, pre- and post-conditions, theory