Subtyping, Modular Specification, and Modular Verification for Applicative Object-Oriented Programs

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.

Abstract

Subtyping, Modular Specification, and Modular Verification
for Applicative Object-Oriented Programs
by
Gary T. Leavens and William E. Weihl
TR92-28d
Abstract
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
verification logic.
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.


Subjects:
All uncategorized technical reports


ID code:
00000031
Deposited by:
Staff Account on 01 September 1994





Contact site administrator at: ssg@cs.iastate.edu