Z-notation

Z-notation ( engelsk  Z-notation , udtales /zɛd/) er et formelt specifikationssprog, der bruges til at beskrive og modellere programmer og deres formelle verifikation .

Foreslået af Jean -Raymond Abrial i 1977, deltog Steve Schuman og Bertrand Meyer i udviklingen [1 ] .

Baseret på den matematiske standardnotation, der bruges i aksiomatisk mængdeteori , lambdaregning og førsteordens prædikatlogik . Gyldige udtryk i Z-notation er valgt for at undgå paradokserne i den aksiomatiske mængdeteori . Indeholder også et standardiseret katalog over ofte anvendte matematiske funktioner og prædikater.

Selvom notationen bruger mange tegn uden for ASCII- sættet , tillader specifikationen udtryk at blive skrevet helt i ASCII eller gennem LaTeX , der er en specialiseret skrifttype til at understøtte det (Z ttf font) [2] .

I 2002 afsluttede International Organization for Standardization processen med at standardisere Z-notationen [3] .

Der er en objektorienteret udvidelse Object-Z [4] .

Noter

  1. ↑ Jean-Raymond Abrial, Stephen A. Schuman og Bertrand Meyer: A Specification Language , i On the Construction of Programs , Cambridge University Press, eds. A.M. Macnaghten og R.M. McKeag, 1980 (beskriver den tidlige version af sproget). ISBN 0-521-23090-X
  2. ↑ GoldenWeb.it - ​​Gratis True Type-skrifttyper download - Zed.ttf . Hentet 7. november 2008. Arkiveret fra originalen 13. november 2007.
  3. ↑ Informationsteknologi - Z Formel specifikation Notation - Syntaks, typesystem og  semantik . — ISO/IEC 13568:2002 . - 2002. - S. 196.
  4. ↑ Duke, R., & Rose, G. (2000). Formel objektorienteret specifikation ved hjælp af objekt-z. Hjørnesten i computing. Macmillan.

Litteratur

  Gå til Wikidata-elementet  I bibliografiske kataloger