We present a computation model for Z, which is based on a reduction to a small calculus, called, and on concurrent constraint resolution techniques applied for computing in this calculus. The power of the model is comparable to that of functional logic languages, and combines the strength of higher-order functional computation with logic computation. The model is implemented as part of the ZETA system, where it is used for executing Z specifications for the purpose of test-data evaluation and prototyping.
展开▼
