next up previous
Next: Class Refinement Up: Refinement in Object-Z Previous: Refinement in Object-Z


Bibliographical Notes

Definitions of the simulation rules for Object-Z were first given by Smith and Derrick [182] for a restricted subset of Object-Z where classes could not contain objects as state variables (which were unnecessary as the language was being combined with CSP).

Refinement in Object-Z is also briefly discussed by Smith in [179] and Duke et al in [76] in the context of behavioural compatibility. The central view of behavioural compatibility taken in [76] is the same notion that underlies refinement, i.e., an object $ ob_2$ is compatible with an object $ ob_1$ if $ ob_1$ can be replaced by $ ob_2$ without the substitution resulting in any detectable difference in behaviour. However, the blocking model defined in [76] differentiates between output messages controlled by the object and input messages which are under the control of the environment. It is also concerned with object substitutability whereas refinement is concerned with the behaviour and substitutability of the whole specification. Refinement in Object-Z as we have discussed here takes a simpler view in that operations are atomic and are under control of the environment irrespective of whether they contain input or output declarations.

Refinement methods have also been considered for a number of other object-oriented specification languages. In [27] a refinement methodology for OO action systems is presented, OO action systems being based upon the action systems formalism. Refinement for OO action systems is defined within the refinement calculus framework [14], and refinement is designed to preserve trace behaviour. There has also been work on refinement for object-oriented languages based around TLA [139] which includes, for example, DisCo [128] and TLO [47].

Work that is relevant to subtyping [7] in Object-Z includes that of [197,149,53]. Ideas on how to reconcile refinement with subtyping where new operations can be added are contained in [89,204] which looks at these questions in the context of CSP and its failures-divergences semantics.


next up previous
Next: Class Refinement Up: Refinement in Object-Z Previous: Refinement in Object-Z
E.A.Boiten 2002-11-22