Z Mathematical Toolkit

The Z notation provides a rich foundation of mathematical datatypes, including sets, relations, functions, sequences and bags. Since these are frequently used in Z specifications, we implemented one or more SAL library contexts to model each datatype. Each context is parameterised by one or more types, affording reuse of each context to model many different typed constructions, by instantiating the parameters with different types.

Here, we provide copies of the latest SAL library context files used to model the Z mathematical toolkit. These have been painstakingly developed and tested (using the theorems from the Z reference manual) for soundness. They are periodically revised, when new encodings are discovered that are more efficient. Currently, the SAL encodings fall into two groups: those constructions based on SAL sets, and those constructions based on SAL total functions.

The Set Contexts

We wanted to preserve the style of Z, in which every datatype may ultimately be viewed as a kind of set. There is one main set context and several anciliary contexts that provide additional operations. Cardinality of sets always requires a custom context, optimised for the maximum number of elements in a set — here we give an example for sets with up to five elements. One context provides extra operations on sets-of-sets.

• set.sal — for sets and finite sets
• power.sal — additional operations for powersets
• count5.sal — for counting sets with max 5 elements
• setmax.sal — for computing set maximum, minimum values

The Relation Contexts

Relations are basically sets-of-pairs in Z. All set-like operations on relations are accessed from the set context. The relation context provides additional operations over domain and range sets. Two more contexts deal with relational composition, and computing closures over a homogeneously typed relation. The identity relation may be computed for a subset, or for the whole type.

• relation.sal — for additional operations on relations
• relcompose.sal — for composing two different relations
• relclosure.sal — for computing closures over relations
• relidentity.sal — for computing the identity relation

The Function Contexts

Functions are also sets-of-pairs in Z. However, we use a different SAL encoding, where a (partial) Z function is encoded as a total SAL function, from the domain type to an extended codomain type (with the undefined bottom value). This means that all the set and relation operations are replicated for this new encoding. It is also possible to convert from the SAL function encoding to the set-of-pairs encoding.

• function.sal — for general partial functions
• totalfun.sal — for total functions only
• funcompose.sal — for composing two different functions
• funidentity.sal — for computing the identity function
• funinverse.sal — for asserting the total inverse of an injective function

The Sequence Contexts

Sequences are functions from positive naturals to elements in Z. We use a similar SAL encoding as for (partial) Z functions, with an extended codomain type (including bottom). This datatype was extremely difficult to encode, because of the need to preserve sequence order, after deleting arbitrary elements. For this, we developed a finite recursive encoding of the Z squash() operation that renumbers sequence elements. A separate context distributively concatenates sequence-of-sequence types.

• sequence.sal — for sequences indexed by positive naturals
• seqconcat.sal — for concatenating sequences-of-sequences

The Bag Context

Bags are functions from elements to the positive naturals in Z. We used a similar SAL encoding as for (partial) Z functions, with an extended codomain type (where zero is bottom). This datatype was fairly easy to develop, after the others.

• bag.sal — for bags mapping elements to natural numbers