Z-merkintä

Z-notaatio ( englanniksi  Z notation , lausutaan /zɛd/) on muodollinen määrittelykieli, jota käytetään kuvaamaan ja mallintamaan ohjelmia ja niiden muodollista todentamista .

Jean- Raymond Abrialin vuonna 1977 ehdottama Steve Schuman ja Bertrand Meyer osallistuivat kehitykseen [1 ] .

Perustuu aksiomaattisessa joukkoteoriassa , lambda -laskennassa ja ensimmäisen asteen predikaattilogiikassa käytettyyn standardiin matemaattiseen merkintään . Kelvolliset lausekkeet Z-merkinnässä valitaan välttämään aksiomaattisen joukkoteorian paradokseja . Sisältää myös standardoidun luettelon usein käytetyistä matemaattisista funktioista ja predikaateista.

Vaikka merkintätapa käyttää monia ASCII -joukon ulkopuolisia merkkejä , määrittely sallii lausekkeiden kirjoittamisen kokonaan ASCII-muodossa tai LaTeX :n kautta , sitä tukee erikoisfontti (Z ttf -fontti) [2] .

Vuonna 2002 Kansainvälinen standardointijärjestö sai päätökseen Z-merkinnän standardointiprosessin [3] .

On olio- laajennus Object-Z [4] .

Muistiinpanot

  1. ↑ Jean-Raymond Abrial, Stephen A. Schuman ja Bertrand Meyer: A Specification Language , julkaisussa On the Construction of Programs , Cambridge University Press, toim. A.M. Macnaghten ja R.M. McKeag, 1980 (kuvaa kielen varhaista versiota). ISBN 0-521-23090-X
  2. ↑ GoldenWeb.it ->Ilmainen True Type -fonttien lataus - Zed.ttf . Haettu 7. marraskuuta 2008. Arkistoitu alkuperäisestä 13. marraskuuta 2007.
  3. ↑ Tietotekniikka - Z:n muotomäärittely - syntaksi, tyyppijärjestelmä ja  semantiikka . — ISO/IEC 13568:2002 . - 2002. - s. 196.
  4. ↑ Duke, R., & Rose, G. (2000). Muodollinen oliosuuntautunut määritys objekti-z:llä. Tietojenkäsittelyn kulmakivet. Macmillan.

Kirjallisuus

  Siirry Wikidata-kohteeseen  Bibliografisissa luetteloissa