Modular specification and verification of object-oriented programs

A method for modular specification and verification using the ideas of subtype and normal type is presented. The method corresponds to informal techniques used by object-oriented programmers. The key idea is that objects of a subtype must behave like objects of that type´s supertypes. An example program is used to show the reasoning problems that supertype abstraction may cause and how the method resolves them. Subtype polymorphism is addressed, and specification and verification update is discussed. A set of syntactic and semantic constraints on subtype relationships, which formalize the intuition that each object of a subtype must behave like some object of each of its supertypes, is examined. These constraints are the key to the soundness of the method. To state them precisely, a formal model of abstract type specifications is used.<>