Powered by
Share this page on
Article provided by Wikipedia

An example of a "formal specification (in Spanish) using the Z notation.

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.

Usage and notation[edit]

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:


See also[edit]


  1. ^ "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 
  2. ^ "Meyer, Bertrand; Baudoin, Claude (1980), Méthodes de programmation (in French), Eyrolles 
  3. ^ 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).
  4. ^ Hoogeboom, Hendrik Jan. "Formal Methods in Software Engineering" (PDF). The Netherland: "University of Leiden. Retrieved 14 April 2017. 
  5. ^ 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.
  6. ^ 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.

Further reading[edit]

External links[edit]

) ) WikipediaAudio is not affiliated with Wikipedia or the WikiMedia Foundation.