Z notacija

Šį puslapį ar jo dalį reikia sutvarkyti pagal Vikipedijos standartus. Jei galite, sutvarkykite.

Z notacija, pavadinta pagal Zermelo–Fraenkel aibių teoriją – formali specifikavimo kalba, naudojami aprašyti ir modeliuoti sistemas. Ji skirta programinės įrangos ir kompiuterių sistemoms specifikavimui.

Istorija

Jean-Raymond Abrial 1974 metais paskelbė pradinę žymėjimo versiją "Data Semantics" ^[1], kurią dėstė Grenoblio universitete iki aštuoniasdešimtųjų pabaigos.

Pirmą kartą Z notaciją pasiūlė Abrial su Steve Schuman ir Bertrand Meyer 1977^[2]. Toliau Z buvo plėtojama Programavimo Tyrimų grupėje (Programming Research Group) Oksfordo universitete.

Abrialas atsakymas į klausimą „kodėl Z?“ - „Nes tai pagrindinė kalba!”

Naudojimas ir notacija

Z remiasi standartine matematine notacija, naudojama aksiomatinėje aibių teorijoje, lambda algebroje ir pirmos eilės predikatų logikoje. Visos Z išraiškos yra tipizuotas, tuo būdu išvengiant kai kurių paprastos aibių teorijos paradoksų. Z sudaro standartizuotas dažnai naudojamų matematinių funkcijų ir predikatų katalogas, vadinamas matematiniu įrankių komplektu.

Z notacija naudoja daug ne ASCII simbolių, todėl kalbos aprašyme rekomenduojama, kaip juos užrašyti ASCII ir LaTeX (TeX). Taip pat nemokamai galima parsisiųsti Z ttf šriftą.

Standartai

ISO baigė Z standartizaciją 2002 metais. Šis standartas gali būti įsigytas tiesiai iš ISO.^[3].

Taip pat skaitykite

• Formalūs metodai
• Formalios specifikacijos
• Formalus verifikavimas
• Modelių tikrinimas
• Procesų algebra
• Programų inžinerija

Šaltiniai

1. Jean-Raymond Abrial. Data Semantics. In "Data Base Management", eds. Klimbie, Koffeman, North-Holland, pp. 1-59.
2. 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
3. Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics (1 MB PDF). 2002-07-01. pp. 196 pages.

Literatūra

• J. Michael Spivey (1992). The Z Notation: A reference manual (2nd leid.). Prentice Hall International Series in Computer Science. Suarchyvuotas originalas 2008-10-09. Nuoroda tikrinta 2009-12-14.
• Jim Davies and Jim Woodcock (1996). Using Z: Specification, Refinement and Proof. Prentice Hall International Series in Computer Science. ISBN 0-13-948472-8. Suarchyvuotas originalas 2009-06-27. Nuoroda tikrinta 2009-12-14.
• Jonathan Bowen (1996). Formal Specification and Documentation using Z: A Case Study Approach. International Thomson Computer Press. ISBN 1-85032-230-9. Suarchyvuotas originalas 2010-04-09. Nuoroda tikrinta 2009-12-14.
• Jonathan Jacky (1997). The Way of Z: Practical Programming with Formal Methods. Cambridge University Press. ISBN 0-521-55976-6.

Nuorodos

• The World Wide Web Virtual Library: The Z notation
• Community Z Tools (CZT) project Archyvuota kopija 2004-07-01 iš Wayback Machine projekto.
• Tools for developing and checking Z specifications in Microsoft Word
• Specification proposals by Ian Toyn Archyvuota kopija 2012-06-22 iš Wayback Machine projekto.
• Mike Spivey's Fuzz Type-Checker for Z Archyvuota kopija 2006-03-26 iš Wayback Machine projekto.
• ZETA open-source system for development software specifications in Z Archyvuota kopija 2006-01-10 iš Wayback Machine projekto.
• HOL-Z open-source proof environment for Z in Isabelle/HOL^{[neveikianti nuoroda]}
• Z/Eves – A proof checker for the Z notation Archyvuota kopija 2009-05-19 iš Wayback Machine projekto. (German site but all manuals in English)
• Z/EVES Archyvuota kopija 2011-10-07 iš Wayback Machine projekto. Documentation, papers, and manuals on Z/EVES
• W3C WSDL 2.0 a specification containing Z notation assertions and explanation