•  


Z notation - Wikipedia Jump to content

Z notation

From Wikipedia, the free encyclopedia

An example of a formal specification (in Spanish) using the Z notation, with named schema boxes, including declarations and predicates

The Z notation / ? z ? d / is a formal specification language used for describing and modelling computing systems. [1] It is targeted at the clear specification of computer programs and computer-based systems in general.

History [ edit ]

In 1974, Jean-Raymond Abrial published "Data Semantics". [2] He used a notation that would later be taught in the University of Grenoble until the end of the 1980s. While at EDF ( Electricite de France ), working with Bertrand Meyer , Abrial also worked on developing Z. [3] The Z notation is used in the 1980 book Methodes de programmation . [4]

Z was originally proposed by Abrial in 1977 with the help of Steve Schuman and Bertrand Meyer . [5] 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!" [6] although the name " 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. [7]

Usage and notation [ edit ]

Z is based on the standard mathematical notation used in axiomatic set theory , lambda calculus , and first-order predicate logic . [8] All expressions in Z notation are typed , thereby avoiding some of the 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 language , long before it) uses many non- ASCII symbols, the specification includes suggestions for rendering the Z notation symbols in ASCII and in LaTeX . There are also Unicode encodings for all standard Z symbols. [9]

Standards [ edit ]

ISO completed a Z standardization effort in 2002. This standard [10] and a technical corrigendum [11] are available from ISO free:

  • the standard is publicly available [10] from the ISO ITTF site free of charge and, separately, available for purchase [10] from the ISO site;
  • the technical corrigendum is available [11] from the ISO site free of charge.

Award [ edit ]

In 1992, Oxford University Computing Laboratory was awarded The Queen's Award for Technological Achievement for their joint development with IBM of Z notation. [12]

See also [ edit ]

References [ edit ]

  1. ^ Bowen, Jonathan P. (2016). "The Z Notation: Whence the Cause and Whither the Course?" (PDF) . Engineering Trustworthy Software Systems . Lecture Notes in Computer Science . Vol. 9506. Springer . pp. 103?151. doi : 10.1007/978-3-319-29628-9_3 . ISBN   978-3-319-29627-2 .
  2. ^ Abrial, Jean-Raymond (1974), "Data Semantics", in Klimbie, J. W.; Koffeman, K. L. (eds.), Proceedings of the IFIP Working Conference on Data Base Management , North-Holland , pp. 1?59
  3. ^ Hoare, Tony (2010). Greetings to Bertrand on the Occasion of his Sixtieth Birthday (PDF) . Springer . p. 183. ISBN   978-3-642-15187-3 . {{ cite book }} : |work= ignored ( help )
  4. ^ Meyer, Bertrand ; Baudoin, Claude (1980), Methodes de programmation (in French), Eyrolles
  5. ^ Abrial, Jean-Raymond; Schuman, Stephen A; Meyer, Bertrand (1980), "A Specification Language", in Macnaghten, A. M.; McKeag, R. M. (eds.), On the Construction of Programs , Cambridge University Press , ISBN   0-521-23090-X (describes early version of the language).
  6. ^ Hoogeboom, Hendrik Jan. "Formal Methods in Software Engineering" (PDF) . The Netherland: University of Leiden . Retrieved 14 April 2017 .
  7. ^ Bowen, Jonathan (July 2022). "The Z User Group: Thirty Years After" (PDF) . FACS FACTS . No. 2022?2. BCS-FACS . pp. 50?56 . Retrieved 3 August 2022 .
  8. ^ Spivey, J. Michael (1992). The Z Notation: A Reference Manual . International Series in Computer Science (2nd ed.). Hemel Hempstead: Prentice Hall . ISBN   978-0139785290 .
  9. ^ Korpela, Jukka K. "Unicode Explained: Internationalize Documents, Programs, and Web Sites" . unicode-search.net . Retrieved 24 March 2020 .
  10. ^ a b c "ISO/IEC 13568:2002" . Information Technology ? Z Formal Specification Notation ? Syntax, Type System and Semantics ( Zipped PDF ) . ISO. 1 July 2002. 196 pp.
  11. ^ a b "ISO/IEC 13568:2002/Cor.1:2007". Information Technology ? Z Formal Specification Notation ? Syntax, Type System and Semantics ? Technical corrigendum 1 (PDF) . ISO. 15 July 2007. 12 pp.
  12. ^ "The Queen's Award for Technological Achievement 1992" . Oxford University Computing Laboratory . Archived from the original on 2 December 2008 . Retrieved 17 October 2021 .

Further reading [ edit ]


Retrieved from " https://en.wikipedia.org/w/index.php?title=Z_notation&oldid=1213109756 "
- "漢字路" 한글한자자동변환 서비스는 교육부 고전문헌국역지원사업의 지원으로 구축되었습니다.
- "漢字路" 한글한자자동변환 서비스는 전통문화연구회가 "울산대학교한국어처리연구실 옥철영(IT융합전공)교수팀"에서 개발한 한글한자자동변환기를 바탕하여 지속적으로 공동 연구 개발하고 있는 서비스입니다.
- 현재 고유명사(인명, 지명등)을 비롯한 여러 변환오류가 있으며 이를 해결하고자 많은 연구 개발을 진행하고자 하고 있습니다. 이를 인지하시고 다른 곳에서 인용시 한자 변환 결과를 한번 더 검토하시고 사용해 주시기 바랍니다.
- 변환오류 및 건의,문의사항은 juntong@juntong.or.kr로 메일로 보내주시면 감사하겠습니다. .
Copyright ⓒ 2020 By '전통문화연구회(傳統文化硏究會)' All Rights reserved.
 한국   대만   중국   일본 

Close