Formal Definitions of Behavioural Compatibility for Active and Passive Objects

The modular refinement of object-oriented specifications requires a sound theory of behavioural compatibility of classes. Such a theory will depend on the way in which objects of a class interact with their environment. This paper defines two notions of behavioural compatibility. Observational compatibility is relevant when an active object is placed within a passive environment and operational compatibility when a passive object is placed in an active environment. Rules for maintaining each type of behavioural compatibility through inheritance are also presented. 1 Introduction Recently, several approaches have been proposed for adding object-oriented 1 concepts to formal methods[11, 5, 3]. These approaches have been largely motivated by the need for enhanced structuring in large specifications. One of the advantages of this structuring is that an object-oriented specification can be refined in a modular fashion by separately refining the classes of each of its component objects. T..