archives

Specifying and Verifying Object-Oriented Programs: An Overview of the Problems and a Solution

Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

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.

Full text available as:Postscript
Adobe PDF

Abstract

Specifying and Verifying Object-Oriented Programs:
an Overview of the Problems and a Solution
by
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
(subclassing).
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.




Subjects:All uncategorized technical reports



ID code:00000005


Deposited by:Staff Account on 01 February 1991









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