Modular Verification of Object-Oriented Programs with Subtypes
				  by
			   Gary T. Leavens

Object-oriented programming languages like Smalltalk-80
have a message passing mechanism
that allows code to work on instances of many different types.
Techniques for the formal specification of such polymorphic functions
and abstract types are described,
as well as a logic for verifying
programs that use message passing but not object mutation or assignment.

The reasoning techniques formalize informal methods based on
the use of subtypes.
A formal definition of subtype relationships among
abstract types whose objects have no time-varying state
but may be nondeterministic or incompletely specified
is given.
This definition captures the intuition that each instance of a subtype
behaves like some instance of that type's supertypes.
Specifications of polymorphic functions are written
by allowing instances of subtypes as arguments.
Restrictions on the way that abstract types are specified ensure that such
function specifications are meaningful and do not have to be rewritten
when new subtypes are specified.
Verification consists of showing that the specified relation among types
has certain semantic properties,
that each expression's value is an instance of a subtype
of the expression's type,
and a proof of correctness that ignores subtyping.