Z notation

The Z notation (formally pronEng|zɛd), named after Zermelo-Fränkel set theory, is a formal specification language used for describing and modeling 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 [Jean-Raymond Abrial, Stephen A. Schuman and Bertrand Meyer: "A Specification Language", in "On the Construction of Programs", Cambridge University Press, eds. A. M. Macnaghten and R. M. McKeag, 1980 (describes early version of the language). ISBN 0-521-23090-X] . 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 [http://fonts.goldenweb.it/pan_file/l/en/font2/Zed.ttf/d2/Freeware_fonts/c/z/default.html Z ttf font] is also available for free download.

tandards

The ISO completed a Z standardization effort in 2002. This standard can be obtained directly from ISO. [cite book
title = Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics
edition = [http://www.iso.ch/iso/en/CatalogueDetailPage.CatalogueDetail?CSNUMBER=21573 ISO/IEC 13568:2002]
date = 2002-07-01
url = http://standards.iso.org/ittf/PubliclyAvailableStandards/c021573_ISO_IEC_13568_2002(E).zip
format = 1 MB PDF
pages = 196 pages]

ee also

* B-Method
* Z++
* Object-Z
* Z User Group (ZUG)
* Community Z Tools (CZT) project
* Formal methods

References

Further reading

*cite book
author = J. Michael Spivey
title = The Z Notation: a reference manual
edition = 2nd edition
year = 1992
isbn =
publisher = Prentice Hall International Series in Computer Science
url = http://spivey.oriel.ox.ac.uk/mike/zrm/
*cite book
author = Jim Davies and Jim Woodcock
title = Using Z: Specification, Refinement and Proof
year = 1996
isbn = 0-13-948472-8
publisher = Prentice Hall International Series in Computer Science
url = http://www.usingz.com/text/online/
*cite book
author = Jonathan Bowen
title = Formal Specification and Documentation using Z: A Case Study Approach
year = 1996
isbn = 1-85032-230-9
publisher = International Thomson Computer Press
url = http://www.zuser.org/zbook/
*cite book
author = Jonathan Jacky
title = The Way of Z: Practical Programming with Formal Methods
year = 1997
isbn = 0-521-55976-6
publisher = Cambridge University Press
url = http://staff.washington.edu/jon/z-book/

External links

* [http://vl.zuser.org/ The World Wide Web Virtual Library: The Z notation] , by Jonathan Bowen
* [http://czt.sourceforge.net/ Community Z Tools (CZT) project]
* [http://www.cs.york.ac.uk/hise/Zstandard/ Specification proposals by Ian Toyn]
* [http://uebb.cs.tu-berlin.de/zeta/ ZETA open-source system for development software specifications in Z]
* [http://www.brucker.ch/projects/hol-z HOL-Z open-source proof environment for Z in Isabelle/HOL]
* [http://spivey.oriel.ox.ac.uk/mike/fuzz/ Mike Spivey's Fuzz Type-Checker for Z]
* [http://www.uni-koblenz.de/~winter/Lehre/SS01/ZEves/ZEves.html Z/Eves — A proof checker for the Z notation] (German site but all manuals in English)