The Z notation /ˈzɛd/ is a formal specification language used for describing and modelling computing systems. [1] 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". [2] 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), working with Bertrand Meyer, Abrial also worked on developing Z. [3] The Z notation is used in the 1980 book Méthodes de programmation. [4]
Z was originally proposed by Abrial in 1977 with the help of Steve Schuman and Bertrand Meyer. [5] 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!" [6] although the name " Zermelo" is also associated with the Z notation through its use of Zermelo–Fraenkel set theory.
In 1992, the Z User Group (ZUG) was established to oversee activities concerning the Z notation, especially meetings and conferences. [7]
Usage and notation
Z is based on the standard mathematical notation used in axiomatic set theory, lambda calculus, and first-order predicate logic. [8] 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. It is augmented with Z schema boxes, which can be combined using their own operators, based on standard logical operators, and also by including schemas within other schemas. This allows Z specifications to be built up into large specifications in a convenient manner.
Because 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. [9]
Standards
ISO completed a Z standardization effort in 2002. This standard [10] and a technical corrigendum [11] are available from ISO free:
- the standard is publicly available [10] from the ISO ITTF site free of charge and, separately, available for purchase [10] from the ISO site;
- the technical corrigendum is available [11] from the ISO site free of charge.
Award
In 1992, Oxford University Computing Laboratory was awarded The Queen's Award for Technological Achievement for their joint development with IBM of Z notation. [12]
See also
- Z User Group (ZUG)
- Community Z Tools (CZT) project
- Other
formal methods (and languages using
formal specifications):
- VDM-SL, the main alternative to Z
- B-Method, developed by Jean-Raymond Abrial (creator of Z notation)
- Z++ and Object-Z, object extensions for the Z notation
- Alloy, a specification language inspired by Z notation and implementing the principles of Object Constraint Language (OCL).
- Verus, a proprietary tool built by Compion, Champaign, Illinois (later purchased by Motorola), for use in the multi-level secure UNIX project pioneered by its Addamax division.
- Fastest, a model-based testing tool for the Z notation.
- Unified Modeling Language, a software system design modeling tool by Object Management Group
References
- ^ Bowen, Jonathan P. (2016). "The Z Notation: Whence the Cause and Whither the Course?" (PDF). Engineering Trustworthy Software Systems. Lecture Notes in Computer Science. Vol. 9506. Springer. pp. 103–151. doi: 10.1007/978-3-319-29628-9_3. ISBN 978-3-319-29627-2.
- ^ Abrial, Jean-Raymond (1974), "Data Semantics", in Klimbie, J. W.; Koffeman, K. L. (eds.), Proceedings of the IFIP Working Conference on Data Base Management, North-Holland, pp. 1–59
-
^
Hoare, Tony (2010).
Greetings to Bertrand on the Occasion of his Sixtieth Birthday (PDF).
Springer. p. 183.
ISBN
978-3-642-15187-3.
{{ cite book}}:|work=ignored ( help) - ^ 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. (eds.), 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.
- ^ Bowen, Jonathan (July 2022). "The Z User Group: Thirty Years After" (PDF). FACS FACTS. No. 2022–2. BCS-FACS. pp. 50–56. Retrieved 3 August 2022.
- ^ Spivey, J. Michael (1992). The Z Notation: A Reference Manual. International Series in Computer Science (2nd ed.). Hemel Hempstead: Prentice Hall. ISBN 978-0139785290.
- ^ Korpela, Jukka K. "Unicode Explained: Internationalize Documents, Programs, and Web Sites". unicode-search.net. Retrieved 24 March 2020.
- ^ a b c "ISO/IEC 13568:2002". Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics ( Zipped PDF). ISO. 1 July 2002. 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. 15 July 2007. 12 pp.
- ^ "The Queen's Award for Technological Achievement 1992". Oxford University Computing Laboratory. Archived from the original on 2 December 2008. Retrieved 17 October 2021.
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, International Thomson Publishing. 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.
- Ince, D C (1993). An Introduction to Discrete Mathematics, Formal System Specification, and Z. Oxford University Press. ISBN 9780198538370.
The Z notation /ˈzɛd/ is a formal specification language used for describing and modelling computing systems. [1] 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". [2] 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), working with Bertrand Meyer, Abrial also worked on developing Z. [3] The Z notation is used in the 1980 book Méthodes de programmation. [4]
Z was originally proposed by Abrial in 1977 with the help of Steve Schuman and Bertrand Meyer. [5] 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!" [6] although the name " Zermelo" is also associated with the Z notation through its use of Zermelo–Fraenkel set theory.
In 1992, the Z User Group (ZUG) was established to oversee activities concerning the Z notation, especially meetings and conferences. [7]
Usage and notation
Z is based on the standard mathematical notation used in axiomatic set theory, lambda calculus, and first-order predicate logic. [8] 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. It is augmented with Z schema boxes, which can be combined using their own operators, based on standard logical operators, and also by including schemas within other schemas. This allows Z specifications to be built up into large specifications in a convenient manner.
Because 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. [9]
Standards
ISO completed a Z standardization effort in 2002. This standard [10] and a technical corrigendum [11] are available from ISO free:
- the standard is publicly available [10] from the ISO ITTF site free of charge and, separately, available for purchase [10] from the ISO site;
- the technical corrigendum is available [11] from the ISO site free of charge.
Award
In 1992, Oxford University Computing Laboratory was awarded The Queen's Award for Technological Achievement for their joint development with IBM of Z notation. [12]
See also
- Z User Group (ZUG)
- Community Z Tools (CZT) project
- Other
formal methods (and languages using
formal specifications):
- VDM-SL, the main alternative to Z
- B-Method, developed by Jean-Raymond Abrial (creator of Z notation)
- Z++ and Object-Z, object extensions for the Z notation
- Alloy, a specification language inspired by Z notation and implementing the principles of Object Constraint Language (OCL).
- Verus, a proprietary tool built by Compion, Champaign, Illinois (later purchased by Motorola), for use in the multi-level secure UNIX project pioneered by its Addamax division.
- Fastest, a model-based testing tool for the Z notation.
- Unified Modeling Language, a software system design modeling tool by Object Management Group
References
- ^ Bowen, Jonathan P. (2016). "The Z Notation: Whence the Cause and Whither the Course?" (PDF). Engineering Trustworthy Software Systems. Lecture Notes in Computer Science. Vol. 9506. Springer. pp. 103–151. doi: 10.1007/978-3-319-29628-9_3. ISBN 978-3-319-29627-2.
- ^ Abrial, Jean-Raymond (1974), "Data Semantics", in Klimbie, J. W.; Koffeman, K. L. (eds.), Proceedings of the IFIP Working Conference on Data Base Management, North-Holland, pp. 1–59
-
^
Hoare, Tony (2010).
Greetings to Bertrand on the Occasion of his Sixtieth Birthday (PDF).
Springer. p. 183.
ISBN
978-3-642-15187-3.
{{ cite book}}:|work=ignored ( help) - ^ 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. (eds.), 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.
- ^ Bowen, Jonathan (July 2022). "The Z User Group: Thirty Years After" (PDF). FACS FACTS. No. 2022–2. BCS-FACS. pp. 50–56. Retrieved 3 August 2022.
- ^ Spivey, J. Michael (1992). The Z Notation: A Reference Manual. International Series in Computer Science (2nd ed.). Hemel Hempstead: Prentice Hall. ISBN 978-0139785290.
- ^ Korpela, Jukka K. "Unicode Explained: Internationalize Documents, Programs, and Web Sites". unicode-search.net. Retrieved 24 March 2020.
- ^ a b c "ISO/IEC 13568:2002". Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics ( Zipped PDF). ISO. 1 July 2002. 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. 15 July 2007. 12 pp.
- ^ "The Queen's Award for Technological Achievement 1992". Oxford University Computing Laboratory. Archived from the original on 2 December 2008. Retrieved 17 October 2021.
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, International Thomson Publishing. 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.
- Ince, D C (1993). An Introduction to Discrete Mathematics, Formal System Specification, and Z. Oxford University Press. ISBN 9780198538370.