[Object Orientation in Z] Susan Stepney, Rosalind Barden, David Cooper, editors.
Object Orientation in Z .

Workshops in Computing. Springer, 1992.

Copyright © 1992 Logica UK Ltd

A. Z and HOOD

HOOD --- Hierarchical Object Oriented Design --- is the approved European Space Agency design method for Ada. It is not actually object oriented, since it has no idea of classes or inheritance; it is object based (as is Ada). The hierarchical design approach consists of decomposing a parent object into several child objects which act together to provide the functionality of the parent.

In conventional HOOD, the more 'formal' parts of the specification are achieved by using Ada as a program description language. [Giovanni & Iachini 1990] describe a way to use Z to specify the HOOD objects. A parent object is specified abstractly (a WHAT specification), using Z to specify an abstract state and abstract operations. The child objects, identified by the HOOD design process, are specified abstractly (as a WHAT specification, or as a WHAT-WITH specification for objects that use other objects). The parent object is then re-specified, more concretely in terms of these child objects (a HOW specification), by defining how its abstract state and operations are built from its children and their operations.

The approach differs from plain Z in two ways:

  1. It uses HOOD constructs to limit the scope of the Z definitions. For example, child operation definitions are not visible outside the parent.
  2. It extends Z's dot notation to refer to particular objects' operations.

As a trivial example (not using the WHAT-WITH specifications), consider an abstract parent specification that has an (internal) state specified by State and a series of available operations Op 1, .... Its HOOD+Z specification would look something like:

\begin{zed}WHAT\ Parent ::=\end{zed}\begin{schema}{Parent}State\end{schema}\begin{schema}{Op1}\Delta Parent\where pred\end{schema}\begin{zed}\mbox{(other operations)}\\END\ Parent\end{zed}

The HOOD process might then decompose the parent into various child objects, each with a specification looking like:

\begin{zed}WHAT\ Child1 ::=\end{zed}\begin{schema}{Child1}state\end{schema}\begin{schema}{Op1}\Delta Child1\where pred\end{schema}\begin{zed}\mbox{(other operations)}\\ END\ Child1\end{zed}

The parent's concrete specification, in terms of its children, might then look like:

\begin{zed}HOW\ Parent ::=\end{zed}\begin{schema}{Parent}Child1\\Child2\\\ldots\end{schema}\begin{zed}Op1 \defs Child1.Op1\\Op2 \defs Child2.Op1\\Op3 \defs Child2.Op2\\\ldots\\END\ Parent\end{zed}

These two extensions give Z a full object-based capability: local scope and the ability to apply operations to objects. [Iachini 1991] describes a proposed notation to allow operation schemas to be iterated (giving something analogous to a `while loop'), since such constructs can occur in the internals of object specifications.

HOOD also supports concurrency (in the Ada style) --- the authors want to extend their Z work to cover this aspect, too. If they are successful, this appears to be a promising approach to 'firming up' HOOD and Ada designs.