Leavens, Gary T. (1991) Specifying and Verifying Object-Oriented Programs: An Overview of the Problems and a Solution. Technical Report TR91-06, Department of Computer Science, Iowa State University.
Specifying and Verifying Object-Oriented Programs:
an Overview of the Problems and a Solution
Gary T. Leavens
This paper presents a careful analysis of the problem of reasoning
about object-oriented programs. A solution to this problem allows new
types to be added to a program without respecifying or reverifying
unchanged modules --- if the new types are subtypes of existing types.
The key idea is that subtype relationships must satisfy certain
semantic constraints based on the types' specified behavior.
Thus subtyping is not the same as inheritance of implementations
Subtyping aids specification and verification of object-oriented
programs by allowing supertypes to stand for their subtypes.
This reduces the problem of reasoning about both supertypes and their
subtypes to the problems of reasoning about just the supertypes and
proving that the subtype relationships satisfy the required constraints.
Contact site administrator at: firstname.lastname@example.org