1. Introduction

The automatic evaluation of test-data for safety-critical embedded systems is an interesting application which can help to bring declarative language implementation techniques into industrial practice. Some figures report about more then 50% of development costs in this application area which goes into testing. A setting for test-case evaluation which can improve this situation is as follows: given a requirements specification by an executable prototype, some input data describing a test-case, and the output data of a run of the system's implementation on the given input, by executing the specification we check whether the implementation meets its requirements. On the first sight, this goal seems to be simple, since input and output data are fixed. Yet, a real-world specification of a complex system may contain a lot of ``hidden'' data, which is used to describe the observable behavior. Thus the problem scales up to finding the solution(s) to a (sequence of) partial data bindings.

In the application-oriented research project ESPRESS¹, which is concerned with methods and tools for the development of embedded systems, the set-based specification language Z [16] is used for requirements specification, in combination with other notations such as Statecharts which are incorporated by a shallow encoding into Z [2]. Performing test-case evaluation in this setting requires a computation model for Z and its implementation.

In this paper, we report on some results of the efforts on implementing such a framework. The main theme of the paper is the presentation of the µZ calculus (Sect. 2), and the definition of a computation model for it (Sect. 3). The µZ calculus is a pure expression language with only a few constructs which abstracts from the diversity of Z. Since it can embed the full Z language - the simple-typed $\lambda$-calculus, set calculus, predicate calculus, and schema calculus - computation in µZ can indeed not be complete: but a computation model and implementation by an abstract machine can be provided which is comparable to that of functional logic paradigms (e.g. [5]).

The work presented in this paper constitutes the plan for refining an existing implementation of Z, the so-called ZAP compiler, which is part of the ESPRESS tool environment ZETA[4]. Within ZAP, Z is reduced to µZ, and µZ is compiled to Java, using a functional (deterministic) approach with concurrent constraint resolution for dealing with the problem of undirected equality and ``parallel and''. Several case studies performed together with industry partners demonstrated the feasibility of the principal approach, but also clearly showed that (1) deterministic computation for test-data evaluation is a serious restriction, since it constraints the way of how requirement specifications can be formulated in Z significantly (2) Java is a high performance penalty as the target for compiling a declarative language. Thus this work sets out to define an enhanced computation model for µZ, incorporating indeterministic logic principles, and designing an abstract machine which can be efficiently implemented in C++.

Using a set-based calculus to view computation might raise the impression that set-based resolution techniques shall be incorporated, such as set-unification [17], or subset clauses [12]. Yet, this is not the case: µZ and its implementation rather provides an alternative and unorthodox view on functional logic computation, where sets provide the framework for a smooth integration of these two concepts.