Summary
Spivey’s reference manual defines the Z notation — a formal specification language standardized as ISO 13568. Z describes systems as states, invariants that constrain them, and operations that transition between them. The manual covers the mathematical toolkit (sets, relations, functions, sequences), schema calculus for composing specifications, and the type system that makes Z amenable to mechanical checking.
What it means for our work
This is the notation Z Spec wraps. Every /z check and /z test invocation ultimately relies on the semantics Spivey defined here. The manual also informed our decision to use fuzz (Spivey’s own type-checker) as the primary checking backend — it implements the notation exactly as specified, with no extensions or deviations. When we generate Z specifications from code via code2model, the output conforms to this reference.