Z jelölés

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] .

Jegyzetek

  1. Jean-Raymond Abrial, Stephen A. Schuman és Bertrand Meyer: A Specification Language , On the Construction of Programs , Cambridge University Press, szerk. A.M. Macnaghten és R.M. McKeag, 1980 (a nyelv korai változatát írja le). ISBN 0-521-23090-X
  2. GoldenWeb.it - ​​Ingyenes True Type Fonts letöltés - Zed.ttf . Letöltve: 2008. november 7. Az eredetiből archiválva : 2007. november 13..
  3. Információtechnológia - Z Formális specifikációs jelölések - Szintaxis, típusrendszer és  szemantika . – ISO/IEC 13568:2002 . - 2002. - 196. o.
  4. Duke, R. és Rose, G. (2000). Formális objektumorientált specifikáció az objektum-z használatával. A számítástechnika sarokkövei. Macmillan.

Irodalom