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.
History
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. 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
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.
Standards
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.
Tools
- Community Z Tools (CZT) (project), Source forge.
- Z Word tools (project), Source forge for developing and checking Z specifications in Microsoft Word.
- Spivey, Michael ‘Mike’, Fuzz 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.
See also
- 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.
References
- ↑ 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.
- 1 2 3 "ISO/IEC 13568:2002". Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics (Zipped PDF). ISO. 2002-07-01. 196 pp.
- 1 2 "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
- 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.
External links
- Toyn, Ian, Z Specification proposals, UK: York.
- WSDL 2.0, W3C, a specification containing Z notation assertions and explanation