Notația Z

Notația Z ( în engleză  Notația Z , pronunțată /zɛd/) este un limbaj de specificare formală folosit pentru a descrie și modela programe și verificarea lor formală .

Propuși de Jean -Raymond Abrial în 1977, Steve Schuman și Bertrand Meyer au participat la dezvoltare [1 ] .

Bazat pe notația matematică standard utilizată în teoria mulțimilor axiomatice , calculul lambda și logica predicatelor de ordinul întâi . Expresiile valide în notația Z sunt alese pentru a evita paradoxurile teoriei axiomatice a mulțimilor . Conține, de asemenea, un catalog standardizat de funcții și predicate matematice utilizate frecvent.

Deși notația folosește multe caractere în afara setului ASCII , specificația permite ca expresiile să fie scrise în întregime în ASCII sau prin LaTeX , există un font specializat care să o susțină (fontul Z ttf) [2] .

În 2002, Organizația Internațională de Standardizare a finalizat procesul de standardizare a notației Z [3] .

Există o extensie orientată pe obiecte Object-Z [4] .

Note

  1. ↑ Jean-Raymond Abrial, Stephen A. Schuman și Bertrand Meyer: A Specification Language , în On the Construction of Programs , Cambridge University Press, eds. A.M. Macnaghten și R.M. McKeag, 1980 (descrie versiunea timpurie a limbii). ISBN 0-521-23090-X
  2. ↑ GoldenWeb.it - ​​Descărcare gratuită a fonturilor True Type - Zed.ttf . Consultat la 7 noiembrie 2008. Arhivat din original pe 13 noiembrie 2007.
  3. ↑ Tehnologia informației - Notarea specificației formale Z - Sintaxă, Sistem de tipare și  Semantică . — ISO/IEC 13568:2002 . - 2002. - P. 196.
  4. ↑ Duke, R., & Rose, G. (2000). Specificație formală orientată pe obiect folosind obiect-z. Pietrele de temelie ale calculului. Macmillan.

Literatură

  Accesați articolul Wikidata  În cataloagele bibliografice