Z-Spezifikation
Eine Z-Spezifikation besteht aus (abwechselnd) erklärendem Text und der eigentlichen Spezifikation in Z-Notation.
Die Z-Notation bietet im wesentlichen die folgenden Ausdruckselemente:
• Definition der Basismengen (basic type definitions),
• Definition freier Typen (free type definitions),
• Definition von Schreibabkürzungen (abbreviation definitions),
• axiomatische Definitionen (axiomatic descriptions),
• einschränkende Bedingungen für globale Variable (constraints) und
• Schemadefinitionen (schema definitions).
Als Basismengen sind die natürlichen Zahlen (N), die ganzen Zahlen (Z) und die Menge der Wahrheitswerte (B) vorgegeben.
Mengen können durch das Bekanntmachen ihres Namens eingeführt werden.
[NAME, DATE, PERSON]
stellt die Mengen der Namen, Daten und Personen für nachfolgende Z-Ausdrücke zur Verfügung. Für derartige Mengen gilt, dass deren Elemente atomar sind und auf Gleichheit überprüft werden können.
Freie Typen werden durch (rekursive) Definitionen erklärt:
LIST ::= emptyList | cons << Z ✕ LIST >>
COLOR :== red | green | blue
OBJECTS :== vertex << N >> | edge << N >>
LIST ist die Menge der Listen von ganzen Zahlen. emptyList und cons sind die Konstruktoren. Aufzählungstypen wie COLOR werden durch Aufzählung der verschiedenen Konstruktoren definiert. Die Definition von OBJECTS verwendet so genanntes Tagging, bei dem bekannte Mengen "verpackt" (umbenannt) werden.
Weitere Mengen können durch Mengenkonstruktoren gewonnen werden:
P S
erzeugt die Potenzmenge von S
S ✕ T
erzeugt das kartesische Produkt von S und T.
Schreibabkürzungen dienen der verkürzten Schreibweise von Ausdrücken oder Prädikaten.
NMAX == 5
Axiomatische Definitionen bestehen aus zwei Teilen. Im ersten Teil werden die Typen der beteiligten Objekte deklariert. Der zweite, optionale Teil enthält eine Reihe von Prädikaten, mit denen Einschränkungen für die Objekte formuliert werden können.
[ square: N → N | ∀ n ∈ N ● square(n) = n * n ]
Einschränkende Bedingungen sind Prädikate, die sich auf globale Variable beziehen.
NMAX < 20
Schemadefinitionen sind benannte axiomatische Definitionen.
QUEUE ≙ [ elements: N → DATA; count: N | dom(elements) = 1 .. count ]
Die Z-Notation bietet im wesentlichen die folgenden Ausdruckselemente:
• Definition der Basismengen (basic type definitions),
• Definition freier Typen (free type definitions),
• Definition von Schreibabkürzungen (abbreviation definitions),
• axiomatische Definitionen (axiomatic descriptions),
• einschränkende Bedingungen für globale Variable (constraints) und
• Schemadefinitionen (schema definitions).
Als Basismengen sind die natürlichen Zahlen (N), die ganzen Zahlen (Z) und die Menge der Wahrheitswerte (B) vorgegeben.
Mengen können durch das Bekanntmachen ihres Namens eingeführt werden.
[NAME, DATE, PERSON]
stellt die Mengen der Namen, Daten und Personen für nachfolgende Z-Ausdrücke zur Verfügung. Für derartige Mengen gilt, dass deren Elemente atomar sind und auf Gleichheit überprüft werden können.
Freie Typen werden durch (rekursive) Definitionen erklärt:
LIST ::= emptyList | cons << Z ✕ LIST >>
COLOR :== red | green | blue
OBJECTS :== vertex << N >> | edge << N >>
LIST ist die Menge der Listen von ganzen Zahlen. emptyList und cons sind die Konstruktoren. Aufzählungstypen wie COLOR werden durch Aufzählung der verschiedenen Konstruktoren definiert. Die Definition von OBJECTS verwendet so genanntes Tagging, bei dem bekannte Mengen "verpackt" (umbenannt) werden.
Weitere Mengen können durch Mengenkonstruktoren gewonnen werden:
P S
erzeugt die Potenzmenge von S
S ✕ T
erzeugt das kartesische Produkt von S und T.
Schreibabkürzungen dienen der verkürzten Schreibweise von Ausdrücken oder Prädikaten.
NMAX == 5
Axiomatische Definitionen bestehen aus zwei Teilen. Im ersten Teil werden die Typen der beteiligten Objekte deklariert. Der zweite, optionale Teil enthält eine Reihe von Prädikaten, mit denen Einschränkungen für die Objekte formuliert werden können.
[ square: N → N | ∀ n ∈ N ● square(n) = n * n ]
Einschränkende Bedingungen sind Prädikate, die sich auf globale Variable beziehen.
NMAX < 20
Schemadefinitionen sind benannte axiomatische Definitionen.
QUEUE ≙ [ elements: N → DATA; count: N | dom(elements) = 1 .. count ]