zbMATH — the first resource for mathematics

The Z Notation. A Reference Manual. (English) Zbl 0777.68003
Prentice Hall International Series in Computer Science. New York etc.: Prentice Hall. XI, 155 p. (1989).
A formal specification is a single, reliable reference point that promotes common understanding for customers, implementors, testers, and documenters of a system. The \(Z\) notation is one of the most commonly used for this purpose. It is very powerful and is based on simple mathematical concepts. It has reasonable facilities for structuring sizable specifications and therefore for understanding them. It is used by various international standardization documents, notably in Open Distributed Processing (ODP). The book serves as the acknowledged reference about \(Z\).
The book has been, in the author’s words, “written with everyday needs of readers and writers of \(Z\) specifications in mind”. The author clearly achieves his goal. The book is pragmatic and does not teat “foundational” issues. There are no formal definitions of the notation – “informal but rigorous style of presentation” is used as more accessible to \(Z\) users. (For example, the Laws in the mathematical toolkit are not proven.) Some level of mathematical (and programming) maturity (e.g., naive set theory and predicate calculus) is a prerequisite. Although the book starts with a short and very useful tutorial, it is not recommended as the very first text about \(Z\): other ones (like B. Potter, J. Sinclair and D. Till [An introduction to formal specification and Z. New York, Prentice-Hall (1991; Zbl 0745.68028)]) are more appropriate for this purpose. The goal of the book is to serve as a reference about the \(Z\) notation. Of course, just as understanding programming constructs does not automatically lead to good programs, understanding \(Z\) constructs does not automatically lead to good specifications.
The author used maintaining a balance between comprehensiveness and simplicity as a criteria for selecting the language features to be presented. A “standard set of notations” is proposed. Some important more complicated constructs are almost not dealt with: e.g., promotion is just referred to on p. 11 (8 lines) in discussing modularization. Certain concepts (like bindings, \(\lambda\), and \(\mu)\) may be considered by some as better exposed elsewhere. A more advanced book by the same author, [J. M. Spivey, Understanding Z, Cambridge University Press (1988; Zbl 0658.68005)], includes some design considerations that explain choices made by the creators of \(Z\).
Naturally, the emphasis is on abstraction – what instead of on how – as it should be for a specification. And, in addition, the emphasis is on precision needed to get rid of “the need to speculate about the meaning of phrases in an imprecisely-worded prose description”. This approach is consistent throughout. It is essential in information management, especially in analysis (information modeling).
The semantics of an operation is specified by its pre- and postconditions. Although the precondition is not presented explicitly in a \(Z\) operation schema, the author introduces this notion at the very beginning an essential for understanding operations. Throughout the book, the author stresses the need to separate concerns. In particular, he contrasts a specification where expressive clarity is of utmost importance with an implementation where ability to be directly represented in a computer is important. The author observes that not all variables have to be represented explicitly in the implementation, although the specification may include important, but derived, components (for readability). The description of the mathematical toolkit serves as a good example: as “the data types it contains are oriented towards mathematical simplicity rather than computer implementation, reasoning ... is made easier”. (The definitions in the mathematical toolkit manual pages are recommended for careful reading.) The author also notes that it is possible and desirable to model the implementation using the same mathematical approach as in specifying the business rules. This helps to clarify the abstract data types (like arrays, p. 13) used in an implementation. The implementation itself is also made clear, thanks to its declarative specification which “describes operations in terms of their function”. Of course, this approach is not new: it dates back to E. W. Dijkstra and C. A. R. Hoare who used it for conventional programming. The \(Z\) notation uses it, in particular, for specifying business rules. In this manner, programming concepts are being reused in formulating specifications. The author provides no formal inference rules for defining theorems about specifications: “The practical usefulness of inference rules seems to depend crucially on making them interact smoothly, and we have not yet gained enough experience to do this.” However, some simple theorems about the correctness of implementations are proven.
Chapter 5 of the book is a concise and lucid explanation of how a \(Z\) specification viewed as a mathematical theory may also be used to describe computer programs. In particular, the author explains why and how “loose” specifications facilitate the level of abstraction appropriate for the problem at hand.
The author recommends a \(Z\) specification to consist of interleaved passages of formal text and informal prose explanation. In particular, for every \(Z\) definition in the mathematical toolkit, its translation into stylized English is also provided. This approach is highly recommended and actually used in real-life large \(Z\) specifications, substantially enhancing their readability. As another example, the \(Z\) specification of the ODP Trader presented in this manner is readable by people with a quite restricted exposure to \(Z\) syntax.
The book contains no reference list, but the people on whose ideas the work was based are listed on the title page. The book has some typos (e.g., in the second to the last predicate on p. 37) which have been taken care of in the second edition [Spivey, The Z. Notation: A Reference Manual (2nd. ed.). Hemel Hempstead, UK: Prentice Hall (1992)]. More importantly, in the second edition the author made some additions (like renaming of schema components, let, schema piping, etc.) have remedied some defects and improved the exposition “in many small ways” (in particular, “situation” has been replaced with “binding”).
The book is highly recommended to a wide variety of readers, from computing scientists to specifier and programmers.

68-00 General reference works (handbooks, dictionaries, bibliographies, etc.) pertaining to computer science
68N01 General topics in the theory of software
68Q60 Specification and verification (program logics, model checking, etc.)
03B10 Classical first-order logic
68Q45 Formal languages and automata
68Q55 Semantics in the theory of computing