Z-notation

Z-notation ( engelsk  Z-notation , uttalas /zɛd/) är ett formellt specifikationsspråk som används för att beskriva och modellera program och deras formella verifiering .

Föreslog av Jean -Raymond Abrial 1977, Steve Schuman och Bertrand Meyer deltog i utvecklingen [1 ] .

Baserat på den matematiska standardnotationen som används i axiomatisk mängdteori , lambdakalkyl och första ordningens predikatlogik . Giltiga uttryck i Z-notation väljs för att undvika paradoxerna i axiomatisk mängdlära . Innehåller även en standardiserad katalog över ofta använda matematiska funktioner och predikat.

Även om notationen använder många tecken utanför ASCII- uppsättningen tillåter specifikationen att uttryck helt och hållet kan skrivas i ASCII eller genom LaTeX , det finns ett specialiserat teckensnitt som stödjer det (Z ttf-font) [2] .

År 2002 avslutade Internationella standardiseringsorganisationen processen med att standardisera Z-notationen [3] .

Det finns en objektorienterad förlängning Object-Z [4] .

Anteckningar

  1. ↑ Jean-Raymond Abrial, Stephen A. Schuman och Bertrand Meyer: Ett specifikationsspråk , i On the Construction of Programs , Cambridge University Press, red. A.M. Macnaghten och R.M. McKeag, 1980 (beskriver tidig version av språket). ISBN 0-521-23090-X
  2. ↑ GoldenWeb.it - ​​Gratis nedladdning av True Type-teckensnitt - Zed.ttf . Hämtad 7 november 2008. Arkiverad från originalet 13 november 2007.
  3. ↑ Informationsteknologi - Z formell specifikation Notation - Syntax, typsystem och  semantik . — ISO/IEC 13568:2002 . - 2002. - S. 196.
  4. ↑ Duke, R., & Rose, G. (2000). Formell objektorienterad specifikation med hjälp av objekt-z. Hörnstenar i datoranvändning. Macmillan.

Litteratur

  Gå till Wikidata-objektet  I bibliografiska kataloger