View source for Z notation

{{Short description|Formal specification language used for describing and modelling computing systems}}
[[File:Agendacumple en Z.svg|thumb|350px|An example of a [[Formal specification|formal specification]] (in Spanish) using the Z notation, with named schema boxes, including declarations and predicates.]]

The '''Z notation''' {{IPAc-en|ˈ|z|ɛ|d}} is a [[Formal specification|formal]] [[Specification language|specification language]] used for describing and modelling computing systems.<ref>{{cite book| last=Bowen | first=Jonathan P. | chapter=The Z Notation: Whence the Cause and Whither the Course? |  title=Engineering Trustworthy Software Systems | pages=103–151 | publisher=[[Company:Springer Science+Business Media|Springer]] | series=[[Lecture Notes in Computer Science]] | volume=9506 | date=2016 | doi=10.1007/978-3-319-29628-9_3| isbn=978-3-319-29627-2 | chapter-url=http://researchopen.lsbu.ac.uk/395/1/setss2014.pdf }}</ref> It is targeted at the clear specification of [[Computer program|computer program]]s and computer-based systems in general.

==History==
In 1974, [[Biography:Jean-Raymond Abrial|Jean-Raymond Abrial]] published "Data Semantics".<ref>{{Citation |  first = Jean-Raymond | last = Abrial | contribution = Data Semantics | editor1-last = Klimbie | editor1-first = J. W. | editor2-last = Koffeman | editor2-first = K. L. | title = Proceedings of the IFIP Working Conference on Data Base Management | publisher = North-Holland | pages = 1–59 | year=1974 }}</ref> 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 [[Biography:Bertrand Meyer|Bertrand Meyer]], Abrial also worked on developing Z.<ref>{{cite book| url=https://link.springer.com/content/pdf/bbm%3A978-3-642-15187-3%2F1.pdf | title=Greetings to Bertrand on the Occasion of his Sixtieth Birthday | first=Tony | last=Hoare |  date=2010 | work=The Future of Software Engineering | page=183 | isbn=978-3-642-15187-3 | publisher=[[Company:Springer Science+Business Media|Springer]] }}</ref> The Z notation is used in the 1980 book ''Méthodes de programmation''.<ref>{{Citation |  first1 = Bertrand | last1 = Meyer | first2 = Claude | last2 = Baudoin | title = Méthodes de programmation | publisher = Eyrolles | year = 1980 | language = fr}}</ref>

Z was originally proposed by Abrial in 1977 with the help of Steve Schuman and [[Biography:Bertrand Meyer|Bertrand Meyer]].<ref>{{Citation | first1 = Jean-Raymond | last1 = Abrial | first2 = Stephen A | last2 = Schuman | first3 = Bertrand | last3 = Meyer | contribution = A Specification Language | title = On the Construction of Programs | publisher = {{wipe|Cambridge University Press}} | editor1-first = A. M. | editor1-last = Macnaghten | editor2-first = R. M. | editor2-last = McKeag | year = 1980 | isbn = 0-521-23090-X}} (describes early version of the language).</ref> 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!"<ref>{{cite web|
 url=http://liacs.leidenuniv.nl/~hoogeboomhj/praatjes/formalmethods/formalmethods.pdf |
 title=Formal Methods in Software Engineering | first=Hendrik Jan | last=Hoogeboom | publisher=University of Leiden | location=The Netherland | access-date=14 April 2017 }}</ref> although the name "[[Biography:Ernst Zermelo|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.<ref name="zug22">{{cite news| first=Jonathan | last=Bowen |  title=The Z User Group: Thirty Years After | work=FACS FACTS | publisher=BCS-FACS | issue=2022–2 | pages=50–56 | date=July 2022 | url=https://www.bcs.org/media/9401/facs-jul22.pdf | accessdate=3 August 2022 }}</ref>

==Usage and notation==
Z is based on the standard mathematical notation used in axiomatic set theory, [[Lambda calculus|lambda calculus]], and first-order predicate logic.<ref>{{cite book| last=Spivey | first=J. Michael |  title=The Z Notation: A Reference Manual | edition=2nd | location=Hemel Hempstead | publisher=Prentice Hall | series=International Series in Computer Science | date=1992 | isbn=978-0139785290 }}</ref> All expressions in Z notation are [[Type (model theory)|typed]], thereby avoiding some of the [[Naive set theory#Paradoxes|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 (programming language)|APL language]], long before it) uses many non-[[ASCII]] symbols, the specification includes suggestions for rendering the Z notation symbols in [[ASCII]] and in [[Software:LaTeX|LaTeX]]. There are also [[Unicode]] encodings for all standard Z symbols.<ref>{{cite web| url=https://unicode-search.net/unicode-namesearch.pl?term=Z%20NOTATION | title=Unicode Explained: Internationalize Documents, Programs, and Web Sites | first=Jukka K. | last=Korpela | website=unicode-search.net | access-date=24 March 2020 }}</ref>

==Standards==
[[Organization:International Organization for Standardization|ISO]] completed a Z standardization effort in 2002. This standard<ref name = "Standard">{{cite book | title = Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics | chapter-url = http://www.iso.ch/iso/en/CatalogueDetailPage.CatalogueDetail?CSNUMBER=21573 | chapter = ISO/IEC 13568:2002 | date = 2002-07-01 | publisher = ISO | url = http://standards.iso.org/ittf/PubliclyAvailableStandards/c021573_ISO_IEC_13568_2002(E).zip | format = [[Zip (file format)|Zip]]ped [[PDF]]}}  196 pp.</ref> and a technical corrigendum<ref name = "Corrigendum">{{cite book | title = Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics — Technical corrigendum 1 | url = http://www.iso.org/iso/iso_catalogue/catalogue_tc/catalogue_detail.htm?csnumber=46112 | chapter = ISO/IEC 13568:2002/Cor.1:2007 | publisher = ISO | date = 2007-07-15 | format = PDF}}  12 pp.</ref> are available from ISO free:
* the standard is publicly available<ref name = "Standard" /> from the ISO ITTF site free of charge and, separately, available for purchase<ref name = "Standard" /> from the ISO site;
* the technical corrigendum is available<ref name = "Corrigendum" /> 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 [[Company:IBM|IBM]] of Z notation.<ref>{{cite web |url=http://web2.comlab.ox.ac.uk/oucl/about/qata92.html |title=The Queen's Award for Technological Achievement 1992 |archive-url=https://web.archive.org/web/20081202044350/http://web2.comlab.ox.ac.uk/oucl/about/qata92.html |archive-date=2 December 2008 |website= Oxford University Computing Laboratory |access-date=17 October 2021}}</ref>

==See also==
* Z User Group (ZUG)
* [[Software:Community Z Tools|Community Z Tools]] (CZT) project
* Other [[Formal methods|formal methods]] (and languages using [[Formal specification|formal specification]]s):
** 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 (specification language)|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.
* [[Software:Fastest|Fastest]], a [[Model-based testing|model-based testing]] tool for the Z notation.
* [[Unified Modeling Language]], a software system design modeling tool by [[Organization:Object Management Group|Object Management Group]]

==References==
{{Reflist}}

==Further reading==
*{{cite book
 | title = The Z Notation: A reference manual | edition = 2nd | year = 1992
 | publisher = Prentice Hall | series = International Series in Computer Science | url=https://spivey.oriel.ox.ac.uk/corner/Z_Reference_Manual }}
*{{cite book|title=Using Z: Specification, Refinement and Proof|last1=Davies|first1=Jim|last2=Woodcock|first2=Jim|publisher=Prentice Hall|year=1996|isbn=0-13-948472-8|series=International Series in Computer Science| url=http://www.usingz.com/ }}
*{{cite book|title=Formal Specification and Documentation using Z: A Case Study Approach|last=Bowen|first=Jonathan| publisher=International Thomson Computer Press, International Thomson Publishing |year=1996|isbn=1-85032-230-9| url=https://www.researchgate.net/publication/2480325 }}
*{{cite book|title=The Way of Z: Practical Programming with Formal Methods|last=Jacky|first=Jonathan| publisher={{wipe|Cambridge University Press}} |year=1997|isbn=0-521-55976-6| url=https://staff.washington.edu/jon/z-book/ }}
*{{cite book|title=An Introduction to Discrete Mathematics, Formal System Specification, and Z|last=Ince|first=D C| publisher=[[Organization:Oxford University Press|Oxford University Press]] |year=1993|isbn=9780198538370| url=https://doi.org/10.1093/oso/9780198538370.001.0001 }}


{{ISO standards}}
{{List of IEC standards}}

{{DEFAULTSORT:Z Notation}}
[[Category:Specification languages]]
[[Category:Formal specification languages]]

{{Sourceattribution|Z notation}}