Behavioral Subtyping is Equivalent to Modular Reasoning
		     for Object-oriented Programs
                                  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 and the standard informal notion has inadequacies.
This paper formalizes behavioral subtyping and introduces a new
formalization of modular reasoning, called supertype abstraction.  A
Java-like sequential language is considered, with classes and
interfaces, recursive types, first-class exceptions and handlers, and
dynamically allocated mutable heap objects; the semantics is designed
to serve as foundation for the Java Modeling Language (JML), a widely
used specification language.  Behavioral subtyping is characterized as
sound and semantically complete for reasoning with supertype
abstraction.

Keywords: Behavioral subtyping, modular reasoning, object-oriented
programming, recursive types, denotational semantics, functional
specification, Java Modeling Language (JML).

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;