A Z-jelölés ( angolul Z notation , ejtsd: /zɛd/) egy formális specifikációs nyelv , amelyet a programok leírására és modellezésére , valamint azok formális ellenőrzésére használnak .
Jean -Raymond Abrial javaslatára 1977-ben Steve Schuman és Bertrand Meyer vett részt a fejlesztésben [1 ] .
Az axiomatikus halmazelméletben , a lambda-számításban és az elsőrendű predikátumlogikában használt szabványos matematikai jelölésen alapul . A Z-jelölésben érvényes kifejezéseket úgy választjuk meg, hogy elkerüljük az axiomatikus halmazelmélet paradoxonjait . Tartalmazza a gyakran használt matematikai függvények és predikátumok szabványosított katalógusát is.
Bár a jelölés sok karaktert használ az ASCII -készleten kívül , a specifikáció lehetővé teszi, hogy a kifejezéseket teljes egészében ASCII-ben vagy LaTeX -en keresztül írják le , de van egy speciális betűkészlet, amely támogatja ezt (Z ttf font) [2] .
2002-ben a Nemzetközi Szabványügyi Szervezet befejezte a Z jelölés szabványosítási folyamatát [3] .
Létezik egy objektumorientált kiterjesztés az Object-Z [4] .
![]() |
---|