Technical Report Number
Computer Systems Organization, Theory of Computation
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.