العربية
中国
Français
Deutsch
Ελληνική
हिन्दी
Italiano
日本語
Português
Русский
EspañolZ NOTATION
The 'Z notation' (universally pronounced ''zed'', named after Zermelo-Fränkel 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 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 [1]. 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 valuable resource for newcomers interested in learning Z is The Z Notation: a reference manual.
Z notation was used in the IBM CICS project.
The ISO completed a Z standardization effort in 2002. This standard, entitled ''Information Technology – Z Formal Specification Notation – Syntax, Type System and Semantics'', ISO/IEC 13568:2002, can be obtained directly from ISO.
13568_2002.zip, 1 MB PDF, 196 pages
★ Z++
★ Object-Z
★ Z User Group (ZUG)
★ Community Z Tools (CZT) project
★ Formal methods
★ B-Method
1. Jean-Raymond Abrial, Stephen A. Schuman and Bertrand Meyer: ''A Specification Language'', in ''On the Construction of Programs'', Cambridge University Press, eds. R. McNaughten and R.C. McKeag, 1980 (describes early version of the language). ISBN 0-521-23090-X
★ The Z Notation: a reference manual
★ Jonathan Bowen's ''The Z notation''
★ Specification proposals by Ian Toyn
★ Suppliers of the ISO formal specification
★ Community Z Tools (CZT) project
★ ZETA open-source system for development software specifications in Z
★ HOL-Z open-source proof environment for Z in Isabelle/HOL
★ Mike Spivey's Fuzz Type-Checker for Z
★ Using Z: Specification, Refinement, and Proof (Include a PDF book)
Z was originally proposed by Jean-Raymond Abrial in 1977 with the help of Steve Schuman and Bertrand Meyer [1]. 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 valuable resource for newcomers interested in learning Z is The Z Notation: a reference manual.
Z notation was used in the IBM CICS project.
| Contents |
| Standards |
| See also |
| Bibliography |
| External links |
Standards
The ISO completed a Z standardization effort in 2002. This standard, entitled ''Information Technology – Z Formal Specification Notation – Syntax, Type System and Semantics'', ISO/IEC 13568:2002, can be obtained directly from ISO.
13568_2002.zip, 1 MB PDF, 196 pages
See also
★ Z++
★ Object-Z
★ Z User Group (ZUG)
★ Community Z Tools (CZT) project
★ Formal methods
★ B-Method
Bibliography
1. Jean-Raymond Abrial, Stephen A. Schuman and Bertrand Meyer: ''A Specification Language'', in ''On the Construction of Programs'', Cambridge University Press, eds. R. McNaughten and R.C. McKeag, 1980 (describes early version of the language). ISBN 0-521-23090-X
External links
★ The Z Notation: a reference manual
★ Jonathan Bowen's ''The Z notation''
★ Specification proposals by Ian Toyn
★ Suppliers of the ISO formal specification
★ Community Z Tools (CZT) project
★ ZETA open-source system for development software specifications in Z
★ HOL-Z open-source proof environment for Z in Isabelle/HOL
★ Mike Spivey's Fuzz Type-Checker for Z
★ Using Z: Specification, Refinement, and Proof (Include a PDF book)
This article provided by Wikipedia. To edit the contents of this article, click here for original source.
psst.. try this: add to faves
