Z notacija
 |
Šį puslapį ar jo dalį reikia sutvarkyti pagal Vikipedijos standartus. Jei galite, sutvarkykite; apie sutvarkymą galite pranešti specialiame Vikipedijos projekte. |
Z notacija, pavadinta pagal Zermelo–Fraenkel aibių teoriją, yra formali specifikavimo kalba, naudojami aprašyti ir modeliuoti sistemas. Ji skirta programinės įrangos ir kompiuterių sistemoms specifikavimui.
Turinys |
Istorija [taisyti]
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 [taisyti]
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 [taisyti]
ISO baigė Z standartizaciją 2002 metais. Šis standartas gali būti įsigytas tiesiai iš ISO[3].
Taip pat skaitykite [taisyti]
- Formalūs metodai
- Formalios specifikacijos
- Formalus verifikavimas
- Modelių tikrinimas
- Procesų algebra
- Programų inžinerija
Nuorodos [taisyti]
- ↑ Jean-Raymond Abrial. Data Semantics. In "Data Base Management", eds. Klimbie, Koffeman, North-Holland, pp. 1-59.
- ↑ 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
- ↑ (2002-07-01) Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics (1 MB PDF), ISO/IEC 13568:2002, 196 pages.
Literatūra [taisyti]
- J. Michael Spivey (1992). The Z Notation: A reference manual, 2nd edition, Prentice Hall International Series in Computer Science.
- Jim Davies and Jim Woodcock (1996). Using Z: Specification, Refinement and Proof. Prentice Hall International Series in Computer Science.
- Jonathan Bowen (1996). Formal Specification and Documentation using Z: A Case Study Approach. International Thomson Computer Press.
- Jonathan Jacky (1997). The Way of Z: Practical Programming with Formal Methods. Cambridge University Press.
Išorinės nuorodos [taisyti]
- The World Wide Web Virtual Library: The Z notation
- Community Z Tools (CZT) project
- Tools for developing and checking Z specifications in Microsoft Word
- Specification proposals by Ian Toyn
- Mike Spivey's Fuzz Type-Checker for Z
- ZETA open-source system for development software specifications in Z
- HOL-Z open-source proof environment for Z in Isabelle/HOL
- Z/Eves — A proof checker for the Z notation (German site but all manuals in English)
- Z/EVES Documentation, papers, and manuals on Z/EVES
- W3C WSDL 2.0 a specification containing Z notation assertions and explanation
