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.

Although 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.

"ISO completed a Z standardization effort in 2002. This standard^{[5]} and a technical corrigendum^{[6]} are available from ISO for free:

- the standard is publicly available
^{[5]}from the ISO ITTF site free of charge and, separately, available for purchase^{[5]}from the ISO site; - the technical corrigendum is available
^{[6]}from the ISO site free of charge.

*Community Z Tools (CZT)*(project), Source forge*Z Word tools*(project), Source forge for developing and checking Z specifications in "Microsoft Word- Fuzz, a type-checker for Z
- Z/Eves — A proof checker for the Z notation (German site but all manuals in English)
- Z/EVES Documentation, papers, and manuals on Z/EVES
- ZETA open-source system for development software specifications in Z
- HOL-Z open-source proof environment for Z in Isabelle/HOL
- CADiZ, a set of free software tools that assist use of Z notation
- ProofPower, a suite of "open-source tools supporting specification and proof in "HOL and in the Z notation
- z-vimes Z-Vimes: type checker and (eventually) theorem prover for the Z specification language
- ProB is an animator and model checker originally written for the "B-Method that provides also support for Z specifications ("ProZ") that conform to the Fuzz type checker

- "Z User Group (ZUG)
- "Community Z Tools (CZT) project
- Other "formal methods (and languages using "formal specifications):
- "Z++ and "Object-Z : object extensions for the Z notation
- Abstract Machine Notation (AMN), used in "B-Method
- "Alloy, a specification language inspired by Z notation and implementing the principles of "Object Constraint Language (OCL).

- "Fastest is a "model-based testing tool for the Z notation.

**^**"Abrial, Jean-Raymond (1974), "Data Semantics", in Klimbie, J. W.; Koffeman, K. L.,*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.,*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.- ^
^{a}^{b}^{c}"ISO/IEC 13568:2002".*Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics*("Zipped "PDF). ISO. 2002-07-01. 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. 2007-07-15. 12 pp.

- "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. "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.

- Toyn, Ian,
*Z Specification proposals*, "UK: York. *WSDL 2.0*, W3C, a specification containing Z notation assertions and explanation