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)


Wikimedia Foundation. 2010.

Look at other dictionaries:

  • Notation de la dette — Notation financière Pour les articles homonymes, voir notation et rating. La notation financière ou notation de la dette ou rating (dans le monde anglo saxon) est l appréciation, par une agence de notation financière, du risque de solvabilité… …   Wikipédia en Français

  • Notation financiere — Notation financière Pour les articles homonymes, voir notation et rating. La notation financière ou notation de la dette ou rating (dans le monde anglo saxon) est l appréciation, par une agence de notation financière, du risque de solvabilité… …   Wikipédia en Français

  • notation — [ nɔtasjɔ̃ ] n. f. • 1531 « décision »; lat. notatio 1 ♦ (1750) Action, manière de noter, de représenter par des symboles; système de symboles. Notation des nombres, notation numérique; notation par lettres. Notation littérale, algébrique, créée… …   Encyclopédie Universelle

  • NOTATION MUSICALE — Contrairement à la peinture et à la sculpture, la musique est un art qui suppose un intermédiaire entre le créateur et son public. Cet intermédiaire, l’exécutant, se voit confier un texte noté selon certaines conventions qui ont évolué au fil des …   Encyclopédie Universelle

  • NOTATION MATHÉMATIQUE — Pour connaître une langue naturelle, il n’est pas nécessaire d’en apprendre l’histoire ni, pour comprendre sa littérature, de faire l’étude historique de la grammaire et du vocabulaire. À cet égard, le langage mathématique, en raison de son… …   Encyclopédie Universelle

  • Notation — ist die Benennung von Gegenständen durch das Festhalten (qualitative und quantitative Repräsentation) von Dingen und Bewegungsverläufen in schriftlicher Form mit vereinbarten symbolischen Zeichen. Das Fehlen einer Notation macht es bisweilen… …   Deutsch Wikipedia

  • Notation algebrique — Notation algébrique …   Wikipédia en Français

  • Notation algébrique (jeu d'échecs) — Notation algébrique …   Wikipédia en Français

  • Notation échiquéenne — Notation algébrique …   Wikipédia en Français

  • Notation (jonglerie) — Notation en jonglerie Pour les articles homonymes, voir notation. Une notation en jonglerie est, à l’image d’une notation musicale, le fait de transcrire sur un support la description d’un mouvement de jonglerie afin de pouvoir le conserver, le… …   Wikipédia en Français

  • Notation de Conway — Notation des flèches chaînées de Conway La notation des flèches chaînées de Conway est un moyen d exprimer de très grands nombres créée par le mathématicien John Horton Conway. Elle consiste en une suite finie d entiers positifs séparés par des… …   Wikipédia en Français

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”