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.[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 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 Fuzz, a 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): VDM-SL, the main alternative to Z (compare) 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.  ^ 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. ^ 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 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. Archived from the original on 2009-06-27.  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 v t e ISO standards by standard number List of ISO standards / ISO romanizations / IEC standards 1–9999 1 2 3 4 5 6 7 9 16 31 -0 -1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 -12 -13 128 216 217 226 228 233 259 269 302 306 428 518 519 639 -1 -2 -3 -5 -6 646 690 732 764 843 898 965 1000 1004 1007 1073-1 1413 1538 1745 1989 2014 2015 2022 2047 2108 2145 2146 2240 2281 2709 2711 2788 2848 2852 3029 3103 3166 -1 -2 -3 3297 3307 3602 3864 3901 3977 4031 4157 4217 4909 5218 5428 5775 5776 5800 5964 6166 6344 6346 6385 6425 6429 6438 6523 6709 7001 7002 7098 7185 7200 7498 7736 7810 7811 7812 7813 7816 8000 8178 8217 8571 8583 8601 8632 8652 8691 8807 8820-5 8859 -1 -2 -3 -4 -5 -6 -7 -8 -8-I -9 -10 -11 -12 -13 -14 -15 -16 8879 9000/9001 9075 9126 9293 9241 9362 9407 9506 9529 9564 9594 9660 9897 9899 9945 9984 9985 9995 10000–19999 10005 10006 10007 10116 10118-3 10160 10161 10165 10179 10206 10218 10303 -11 -21 -22 -28 -238 10383 10487 10585 10589 10646 10664 10746 10861 10957 10962 10967 11073 11170 11179 11404 11544 11783 11784 11785 11801 11898 11940 (-2) 11941 11941 (TR) 11992 12006 12182 12207 12234-2 13211 -1 -2 13216 13250 13399 13406-2 13450 13485 13490 13567 13568 13584 13616 14000 14031 14224 14289 14396 14443 14496 -2 -3 -6 -10 -11 -12 -14 -17 -20 14644 14649 14651 14698 14750 14764 14882 14971 15022 15189 15288 15291 15292 15398 15408 15444 -3 15445 15438 15504 15511 15686 15693 15706 -2 15707 15897 15919 15924 15926 15926 WIP 15930 16023 16262 16612-2 16750 16949 (TS) 17024 17025 17100 17203 17369 17442 17799 18000 18004 18014 18245 18629 18916 19005 19011 19092 (-1 -2) 19114 19115 19125 19136 19439 19500 19501 19502 19503 19505 19506 19507 19508 19509 19510 19600:2014 19752 19757 19770 19775-1 19794-5 19831 20000+ 20000 20022 20121 20400 21000 21047 21500 21827:2002 22000 23270 23271 23360 24517 24613 24617 24707 25178 25964 26000 26300 26324 27000 series 27000 27001 27002 27006 27729 28000 29110 29148 29199-2 29500 30170 31000 32000 38500 40500 42010 55000 80000 -1 -2 -3 Category v t e List of International Electrotechnical Commission standards IEC standards IEC 60027 IEC 60034 IEC 60038 IEC 60062 IEC 60063 IEC 60068 IEC 60112 IEC 60228 IEC 60269 IEC 60297 IEC 60309 IEC 60320 IEC 60364 IEC 60446 IEC 60559 IEC 60601 IEC 60870 IEC 60870-5 IEC 60870-6 IEC 60906-1 IEC 60908 IEC 60929 IEC 60958 AES3 S/PDIF IEC 61030 IEC 61131 IEC 61131-3 IEC 61158 IEC 61162 IEC 61334 IEC 61346 IEC 61355 IEC 61400 IEC 61499 IEC 61508 IEC 61511 IEC 61850 IEC 61851 IEC 61883 IEC 61960 IEC 61968 IEC 61970 IEC 62014-4 IEC 62056 IEC 62061 IEC 62196 IEC 62262 IEC 62264 IEC 62304 IEC 62325 IEC 62351 IEC 62365 IEC 62366 IEC 62379 IEC 62386 IEC 62455 IEC 62680 IEC 62682 IEC 62700 ISO/IEC standards ISO/IEC 646 ISO/IEC 2022 ISO/IEC 4909 ISO/IEC 5218 ISO/IEC 6429 ISO/IEC 6523 ISO/IEC 7810 ISO/IEC 7811 ISO/IEC 7812 ISO/IEC 7813 ISO/IEC 7816 ISO/IEC 7942 ISO/IEC 8613 ISO/IEC 8632 ISO/IEC 8652 ISO/IEC 8859 ISO/IEC 9126 ISO/IEC 9293 ISO/IEC 9592 ISO/IEC 9593 ISO/IEC 9899 ISO/IEC 9945 ISO/IEC 9995 ISO/IEC 10021 ISO/IEC 10116 ISO/IEC 10165 ISO/IEC 10179 ISO/IEC 10646 ISO/IEC 10967 ISO/IEC 11172 ISO/IEC 11179 ISO/IEC 11404 ISO/IEC 11544 ISO/IEC 11801 ISO/IEC 12207 ISO/IEC 13250 ISO/IEC 13346 ISO/IEC 13522-5 ISO/IEC 13568 ISO/IEC 13818 ISO/IEC 14443 ISO/IEC 14496 ISO/IEC 14882 ISO/IEC 15288 ISO/IEC 15291 ISO/IEC 15408 ISO/IEC 15444 ISO/IEC 15445 ISO/IEC 15504 ISO/IEC 15511 ISO/IEC 15693 ISO/IEC 15897 ISO/IEC 15938 ISO/IEC 16262 ISO/IEC 17024 ISO/IEC 17025 ISO/IEC 18000 ISO/IEC 18004 ISO/IEC 18014 ISO/IEC 19752 ISO/IEC 19757 ISO/IEC 19770 ISO/IEC 19788 ISO/IEC 20000 ISO/IEC 21000 ISO/IEC 21827 ISO/IEC 23000 ISO/IEC 23003 ISO/IEC 23008 ISO/IEC 23270 ISO/IEC 23360 ISO/IEC 24707 ISO/IEC 24727 ISO/IEC 24744 ISO/IEC 24752 ISO/IEC 26300 ISO/IEC 27000 ISO/IEC 27000-series ISO/IEC 27002 ISO/IEC 27040 ISO/IEC 29119 ISO/IEC 33001 ISO/IEC 38500 ISO/IEC 42010 ISO/IEC 80000 Related International Electrotechnical Commission Authority control GND: 4225739-6 Retrieved from "https://en.wikipedia.org/w/index.php?title=Z_notation&oldid=830296262" Categories: Computer-related introductions in 1977Specification languagesFormal specification languagesZ notationOxford University Computing LaboratoryHidden categories: CS1 French-language sources (fr)All articles with unsourced statementsArticles with unsourced statements from February 2011Wikipedia articles with GND identifiers