KNOWPIA
WELCOME TO KNOWPIA

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.

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.

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]}

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.

In 1992, “Her Majesty the Queen [was] graciously pleased to approve the Prime Minister’s recommendation that The Queen’s Award for Technological Achievement should be conferred this year upon Oxford University Computing Laboratory. Oxford University Computing Laboratory [gained] the Award jointly with IBM United Kingdom Laboratories Limited for the development of a programming method based on elementary set theory and logic known as the **Z notation**, and its application in the IBM Customer Information Control System (CICS) product.”^{[8]}

- Z User Group (ZUG)
- Community Z Tools (CZT) project
- Other formal methods (and languages using formal specifications):
- 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.

**^**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).**^**Hoogeboom, Hendrik Jan. "Formal Methods in Software Engineering" (PDF). The Netherland: University of Leiden. Retrieved 14 April 2017.**^**Korpela, Jukka K. "Unicode Explained: Internationalize Documents, Programs, and Web Sites".*unicode-search.net*. Retrieved 24 March 2020.- ^
^{a}^{b}^{c}"ISO/IEC 13568:2002".*Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics*(Zipped PDF). ISO. 1 July 2002. 196 pp. - ^
^{a}^{b}"ISO/IEC 13568:2002/Cor.1:2007".*Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics — Technical corrigendum 1*(PDF). ISO. 15 July 2007. 12 pp. **^**"The Queen's Award for Technological Achievement 1992".*Oxford University Computing Laboratory*. Archived from the original on 22 March 2012. Retrieved 17 October 2021.

- Spivey, John Michael (1992).
*The Z Notation: A reference manual*. International Series in Computer Science (2nd ed.). Prentice Hall. - Davies, Jim; Woodcock, Jim (1996).
*Using Z: Specification, Refinement and Proof*. International Series in Computer Science. Prentice Hall. ISBN 0-13-948472-8. - Bowen, Jonathan (1996).
*Formal Specification and Documentation using Z: A Case Study Approach*. International Thomson Computer Press, International Thomson Publishing. ISBN 1-85032-230-9. - Jacky, Jonathan (1997).
*The Way of Z: Practical Programming with Formal Methods*. Cambridge University Press. ISBN 0-521-55976-6.