Post on 06-Apr-2016
transcript
Elemente einer Z-Spezifikation
Spezifikation und Verifikation PRWS 03/04
Auer AngelikaHarrich Michaela
Schönhart SabrinaGruppe 4
Struktur einer Z-Spezifikation
Given SetsGlobale VariablenConstraintsZustandsraum InitialisierungOperationen auf den Zustandsraum
Basic Types, Globale Constants, User defined sets[ARZT, PATIENT]
maxAerzte: maxAerzte = 5
RESULT::= OK | NOK
State Spacedoktoren: ARZTpatienten: PATIENTbehandelt: ARZT PATIENT#doktoren ≤ maxAerzteran behandelt patientendom behandelt doktoren
Prädikate
Deklarationen
BezeichnungArztpraxis
Operationsschemata (1)• Spezifieren die über dem
Zustandsraum definierten Operationen
• Eine Operation wird durch ein gewöhnliches Schemata beschrieben
• Die Operation wird nicht explizit deklariert
Operationsschemata (2)• Operationsname = Schemaname• Parameter:
- x?: Eingabeparameter- y!: Ausgabeparameter
• Zustände:s: Zustand vor der Operations´: Zustand nach der Operation
Operationsschemata (3)Operationsschemata gliedern sich in • Preconditions
müssen vor der Operationsausführung erfüllt sein
• Aktion (Transformation)Spezifizierung der Zustandsraumänderung, die durch diese Operation bewirkt werden soll
• Postconditonsmüssen nach der Operationsausführung erfüllt sein
Operationsschematazustandsverändernd
Arztpraxisdoktor?: ARZTantwort!: RESULTdoktor? doktoren#doktoren < maxAerztedoktoren‘ = doktoren {doktor?}antwort! = OK
AufnahmeArztOK
Operationsschematazustandserhaltend
Arztpraxisdoktor?: ARZTantwort!: RESULTdoktor? doktoren#doktoren maxAerzteantwort! = NOK
AufnahmeArztNOK
Initialzustand• beschreiben gültige initiale Zustände
des Systems• beinhalten Wertzuweisungen, die die
Constraints des Zustandraumes erfüllen müssen
Arztpraxisdoktoren = patienten =
InitArztpraxis
Typen, Konstanten und Funktionen
Typen• Basieren auf Mengenbegriff
Menge: Zusammenfassung von beliebigen Elementen unter einem gemeinsamen Namen. Unendliche und endliche Mengen.
• Mengendefinition Extensional: durch Auflistung AMPELFARBE == rot, gelb, grün Intensional: mit Hilfe von Prädikaten FERIALMONAT = {x: MONAT | x Jul, Aug, Sept}
Typen (1)• Zusammenfassung jener Elemente, die
durch einen Satz von Operationen nach gemeinsamen Regeln manipuliert werden können.
• Besteht aus Grundmenge gleichartiger Elemente.
• Ein Typ ist eine maximale Menge.
Typdefinitionen in Z• Sehr eingeschränkter Satz von
vordefinieren Typen:
• Weitere Typen werden aus given sets aufgebaut: [X,Y]; [Namen]; [Banken]; [Tiere];...
Typdefinition in Z (1)• Wir können „Vertreter“ in
Mengendefinitionen auflisten. Für generische Typen definieren wir jedoch Variablen, die Werte des jeweiligen generischen Typs annehmen.
• Bsp.: Tiere == Pferd, Tieger, Strauß | Pferd, Tieger, Strauß : [Tiere]
AufzählungstypenAntwort ::= JA|NEIN
Dient als Abkürzung für:
JA,NEIN : AntwortJA NEINantw: Antwort antw = JA antw = NEIN
[Antwort]
Variablen • Variable
sind vom Typ der Menge, aus der sie Werte annehmen können.
Syntax:<variable> “:“ <type><varliste> “:“ <type><varliste> “:“ <Wertebereich bzw.
Menge>
Konstanten• Konstante
sind Variablen, deren Ausprägung auf einen Wert beschränkt sind.
kreditlimit : kreditlimit = 1000
Funktionen• Spezialform der Relation• Lösungsmenge ist eindeutig• Abbildung Wertebereich (domain)
auf Bildbereich (range) i.Z.: dom f, ran f
Funktionen (1)Funktionsdefinition
someEven: y: | y > 0 someEven = 2*y
Funktionen (2)
X Y X YTotale Funktion
Partielle Funktion
Funktionen (3)
Funktionen (4)Injektiv:
Surjektiv:
Bijektiv:
X
X
X
Y
Y
Y
Generische Funktionen• Eine Funktion die für verschiedene
Typen deklariert wird
_ _ : (X x X) S,T: X S T (x:X x S x T)
[X]Generischer Parameter
Vielen Dank für die Aufmerksamkeit!!!Folien unter:www.edu.uni-klu.ac.at/~sschoenh/Spezi_Praesentation.ppt