Home › Multilingual Archive Index › Z notation

Z notation

The Z notation (formally pronounced /zɛd/), named after Zermelo-Fränkel set theory, is a formal specification language used for describing and modeling computing systems. It is targeted at the clear specification of computer programs and the formulation of proofs about the intended program behavior.

Z was originally proposed by Jean-Raymond Abrial in 1977 with the help of Steve Schuman and Bertrand Meyer ^[1]. It was developed further at the Programming Research Group at Oxford University, where Abrial worked in the early eighties.

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 catalog (called the mathematical toolkit) of commonly used mathematical functions and predicates.

Although Z notation uses many non-ASCII symbols, the specification includes suggestions for rendering the Z notation symbols in ASCII and in LaTeX. A Z ttf font is also available for free download.

Standards

The ISO completed a Z standardization effort in 2002. This standard can be obtained directly from ISO.^[2]

See also

• B-Method
• Z++
• Object-Z
• Z User Group (ZUG)
• Community Z Tools (CZT) project
• Formal methods

References

1. ^ Jean-Raymond Abrial, Stephen A. Schuman and Bertrand Meyer: A Specification Language, in On the Construction of Programs, Cambridge University Press, eds. A. M. Macnaghten and R. M. McKeag, 1980 (describes early version of the language). ISBN 0-521-23090-X
2. ^ (2002-07-01) Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics (1 MB PDF), ISO/IEC 13568:2002, 196 pages. 

Further reading

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

External links

• The World Wide Web Virtual Library: The Z notation, by Jonathan Bowen
• Community Z Tools (CZT) project
• Specification proposals by Ian Toyn
• ZETA open-source system for development software specifications in Z
• HOL-Z open-source proof environment for Z in Isabelle/HOL
• Mike Spivey's Fuzz Type-Checker for Z
• Z/Eves — A proof checker for the Z notation (German site but all manuals in English)