The
Z notation (formally ), named after
Zermelo–Fraenkel set
theory, is a
formal
specification language used
for describing and modelling computing systems. 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" in
Data Base Management
(Klimbie, Koffeman, eds), North-Holland, pp 1-59. He used a
notation that would later be taught in the Université de Grenoble
until the end of the eighties. While at EDF (
Électricité de France),
Abrial wrote internal notes on Z. The Z notation is used in the
book of
Bertrand Meyer and Claude
Baudoin,
Méthodes de programmation, published by Eyrolles
in 1980.
Z was originally proposed by Abrial in 1977 with the help of Steve
Schuman and Bertrand Meyer .
It was developed further at the Programming
Research Group
at Oxford University
, where Abrial worked in the early eighties (he
arrived in Oxford on September 1979).
Abrial answers the question "Why Z?" with "Because it is the
ultimate language!"
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 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
Z ttf font is also available for free
download.
Standards
The
ISO completed
a Z standardization effort in 2002. This standard can be obtained
directly from ISO.
See also
References
Further reading
External links
Top topics
Wikis
Quiz
Map
Search
