Leavens, Gary T. and Weihl, William E. (1994) Subtyping, Modular Specification, and Modular Verification for Applicative Object-Oriented Programs. Technical Report TR92-28d, Department of Computer Science, Iowa State University.
Subtyping, Modular Specification, and Modular Verification
for Applicative Object-Oriented Programs
Gary T. Leavens and William E. Weihl
We present a formal specification language and a formal
verification logic for a simple object-oriented programming
language. The language is applicative and statically typed,
and supports subtyping and message-passing. The verification
logic relies on a behavioral notion of subtyping that captures
the intuition that a subtype behaves like its supertypes. We
give a formal definition for legal subtype relations, based on
the specified behavior of objects, and show that this
definition is sufficient to ensure the soundness of the
The verification logic reflects the way
programmers reason informally about object-oriented programs,
in that it allows them to use static type information,
which avoids the need to consider all possible run-time subtypes.
We also show that the logic does not require reverification of
unchanged code when legal subtypes are added to a program.
Contact site administrator at: email@example.com