Zápis Z

Z-notace ( anglicky  Z notation , vyslovováno /zɛd/) je formální specifikační jazyk používaný k popisu a modelování programů a jejich formální verifikace .

Navrhl Jean -Raymond Abrial v roce 1977, Steve Schuman a Bertrand Meyer se podíleli na vývoji [1 ] .

Na základě standardní matematické notace používané v axiomatické teorii množin , lambda počtu a predikátové logice prvního řádu . Platné výrazy v Z-notaci jsou vybrány, aby se zabránilo paradoxům axiomatické teorie množin . Obsahuje také standardizovaný katalog často používaných matematických funkcí a predikátů.

Ačkoli zápis používá mnoho znaků mimo sadu ASCII , specifikace umožňuje, aby byly výrazy zapsány výhradně v ASCII nebo prostřednictvím LaTeXu , existuje specializovaný font, který to podporuje (font Z ttf) [2] .

V roce 2002 dokončila Mezinárodní organizace pro standardizaci proces standardizace zápisu Z [3] .

Existuje objektově orientované rozšíření Object-Z [4] .

Poznámky

  1. ↑ Jean-Raymond Abrial, Stephen A. Schuman a Bertrand Meyer: A Specification Language , v On the Construction of Programs , Cambridge University Press, eds. AM Macnaghten a RM McKeag, 1980 (popisuje ranou verzi jazyka). ISBN 0-521-23090-X
  2. ↑ GoldenWeb.it – Zdarma True Type Fonty ke stažení – Zed.ttf . Získáno 7. listopadu 2008. Archivováno z originálu 13. listopadu 2007.
  3. ↑ Informační technologie - Zápis formální specifikace Z - Syntaxe, typový systém a  sémantika . — ISO/IEC 13568:2002 . - 2002. - S. 196.
  4. ↑ Duke, R., & Rose, G. (2000). Formální objektově orientovaná specifikace pomocí object-z. Základní kameny výpočetní techniky. Macmillan.

Literatura

  Přejděte na položku Wikidata  V bibliografických katalozích