Annotated links to sources (by others, not me) that document significant moments in the history of the Z notation. They trace the growth, then decline, of interest in Z.
More pages about Z.
This thorough report surveys the work of the Z tool-making community at the time of its greatest expansion. It explains some difficult technical issues in Z better than any other source I know.
I think this report also shows why interest in Z started to decline at about this time. Martin finds a proliferation of incompatible proof tools of only prototype quality, whose convenience and power were limited by technical and foundational issues. This seemed to reveal problems with Z itself, which might have discouraged its adoption. How did this situation arise? Here is how I remember it:
Z was supposed to be easy. One of its creators said, "We just wanted to use simple mathematics to describe software". Z began as nothing more than some conventions for writing formulas about logic and sets, which seemed to be straightforward and uncontroversial.
It is the mathematics that makes Z formal. It promises to make the power of mathematics available for analyzing specifications, in a way that is not possible with prose. Using mathematics for analyzing and writing computer programs is called formal methods.
For some, Z was not just a notation, it was the vanguard innovation in a movement to reform computer programming into a more rigorous, science-based discipline. They hoped that formal specifications might play a similar role in programming that mathematical models play in science and engineering.
The defining innovation in Z is a construct called the schema, which attaches a name to a collection of formulas. An author can use this name in subsequent formulas as if it were an ordinary identifier. There is a schema calculus where all of the usual logical operators can be applied to schema names, with the meanings that intuition would expect. For example, to express that a radiation therapy machine control system meets its safety requirements, one can write TherapyControl => SafeTreatment (pronounced "therapy control implies safe treatment"), where TherapyControl is the schema name applied to many pages of formulas that describe the control system as a collection of state transitions, and SafeTreatment is the schema name applied to many more pages that express the safety requirements as a collection of safe states. This formula says that the operations of the control system can only reach safe states -- never an unsafe state. Here the schema names are used as predicates, but schema names can play any role in a formula -- as declarations, expressions, or predicates -- so their interpretation depends on context.
The most visible innovation in Z is its distinctive appearance, quite unlike program code, or anything else in computing. Schemas and other language constructs are written inside specially shaped boxes, while the enclosed formulas can include Greek letters, mathematical symbols, several kinds of arrows, and some new graphic symbols not found in traditional mathematics. Authors and readers might enjoy the appearance -- or have some other reaction -- but the intent is to provide structure, brevity, and visual mnemonics that could make formal specifications easier to grasp.
Authors found that they could use Z schemas to write formal specifications that were not only precise, but also expressive and pursuasive. Z promised to relieve the tedium and pedantry of writing and reading formal specifications. Advocates hoped it might help formal specifications become an accepted part of the software development process.
Some authors were content to regard a Z specification as purely descriptive: precise and well-structured documentation, which could be more helpful for coding the program than a prose description. In this view, the formula TherapyControl => SafeTreatment merely expresses the designer's intent.
Others were more ambitious. They hoped to to prove properties of the Z specification. They would use the methods of logical inference to check whether all the formulas included in TherapyControl really do guarantee all the safety requirements in SafeTreatment. A successful proof should provide strong confidence that the design expressed in the Z specification really does specify a safe therapy machine -- that nothing has been overlooked or written incorrectly. In this view, the main reason for writing a formal specification is to make it possible to perform proofs like this.
Such proofs are usually lengthy, tedious, and error-prone. They consist of long sequences where rules of inference are applied to formulas from (for example) TherapyControl to derive new formulas, until eventually the sequence reaches the formulas in SafeTreatment. The proofs are so tedious that most people would not even consider attempting them.
But there is a technology of theorem prover programs that assist authors writing proofs, which might make the proofs feasible. These programs check every proof step to confirm that the inference rules have been correctly applied. Some provers can even generate some of the tedious proof steps, under the author's direction. A proof that has been checked by one of these programs is considered to be valid, even if it is complicated and difficult to follow.
It seemed to some that the eventual success of the entire Z movement depended on getting a useful theorem prover program for Z. When Z appeared, there were already a number of these theorem prover programs in use, for ordinary logic without schemas. Since Z was "just sets and logic" and a schema just named a collection of ordinary formulas, it seemed that adapting these provers to work with Z specifications should be straightforward. But this turned out to be more difficult than expected.
To be acceptable to Z authors, the prover has to work with schemas, not the underlying formulas. But it was found that, due to various technical issues, especially their context dependence, schemas and their constituents cannot be handled like ordinary logical formulas. Therefore, to adapt an existing prover, it is necessary to translate Z into its native logic, which is difficult to do faithfully. Alternatively, an entirely new prover tailored to Z can be developed from scratch, requiring substantial effort. Both approaches were tried, in many variations. This is the landscape surveyed in Martin's review.
There was a felt need for a standard that would clarify the complications in Z and provide a canonical interpretation for each. The standard should include a semantics that describes exactly what any Z text denoted, as a collection of variable names and their values, after schemas had been eliminated. It should also include a deductive system -- a "logic for Z" -- a collection of inference rules for writing proofs that included schemas.
A Z Committee was formed in 1992 to write a Z standard and get it approved by an international standards organization, the ISO/IEC. A single author had already written The Z Notation: A Reference Manual in 1989, with a second edition in 1992. Usually called the ZRM, it was the de facto standard, but it did not provide a deductive system nor a semantics (although the same author did propose a semantics in another book). Moreover, some Z authors were eager to use schemas even more liberally, in ways not endorsed by the ZRM. The Z Committee (which did not include the author of the ZRM) chose not to simply codify the existing ZRM in the format required by ISO, but to go further -- to provide a deductive system and semantics, and accommodate the new styles for using schemas.
The Z Committee had, in effect, undertaken a research project. They tried to innovate and standardize at the same time. They worked on through the 1990s, producing a series of inconclusive draft standards. The deductive system proposed in one draft was found to be inconsistent -- that is, erroneous -- and the committee eventually decided not to include one. They advised that any deductive system would conform to the standard if it was consistent with the semantics they defined -- but they declined to provide an example. After several years, one frustrated tool builder wrote, "The Z committee has missed the boat." The standard was finally adopted in 2002 -- too late, some felt.
Meanwhile, lacking guidance from a standard, each group -- there were many -- tried to cope with the difficulties in its own way. No consensus solution emerged. The community was fragmented. The proof tools were all incompatible. Each tool used proof scripts that were not usable by any other. Even the kinds of properties that could be proved varied from one tool to another. This is the situation described in Martin's report.
Several authors (outside the Z Committee) eventually did propose different deductive systems that appeared to be sound, but by then interest in Z was waning. The revelations that Z was not so simple, the long-delayed standard, and the proliferation of incompatible tools, may have contributed to its decline. If you are designing a system, you don't want your notation and tools to be somebody's idea of a research problem. Also, the need to use a typesetting program to write the boxes and graphic symbols was felt by many to be a nuisance.
The most ambitious aspirations of the Z movement were probably doomed to disappointment. The movement viewed formal methods as a Field of Dreams: "Build it and they'll come." But most software developers were never going to write or use formal specifications in any notation, because it seems like extra work, and they know that many successful projects don't use them. Since the 1990s, the emphasis in the mainstream of software development has moved even more toward getting quickly to code, and then trying to solve all the problems there. So the travails I relate here may not have been decisive in Z's decline.
Getting developers to use a prover was even more unlikely. It is not much like programming; it is an esoteric and difficult skill, mastered by few. Since the 1980s, an alternative kind of analysis tool called a model checker has emerged, which (in effect) performs exhaustive testing (of specifications, not programs) over limited domains. Using a model checker is much easier for developers -- it is more like running a program than proving a theorem. Model checkers attracted little interest in the Z community, but turned out to be more effective than provers for detecting most errors.
Z is almost forgotten today, but there are niches where formal specifications are still used -- where some combination of novelty, difficulty, and the cost of errors convinces developers that their usual intuitive approach is not adequate. But instead of Z, two other notations that appeared in the 1990s were the most written about in the 2010s. Both Alloy and TLA+ are influenced by Z. But they don't look like Z; they have dispensed with the boxes and graphic symbols, so they can be typed and edited in the same way as program code. Both are the creations of a single author who remains the leader of their community, provides focus, and avoids fragmentation. Both notations are simpler than Z -- no schemas -- and were developed along with their tool sets, which both feature a model checker. TLA+ also has a prover, but its model checker is used more often.
Z was most popular in the 1980s and 1990s, an age of innocence when people thought Z was easy and there was no standard -- at first, not even the ZRM. The Z movement was sparked by the early book Specification Case Studies (1987) which merely presented some pursuasive examples with minimal explanation. Readers liked it, thought they understood it, formed their own intuitions, and began writing Z specifications that avoided -- or ignored -- the complications that detained later tool builders and standards writers. For many of these authors, the attractions of Z were clarity, brevity, expressiveness, and even visual impact -- not the (mostly unrealized) potential for proving. A later, more critical author called their style vernacular Z. But ambitious systems were specified in this style, and some even got built -- without proof. The same features that made Z proofs difficult also encouraged people to write Z specifications in the first place.
Assembling a Prehistory for Formal Methods: A Personal View by Thomas Haigh (2019). The author begins by recalling the heyday of the formal methods movement. VDM was a rival notation to Z.
"My personal history with formal methods began, and ended, at the University of Manchester where I began my undergraduate studies in computer science in 1991 ... At that time the introductory programming course ... taught programming in Pascal, a common choice at that time ... and specification writing in VDM which was rather less common. ... The idea was presumably that this would raise a generation of computer scientists who thought this was a normal way of working ... a world where nobody would dream of starting to code a Nim program without first coming up with a solid formal specification complete with pre- and post-conditions. ..."
Some of the sources mentioned above. Most links lead to full text PDFs, but the links for Understanding Z and Innovations in ... Standard Z only show excerpts.
Specification Case Studies, edited by Ian Hayes, 2nd edition (1993). The 1987 edition was the first book about Z and helped to popularize it.
Towards a Formal Semantics for the Z Notation by Mike Spivey (1984). Sketches a formal semantics for Z, expressed in Z itself.
Understanding Z: A Specification Language and its Formal Semantics by J. M. Spivey (1989). Book made by developing the ideas in the preceding report. At the publisher's web site, Look Inside shows some short excerpts only.
The Z Notation: A Reference Manual by Mike Spivey, 2nd edition (1992), first edition 1989. The ZRM, the de facto standard for many years. Still highly recommended.
Innovations in the Notation of Standard Z by Ian Toyn (1998). This paper by a member of the Z Committee describes differences between the draft Z Standard and the ZRM. The linked web page only shows the first two pages of the paper.
Z formal specification notation — Syntax, type system and semantics (2002). The ISO/IEC Z Standard. The most accessible part is the Tutorial, Annex D, p. 158 in the standard, but go to p. 164 in the PDF. At this web site, to save you the trouble of digging it out of the ISO web site and extracting it from the .zip archive.
Z logic and its consequences by Martin C. Henson, Steve Reeves, and Jonathan P. Bowen (2003). A deductive system for Z, presented and explained.
Revised Nov 2022