Z notation
From Wikipedia, the free encyclopedia
The Z notation (universally pronounced zed, named after Zermelo-Fränkel set theory) is a formal specification language used for describing and modelling 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 valuable resource for newcomers interested in learning Z is The Z Notation: a reference manual.
Z notation was used in the IBM CICS project.
Contents |
[edit] Standards
The ISO completed a Z standardization effort in 2002. This standard, entitled Information Technology – Z Formal Specification Notation – Syntax, Type System and Semantics, ISO/IEC 13568:2002, can be obtained directly from ISO.
13568_2002.zip, 1 MB PDF, 196 pages
[edit] See also
- Z++
- Object-Z
- Z User Group (ZUG)
- Community Z Tools (CZT) project
- Formal methods
- B-Method
[edit] Bibliography
- ^ Jean-Raymond Abrial, Stephen A. Schuman and Bertrand Meyer: A Specification Language, in On the Construction of Programs, Cambridge University Press, eds. R. McNaughten and R.C. McKeag, 1980 (describes early version of the language). ISBN 052123090X
[edit] External links
- The Z Notation: a reference manual
- Jonathan Bowen's The Z notation
- Specification proposals by Ian Toyn
- Suppliers of the ISO formal specification
- Community Z Tools (CZT) project
- ZETA open-source system for development software specifications in Z
- Mike Spivey's Fuzz Type-Checker for Z
- Using Z: Specification, Refinement, and Proof (Include a PDF book)