Z notation

Z notation (pronounced “zed”) is a formal specification language for describing and reasoning about computer systems with mathematics. It is not a programming language: nothing written in Z runs. A Z specification says what a system must do, precisely enough that you can check it for consistency, prove properties about it, and later show that a design or program meets it. Z is built on typed set theory and first-order predicate logic. It adds one distinctive structuring device, the schema, a named box of declarations and constraints. Through the 1980s and 1990s, Z was one of the most widely taught and most industrially tested formal methods. It also led directly to its creator’s later work on the B-Method and Event-B.

History & Origins

Grenoble and EDF (1970s)

Jean-Raymond Abrial’s path to Z started with data. In Grenoble in the early 1970s he worked on the Socrate database system, and in 1974 he published Data Semantics at an IFIP working conference. That paper used a set-based way of describing the meaning of data structures, and it anticipated much of his later work.

The first documents that name the language come from 1977. That year Abrial produced a Manuel du langage Z and a series of numbered internal notes, including a study of a small business application specified in Z, while working with the research division (DER) of Électricité de France. Bertrand Meyer, then at EDF, and Steve Schuman worked with him. The three co-authored “A Specification Language”, published in 1980 in the Cambridge University Press volume On the Construction of Programs, one of the earliest published accounts of the notation.

Oxford and the Programming Research Group (1979 onward)

Tony Hoare invited Abrial to Oxford’s Programming Research Group (PRG), and he arrived in 1979 (some accounts give 1980). There, working with Bernard Sufrin, Ib Holm Sørensen, Carroll Morgan and others, Z took something close to its lasting form. Abrial’s 1980 PRG reports, The Specification Language Z: Basic Library and The Specification Language Z: Syntax and Semantics, circulated widely. Carroll Morgan was another key discussion partner, and the schema boxes that let large specifications be built from smaller pieces took shape during this period. Ian Hayes, who joined the Oxford–IBM project in January 1983, arrived around the time the “schema calculus” of operators for combining schemas was being worked out.

The Oxford group also had a practical problem to work on. Meetings between Hursley managers and Hoare in mid-1981 led to a contract between IBM Hursley and Oxford University by the end of that year, with Sørensen and Tim Clement working from the Oxford end. The project’s goal was to specify parts of IBM’s Customer Information Control System in Z. By 1988 CICS consisted of well over half a million lines of code, and accounts of the project say that the challenge of describing such a system influenced how the notation developed.

Why “Z”?

Abrial has reportedly joked that Z is so named “because it is the ultimate language”. The name is also often linked to Ernst Zermelo, whose axiomatic set theory (Zermelo–Fraenkel set theory) is the mathematical foundation Z builds on.

Design Philosophy

Z rests on a few firm beliefs:

• Specification is not programming. Z was deliberately not made executable. Freed from execution, a specification can say what should hold without committing to how it is achieved. It can use infinite sets, non-constructive definitions and plain logical conditions.
• Ordinary mathematics is enough. Instead of inventing a new formalism, Z uses the set theory and logic that any mathematically trained engineer already knows, plus a standard mathematical toolkit of relations, functions and sequences, which is itself defined in Z.
• Types keep the mathematics sound. Every expression in Z has a type. Typing rules out the classic paradoxes of naive set theory and lets tools catch many mistakes mechanically.
• Structure makes it scale. Mathematics alone becomes unreadable for large systems. Schemas give specifications a modular structure: you can name, include, combine and reuse them.
• Formal text and prose go together. A good Z document mixes formal paragraphs with plain-language explanation. The mathematics removes ambiguity, and the prose explains what it means.

Key Features

Schemas

The schema is Z’s signature construct. A schema has a declaration part, which introduces variables and their types, and a predicate part, which states the constraints that must hold between them. Schemas describe both the state of a system and the operations that change it.

The best-known teaching example is the “birthday book” from Spivey’s reference manual. The state is a set of known names and a partial function from names to dates:

1
2
3
4
5
6

┌─ BirthdayBook ─────────────────────
│ known    : ℙ NAME
│ birthday : NAME ⇸ DATE
├────────────────────────────────────
│ known = dom birthday
└────────────────────────────────────

An operation that adds a birthday declares that it changes the state (Δ BirthdayBook), takes two inputs (by convention, names ending in ?), and relates the state before the operation (unprimed) to the state after it (primed):

1
2
3
4
5
6
7
8

┌─ AddBirthday ──────────────────────
│ Δ BirthdayBook
│ name? : NAME
│ date? : DATE
├────────────────────────────────────
│ name? ∉ known
│ birthday′ = birthday ∪ {name? ↦ date?}
└────────────────────────────────────

Schema Calculus

Schemas can be combined with operators modeled on logic, including conjunction, disjunction, negation, hiding and sequential composition. That lets a specifier write the normal case and the error cases separately and then combine them, for example RAddBirthday ≙ (AddBirthday ∧ Success) ∨ AlreadyKnown.

Conventions

Mathematical Toolkit

Z has a large standard library of notation: power sets (ℙ), relations (↔), total and partial functions (→, ⇸), injections, domain and range restriction, relational image, override (⊕), sequences and bags. All of it is defined inside Z itself.

Refinement and Proof

Z specifications can be data-refined toward more concrete designs, with proof obligations that show each concrete operation correctly implements its abstract counterpart. This is where Z has been most rigorously exercised in industry, with Z-level proofs done by hand or with tools.

Markup

Because Z uses many mathematical symbols, it is usually written in a LaTeX markup and typeset. The same birthday-book state schema in the LaTeX style used by Spivey’s fuzz type checker looks like this:

1
2
3
4
5
6

\begin{schema}{BirthdayBook}
  known : \power NAME \\
  birthday : NAME \pfun DATE
\where
  known = \dom birthday
\end{schema}

The ISO standard defines both LaTeX and e-mail (ASCII) markups, and Unicode includes characters for Z’s symbols.

Evolution

From Oxford Notation to De Facto Standard

For most of the 1980s, Z was defined by a changing set of Oxford reports, case studies and teaching materials. One history of the period says frustration at the lack of a stable reference in 1981 led PRG researchers to assemble a spoof “reference document”. Ian Hayes’s Specification Case Studies (1987) was the first book on Z. Mike Spivey’s Understanding Z (1988) gave the language a formal semantics, and his The Z Notation: A Reference Manual (1989; second edition 1992) became the de facto standard that most tools and textbooks followed. Spivey also wrote the first tool that type-checked Z specifications, and his fuzz type checker is still available.

The Z User Community

The first Z User Meeting was held at Rewley House, Oxford, in 1985. Meetings continued at Oxford, York and London. The Z User Group was formally set up on 14 December 1992, during ZUM'92 in London. The meeting became the International Conference of Z Users in 1995, when it was held outside the UK for the first time, in Limerick. In 2000 it merged with the B community’s conference to form ZB. From 2008 it grew into ABZ, which added Abstract State Machines and later Alloy (2010), VDM (2012) and TLA (2014). ABZ still runs; its 2026 edition in Tokyo still listed Z among its topics.

Extensions and Descendants

• Object-Z (University of Queensland, first described in a 1991 technical report) adds classes and object-oriented structuring to Z.
• The B-Method. Abrial grew dissatisfied with how little help Z gave for refining a specification step by step into code. He went on to create B, which combines specification, refinement and machine-checked proof, followed by Event-B.
• Alloy. Daniel Jackson’s Alloy, a lightweight relational modeling language with automatic analysis, is widely described as inspired by Z.

ISO Standardization

After years of committee work, ISO/IEC 13568:2002, Z formal specification notation: Syntax, type system and semantics, was published in July 2002. It was prepared by ISO/IEC JTC 1/SC 22 and covers syntax, the type system, formal semantics, the mathematical toolkit, and the LaTeX and e-mail markups. A Technical Corrigendum followed in 2007. ISO has made the standard freely available through its Publicly Available Standards service.

Industrial Use and Evidence

Z is unusual among formal methods in having several large, documented industrial case studies. The claims these projects make come with important caveats:

• IBM CICS. Houston and King’s 1991 report on the Oxford–IBM work described improved quality and earlier error detection in CICS/ESA V3.1. IBM estimated about a 9% reduction in the total development cost of that release. In the first eight months after release, customers reported noticeably fewer problems in Z-specified code than in other code. The authors stressed that this was not a controlled experiment: the same code was never also developed without Z. A 2011 reunion of project members found little trace of Z still being used at Hursley.
• SHOLIS. King, Hammond, Chapman and Pryor (IEEE Transactions on Software Engineering, 2000) report roughly 150 proofs covering about 500 pages at the Z level, and about 9,000 verification conditions at the SPARK code level. On their project, Z-level proof found faults more efficiently than even the most efficient testing phase.
• Mondex. Z models, refinement and proofs supported ITSEC E6 certification of the Mondex electronic purse. About a decade later the work was revived as a pilot project for the Verified Software Grand Challenge, with mechanized re-proofs in tools such as Z/EVES.
• Tokeneer. The NSA-sponsored Tokeneer ID Station was specified in Z and implemented in SPARK Ada. After its public release it became a standard benchmark for other formal methods tools.

Tools

Z was never “compiled”, but a number of tools grew up around it:

• fuzz: Mike Spivey’s LaTeX-based type checker, following the reference manual dialect. Its source is on GitHub.
• Community Z Tools (CZT): an open-source Java framework, proposed in 2001, for parsing, type-checking, printing and animating ISO Standard Z, Object-Z and Circus specifications.
• Z/EVES: a theorem prover for Z, used among other things for the mechanized Mondex proofs.

Current Relevance

Z is best described as dormant but not dead. The notation itself has barely changed since the 2002 ISO standard, the dedicated Z User Meetings have long been absorbed into the broader ABZ conference, and industrial practice has largely moved to tool-centred methods such as B/Event-B, Alloy and TLA+. Some maintenance continues at a low level. The CZT repository received commits in late 2024, Spivey’s fuzz repository was updated in 2025, and ISO still lists the standard as current. Z also appears in formal methods courses and textbooks, and it is often the notation used to teach specification, refinement and proof.

Why It Matters

Z showed that ordinary discrete mathematics, organized with a small amount of structure, could specify real commercial and safety-critical software. Its schema-based style of describing state and operations became a template for later model-based specification languages. The CICS, SHOLIS, Mondex and Tokeneer projects are among the most-cited evidence in debates about whether formal methods pay off in industry. The Oxford work on Z also trained a generation of formal methods researchers, and it led Abrial to the B-Method and Event-B. Those methods carried Z’s ideas into railway signalling, including Paris Métro Line 14. Even the idea that a specification should be precise, abstract and not executable owes much to Z.