An extended semantic foundation for Object-Z

The paper argues that a strict notion of modularity is essential if the reuse of formally verified software components is to be achieved. Motivated by this idea, the author outlines a formal semantic domain for a sub-language of Object-Z. The semantics is based on the “object map model”; a model which accommodates the notion of object identity, structure, and behaviour. The semantics gives a meaning to classes which is strictly modular. It also defines a composition function which takes the modular meaning of classes and returns a system meaning. A characteristic feature of the semantics is the reliance upon the notion that OO operations consist of two parts: an internal state transition and an external interaction