# zbMATH — the first resource for mathematics

Class refinement as semantics of correct object substitutability. (English) Zbl 0963.68103
Summary: Subtype polymorphism, based on syntactic conformance of objects’ methods and used for substituting subtype objects for supertype objects, is a characteristic feature of the object-oriented programming style. While certainly very useful, typechecking of syntactic conformance of subtype objects to supertype objects is insufficient to guarantee correctness of object substitutability. In addition, the behavior of subtype objects must be constrained to achieve correctness. In class-based systems classes specify the behavior of the objects they instantiate. In this paper we define the class refinement relation which captures the semantic constraints that must be imposed on classes to guarantee correctness of substitutability in all clients of the objects these classes instantiate. Clients of class instances are modeled as programs making an iterative choice over invocation of class methods, and we formally prove that when a class $$C'$$ refines a class $$C$$, substituting instances of $$C'$$ for instances of $$C$$ is refinement for the clients.

##### MSC:
 68Q55 Semantics in the theory of computing
PVS; TkWinHOL
Full Text: