Z-Notation: Formale Spezifikation mit Mengenlehre

Die Z-Notation (gesprochen „Zed") ist eine formale Spezifikationssprache, die Jean-Raymond Abrial ab den 1970er-Jahren an der Universität Oxford entwickelte. Sie basiert auf der Zermelo-Fraenkel-Mengenlehre und der Prädikatenlogik — daher der Name — und ist seit 2002 als ISO-Standard 13568 genormt. Mit Z beschreibt man den Zustand eines Systems und seine Operationen präzise, ohne sofort implementieren zu müssen.

Schema-Boxen

Konto
────────────────────────
kontostand : Z
────────────────────────
kontostand >= 0

Eine Schema-Box hat einen Namen, einen Deklarationsteil (Variablen mit Typen) und einen Prädikatenteil (Invarianten). Operationen beschreibt man als Schemata mit Δ (Zustand ändert sich) oder Ξ (Zustand bleibt unverändert):

Einzahlen
────────────────────────
ΔKonto
betrag : Z
────────────────────────
betrag > 0
kontostand' = kontostand + betrag

Der Apostroph (') bezeichnet den Variablenwert nach der Operation — dasselbe Muster wie in TLA+.

Mathematische Bausteine

  • Mengen und Relationen: ∈, ⊆, ∪, ∩, , ×.
  • Funktionen: totale Funktion →, partielle Funktion ⇸, Maplet ↦.
  • Sequenzen: seq, Länge #, Verkettung ^, head/tail.
  • Domäne/Range: dom, ran.

Werkzeuge und Einsatz

Werkzeuge sind fuzz (Spivey), Z/EVES, ProofPower-Z und das Open-Source-Framework Community Z Tools (CZT) mit Parser, Typchecker und LaTeX-/Unicode-Ausgabe. Z wurde unter anderem bei der Mondex-Smartcard-Geldbörse und im IBM-CICS-Umfeld eingesetzt. Während Z Struktur und Zustand mathematisch spezifiziert, modellieren Promela mit dem Model Checker SPIN ausführbares Prozessverhalten; Beweisassistenten wie Isabelle verifizieren die so aufgeschriebenen Eigenschaften maschinell.