Behavioral Subtyping, Specification Inheritance, and Modular Reasoning
                                  by
                 Gary T. Leavens and David A. Naumann

			       Abstract

Behavioral subtyping is an established idea that enables modular
reasoning about behavioral properties of object-oriented programs.
It requires that syntactic subtypes are behavioral refinements.
It validates reasoning about a dynamically-dispatched method call,
say E.m(), using the specification associated with the static type of
the receiver expression E.  For languages with references and mutable
objects the idea of behavioral subtyping has not been rigorously
formalized as such, the standard informal notion has inadequacies, and
exact definitions are not obvious.  This paper formalizes behavioral
subtyping and supertype abstraction for a Java-like sequential
language with classes, interfaces, exceptions, mutable heap objects,
references, and recursive types.  Behavioral subtyping is proved sound
and semantically complete for reasoning with supertype abstraction.
Specification inheritance, as used in the specification language JML,
is formalized and proved to entail behavioral subtyping.

Keywords: Behavioral subtyping, supertype abstraction,
specification inheritance, modularity, specification, verification,
state transformer, dynamic dispatch, invariants, Eiffel language,
JML language.

2006 CR Categories:
D.2.2 [Software Engineering]
        Design Tools and Techniques --- Object-oriented design methods;
D.2.3 [Software Engineering]
        Coding Tools and Techniques --- Object-oriented programming;
D.2.4 [Software Engineering]
        Software/Program Verification --- Class invariants,
        correctness proofs, formal methods,
        programming by contract, reliability, tools, Eiffel, JML;
D.2.7 [Software Engineering]
	Distribution, Maintenance, and Enhancement --- Documentation;
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 and Features --- classes and objects,
        inheritance;
F.3.1 [Logics and Meanings of Programs]
        Specifying and Verifying and Reasoning about Programs ---
                Assertions, invariants, logics of programs,
                pre- and post-conditions,
                specification techniques;