5. Conclusion

We have presented the µZ calculus, a strict computation model for it, and a sketch of the implementation of this model by the abstract machine ZAM.

Calculus.

µZ provides a way on viewing the $\lambda$-calculus, predicate calculus, schema's calculus, set-algebra, etc., in a unified, small expression language. Though the motivation of µZ and its implementation is the execution of a subset of the specification language Z, the approach is also interesting for the implementation of declarative programming languages in general, since µZ can embed these languages. In its intention, the µZ calculus is comparable to the calculi given for Oz in [15], though it doesn't provides the ``impure'' concepts of memory cells and committed choice.

Computation Model.

µZ's computation model is comparable to the one described in [6]. µZ's set values, $\mzbigcup \Mzsingle{\mzexvS} \cup \mzbigcup \Mzinten{\mzpatS}{\mzctrS}$, correspond to the ``definitional trees'' used in this work. Higher-orderness has perhaps a cleaner representation in µZ, since set-values are first-order inhabitants of the operational domain which definitional trees are not - on the other hand, µZ's set values are more restricted then definitional trees since they only support the ``or'' and the ``branch'' constructor.

A strict computation order has been chosen for a easier traceability of execution by humans, which is important for the application to test-data evaluation, and a supposed better overall performance. It is drawn from experiences with functional programming and language implementation that the overhead of laziness has to be paid for significantly, which in practice often results in that programmers use strictness annotations [8].

Machine.

The ZAM's principle design is a straight consequence of µZ's computation model. Some aspects of the design and implementation are comparable to the AMOZ machine for Oz described in [11]. Yet, whereas in this machine by default sequential execution takes place, and only instructions which need to suspend are scheduled for concurrent execution, in the ZAM threads are incorporated from the beginning of a resolution. This allows for the simple but very effective optimization of dynamic choice scheduling.

The use of C++ as the implementation language of the ZAM is a consequence of experiences with an earlier implementation of a deterministic machine for µZ in Java (which uses concurrent constraint resolution for dealing with ``parallel and'', but cannot backtrack). This implementation directly compiles to Java instead of interpreting virtual code. Java's thread system is employed for executing concurrent constraints. The approach turned out to be problematic for several reasons. First, an order of magnitude of performance is lost because of the interpretative character of current Java implementations themselves - meanwhile the advantage of portability does not count so much for an abstract machine implementation which does not rely on library functionality (a core of C++ is supported on all important platforms today). Second, the ``clean'' language design of Java hinders some ``tricks'' one would like to apply for the sake of efficiency in an implementation: allocating unitialized memory, pointer calculation, working with double indirections, and so on. Third, Java threads, which are the only (efficient) possibility to implement context switching in an non-interpretative approach, turned out to have serious restrictions on some platforms: there may be an upper bound of threads which can be allocated at the same time, and there is no guarantee about the allocation costs, since the thread model of Java is declared to be ``medium-weighted'' in some implementations (for example the JDK port to Linux).

Animating Z.

Some basics about a mapping from Z to µZ have been shown, but we have not discussed the intrinsic details, which are out of the scope of this paper. In reality, a mapping of full Z has to convert axioms to definitions where possible, e.g. eliminate quantifiers in axioms of the kind $\forall x:X @ f(x) = e$, map recursion to µZ's fixed-point operator, and more. The mapping also has to weaken the specification by turning some axioms into assumptions: if a user e.g. declares a function to be ``total'' by using Z's total function arrow, $f: A \fun B$, this assertion cannot be computed if f's definition is non-finite, and need therefore be converted into an assumption. All of this has been implemented in the ZAP tool [4], and should port to the new design of the computation model.

There are several other approaches for the animation of Z. Executing the ``imperative'' part of Z is provided by the ZANS tool [9], where imperative means the execution of Z's specification style for sequential systems using state transition schemas. A translation to Haskell is described in [3], where monads are used for dealing with the sequential specification style, but no logic resolution is employed. Translations to Prolog are described e.g. in [20]. The approach presented in this paper goes beyond all these, since it allows for the combination of the functional and logic aspects of Z in a higher-order setting - getting the sequential specification style as a trade-off. Related to our work is the translation of Z to Mercury [21]: however, in this approach the effective power of execution is restricted in comparison to ours, since the flow of control has to be determined statically.