The Z notation/ˈzɛd/ is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.
History
In 1974, Jean-Raymond Abrial published "Data Semantics".[1] He used a notation that would later be taught in the University of Grenoble until the end of the 1980s. While at EDF (Électricité de France), Abrial wrote internal notes on Z.[citation needed] The Z notation is used in the 1980 book Méthodes de programmation.[2]
Z was originally proposed by Abrial in 1977 with the help of Steve Schuman and Bertrand Meyer.[3] It was developed further at the Programming Research Group at Oxford University, where Abrial worked in the early 1980s, having arrived at Oxford in September 1979.
Abrial has said that Z is so named "Because it is the ultimate language!"[4] although the name "Zermelo" is also associated with the Z notation through its use of Zermelo–Fraenkel set theory.
Usage and notation
Z is based on the standard mathematical notation used in axiomatic set theory, lambda calculus, and first-order predicate logic. All expressions in Z notation are typed, thereby avoiding some of the paradoxes of naive set theory. Z contains a standardized catalogue (called the mathematical toolkit) of commonly used mathematical functions and predicates, defined using Z itself.
Because Z notation (just like the APL language, long before it) uses many non-ASCII symbols, the specification includes suggestions for rendering the Z notation symbols in ASCII and in LaTeX. There are also Unicode encodings for all standard Z symbols.[5]
Standards
ISO completed a Z standardization effort in 2002. This standard[6] and a technical corrigendum[7] are available from ISO free:
the standard is publicly available[6] from the ISO ITTF site free of charge and, separately, available for purchase[6] from the ISO site;
the technical corrigendum is available[7] from the ISO site free of charge.
FDM (Formal Development Methodology), revolving around the Ina Jo and Ina Flo specification sub-languages, quite popular in the 1980s and 1990s
VDM-SL, the main alternative to Z
B-Method, developed by Jean-Raymond Abrial (creator of Z notation)
Z++ and Object-Z : object extensions for the Z notation
Alloy, a specification language inspired by Z notation and implementing the principles of Object Constraint Language (OCL).
Verus, a proprietary tool built by Compion, Champaign, Illinois (later purchased by Motorola), for use in the multi-level secure UNIX project pioneered by its Addamax division.
Fastest is a model-based testing tool for the Z notation.
References
^Abrial, Jean-Raymond (1974), "Data Semantics", in Klimbie, J. W.; Koffeman, K. L. (eds.), Proceedings of the IFIP Working Conference on Data Base Management, North-Holland, pp. 1–59
^Meyer, Bertrand; Baudoin, Claude (1980), Méthodes de programmation (in French), Eyrolles
^Abrial, Jean-Raymond; Schuman, Stephen A; Meyer, Bertrand (1980), "A Specification Language", in Macnaghten, A. M.; McKeag, R. M. (eds.), On the Construction of Programs, Cambridge University Press, ISBN 0-521-23090-X (describes early version of the language).
4:45
