Elemente einer Z-Spezifikation
Spezifikation und Verifikation PRWS 03/04Auer AngelikaHarrich MichaelaSchnhart SabrinaGruppe 4
Struktur einer Z-Spezifikation
Basic Types, Globale Constants, User defined sets[ARZT, PATIENT]
maxAerzte: maxAerzte = 5
RESULT::= OK | NOK
State SpacePrdikateDeklarationenBezeichnungArztpraxis
Operationsschemata (1)Spezifieren die ber dem Zustandsraum definierten OperationenEine Operation wird durch ein gewhnliches Schemata beschriebenDie Operation wird nicht explizit deklariert
Operationsschemata (2)Operationsname = SchemanameParameter: - x?: Eingabeparameter - y!: AusgabeparameterZustnde: s: Zustand vor der Operation s: Zustand nach der Operation
Operationsschemata (3)Operationsschemata gliedern sich in Preconditions mssen vor der Operationsausfhrung erfllt seinAktion (Transformation) Spezifizierung der Zustandsraumnderung, die durch diese Operation bewirkt werden sollPostconditons mssen nach der Operationsausfhrung erfllt sein
OperationsschematazustandsvernderndAufnahmeArztOK
Arztpraxisdoktor?: ARZTantwort!: RESULTdoktor? doktoren#doktoren < maxAerztedoktoren = doktoren {doktor?}antwort! = OK
OperationsschematazustandserhaltendAufnahmeArztNOK
Arztpraxisdoktor?: ARZTantwort!: RESULTdoktor? doktoren#doktoren maxAerzteantwort! = NOK
Initialzustandbeschreiben gltige initiale Zustnde des Systemsbeinhalten Wertzuweisungen, die die Constraints des Zustandraumes erfllen mssen
InitArztpraxis
Arztpraxisdoktoren = patienten =
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, grn Intensional: mit Hilfe von Prdikaten FERIALMONAT = {x: MONAT | x Jul, Aug, Sept}
Typen (1) Zusammenfassung jener Elemente, die durch einen Satz von Operationen nach gemeinsamen Regeln manipuliert werden knnen. Besteht aus Grundmenge gleichartiger Elemente. Ein Typ ist eine maximale Menge.
Typdefinitionen in Z Sehr eingeschrnkter Satz von vordefinieren Typen:
Weitere Typen werden aus given sets aufgebaut: [X,Y]; [Namen]; [Banken]; [Tiere];...
Typdefinition in Z (1) Wir knnen Vertreter in Mengendefinitionen auflisten. Fr generische Typen definieren wir jedoch Variablen, die Werte des jeweiligen generischen Typs annehmen. Bsp.: Tiere == Pferd, Tieger, Strau | Pferd, Tieger, Strau : [Tiere]
AufzhlungstypenAntwort ::= JA|NEIN
Dient als Abkrzung fr:
JA,NEIN : AntwortJA NEINantw: Antwort antw = JA antw = NEIN
[Antwort]
Variablen Variablesind vom Typ der Menge, aus der sie Werte annehmen knnen.Syntax: : : :
Konstanten Konstantesind Variablen, deren Ausprgung auf einen Wert beschrnkt sind.
kreditlimit : kreditlimit = 1000
Funktionen Spezialform der Relation Lsungsmenge 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)XYXYTotale FunktionPartielle Funktion
Funktionen (3)
Funktionen (4)Injektiv:
Surjektiv:
Bijektiv: XXXYYY
Generische FunktionenEine Funktion die fr verschiedene Typen deklariert wird[X]Generischer Parameter
Vielen Dank fr die Aufmerksamkeit!!!Folien unter:www.edu.uni-klu.ac.at/~sschoenh/Spezi_Praesentation.ppt
Top Related