2.2 Formalization of various OO approaches in Z

Anthony Hall [Hal90,Hal94b,Hal94a] and others have shown how many basic aspects of an object-oriented approach can be handled very well in Z. These include such issues as objects in isolation, object identity, object creation and deletion, and subtyping. Although Hall shows several ways of handling such issues, his presentation is based on examples. We will try to treat topics generically and to discuss some points previously treated very lightly or not at all.

In traditional OO, objects are isolated, and state and behaviour are specified in an implementation-oriented, or, to be more precise, in an implementation-restricted, way. By contrast, a more general object model defines operations ``regardless of how this effect is achieved" [Hal94a]. The generalized object model, described in more detail in [ANS91,KR94] does not require invariants and operations to be ``owned" by a single object; rather, it uses collective state for invariants, and collective behavior for operation specifications. Both RM-ODP and especially the General Relationship Model follow this more general approach. In this manner collections of objects and their operations can be described in a convenient and natural way.

As ``traditional" Z does not always directly and explicitly correspond to an object model (for example, explicit information hiding in Z is not possible; but see below), various OO extensions to Z have been created for this purpose. These extensions usually supported the classical (message-oriented) object model, and therefore have difficulties in specifying collections of objects (collective state and collective behavior). An exception is OOZE [AG92], a development environment and language explicitly using the concept of a module. It is inspired by Z but has an algebraic semantics rather than a set theoretic model-based semantics. Standard Z itself does not have any problems in specifying collections of objects and their interactions, although it has certain other shortcomings.

[HW93] strongly suggests the need for parameterized modules, with structured parameters, in base Z (``a library can... be viewed as a super-schema"). It suggests that it is possible to achieve this goal, including specifying the internal structure of the parameters, by means of ``simply adding a normal Z predicate equating the variable [of the library] to the value", after the library has been instantiated with appropriate sets for generic set parameters. Another idea mentioned in the paper, ``having an explicit parameters section at the head of the library to specify the types of and constraints on the parameters", may be even better. Our present goal, however, is to see what can be done with standard Z as it is.

Unlike Hall [Hal90,Hal94b,Hal94a] and the chapters in Object Orientation in Z [SBC92], we try to give a general description of our approach, not just examples. This is in the same spirit as the well-known Z mathematical toolkit. While the notion of, say, injection is encountered in many specifications, the specifier does not describe this anew each time since it is already in the toolkit, available for reuse. In the same manner, the notion of such a generic relationship as a hierarchical composition, which is more complex, is encountered in many object-oriented specifications, and its specification should not be repeated each time. It should be defined once and made available for reuse. When appropriate, we will use examples to help in understanding the meaning and use of the notions we define. To be of value, the components in a toolkit must, of course, be widely useful and be precisely specified. RM-ODP Part 4.2 [ISO], the US Comments on this document [X3T96], and our paper in FMOODS'96 [JK97] describe some of these ideas in detail. We now want to expand upon this earlier work.

In addition to specifying the invariants of collections of objects, our toolkit will also include the specification of generic operations applied to these collections. For example, in defining a generic composition, we will specify not only its signature (above the line) and semantics (the invariant - below the line), but also such operations as ``delete a component instance" (designated by its identifier in a given naming context) with several possible outcomes, such as ``OK, composition still exists", ``OK, but no composition exists anymore", ``no such component instance", ``not an identifier", and so on. Some of these operations have been specified semi-formally: on the one hand, Clause 8.1 of [ISO95c] specifies the operation invariants, as well as pre- and postconditions for the following relationship management operations applied to any relationship: ESTABLISH, TERMINATE, BIND, UNBIND, QUERY, and NOTIFY; and on the other hand, for example, Clause F.4 of [ISO95c] specifies, in substantially greater detail, the signature and pre- and postconditions for these operations applied to a generic Composition relationship. Naturally, a formal specification of these operations leads to their being understood more clearly, in the same manner as [ISO] leads to substantially better understanding of at least some Clauses of [ISO95a].