close

Anmelden

Neues Passwort anfordern?

Anmeldung mit OpenID

Formale Spezifikation - TU Berlin

EinbettenHerunterladen
Formale Spezifikation
Object-Z
Beispiel
Typisierung
Formale Spezifikation
Object-Z
Beispiel
Typisierung
Was machen wir heute?
Methodische- und Praktische Grundlagen
der Informatik 3 – Softwaretechnik
WS 0809
➜ Formale Spezifikation
➜ Grunds¨atzliches zu Object-Z
Steffen Helke
➜ Bank-Beispiel-Spezifikation
¨
Andreas Mertgen, Georgy Dobrev (Leitung Ubungsbetrieb)
➜ Typen in Z / Object-Z
➜ Einordnung
Rojahn Ahmadi, Daniel G´
omez Esper´
on, Simon Rauterberg, Jennifer Ulrich
Fachgebiet Softwaretechnik
Technische Universit¨
at Berlin
Formale Spezifikation
Object-Z
Beispiel
Typisierung
Formale Spezifikation
Formale Spezifikation(ssprachen)
Object-Z
Beispiel
Typisierung
Formale Spezifikation(ssprachen)
Einige Vorteile...
Einige Vorteile...
erlauben abstrakte mathematische Beschreibung von Modellen
erlauben abstrakte mathematische Beschreibung von Modellen
Ungenauigkeiten und Mehrdeutigkeiten informeller
Anforderungen k¨onnen pr¨azisiert werden
Ungenauigkeiten und Mehrdeutigkeiten informeller
Anforderungen k¨
onnen pr¨azisiert werden
haben i.d.R. selbst eine formale Semantik
haben i.d.R. selbst eine formale Semantik
Werkzeugunterst¨
utzung (Typchecks, Beweise)
Werkzeugunterst¨
utzung (Typchecks, Beweise)
...und Nachteile
gew¨ohnungsbed¨
urftige Notationen
,,v¨ollig klare Sachverhalte” m¨
ussen explizit eingef¨
uhrt werden
MPGI 3 – Softwaretechnik
3
MPGI 3 – Softwaretechnik
3
Formale Spezifikation
Object-Z
Beispiel
Typisierung
Formale Spezifikation
Object-Z
Beispiel
Typisierung
Object-Z
Formale Spezifikation(ssprachen)
Einige Vorteile...
erlauben abstrakte mathematische Beschreibung von Modellen
Wichtige Eigenschaften:
Ungenauigkeiten und Mehrdeutigkeiten informeller
Anforderungen k¨onnen pr¨azisiert werden
haben i.d.R. selbst eine formale Semantik
zustandsorientierter Modellformalismus
Werkzeugunterst¨
utzung (Typchecks, Beweise)
mengen- und pr¨adikatenbasierte Beschreibung
Kapselung, Modularisierung
...und Nachteile
Strenge Typisierung
gew¨ohnungsbed¨
urftige Notationen
Referenzsemantik
,,v¨ollig klare Sachverhalte” m¨
ussen explizit eingef¨
uhrt werden
Formale Spezifikationen werden f¨
ur bestimmte Klassen von
Systemen gefordert (Zertifizierung)
MPGI 3 – Softwaretechnik
Formale Spezifikation
3
Object-Z
Beispiel
Typisierung
MPGI 3 – Softwaretechnik
4
Formale Spezifikation
Werkzeuge f¨ur Z und Object-Z
Object-Z
Beispiel
Typisierung
Werkzeuge f¨ur Z und Object-Z
... basieren meistens auf LATEX-Syntax ...
... basieren meistens auf LATEX-Syntax ...
F¨
ur Z:
F¨
ur Z:
Spezifikationssatz: LATEX-Stile (oz.sty, esz.sty), Word-Stile
Typcheck: fuzz (Oxford), esz (TU Berlin)
Spezifikationssatz: LATEX-Stile (oz.sty, esz.sty), Word-Stile
Typcheck: fuzz (Oxford), esz (TU Berlin)
Beweiser: Z/EVES, HOL-Z (TU Berlin, TU Bremen, Uni
Freiburg)
Beweiser: Z/EVES, HOL-Z (TU Berlin, TU Bremen, Uni
Freiburg)
Simulatoren: ZETA (TU Berlin)
Simulatoren: ZETA (TU Berlin)
F¨
ur Object-Z:
Typcheck: wizard (SVRC Australien)
Beweiser: OZ in Isabelle/HOL (SVRC TUB)
MPGI 3 – Softwaretechnik
5
MPGI 3 – Softwaretechnik
5
Formale Spezifikation
Object-Z
Beispiel
Typisierung
Formale Spezifikation
Object-Z
UML/RUP vs. Object-Z
Beispiel
Typisierung
UML/RUP vs. Object-Z
Object-Z Spezifikation kann als Fortsetzung von RUP
aufgefasst werden:
Pr¨azisierung von Eigenschaften (von Klassen), die in
UML-Modellen nicht erfasst wurden
Object-Z Spezifikation kann als Fortsetzung von RUP
aufgefasst werden:
Pr¨azisierung von Eigenschaften (von Klassen), die in
UML-Modellen nicht erfasst wurden
Alternative: z.B. Object Constraint Language (OCL) OMG
Syntax n¨aher an Programmiersprache
M¨ogliche Analysen noch Gegenstand der Forschung
MPGI 3 – Softwaretechnik
Formale Spezifikation
6
Object-Z
Beispiel
Typisierung
MPGI 3 – Softwaretechnik
Formale Spezifikation
Beispiel - Kreditkarten-Konten
6
Object-Z
Beispiel
Typisierung
Beispiel - Kreditkarten-Konten
Es soll ein System f¨
ur die Verwaltung von Kreditkarten-Konten
spezifiziert werden.
Es soll ein System f¨
ur die Verwaltung von Kreditkarten-Konten
spezifiziert werden.
Ein Konto hat einen ganzzahligen Kontostand.
¨
Jedem Konto ist ein Uberziehungskredit
zugeordnet. Es gibt
nur drei m¨
ogliche Werte: 1000, 2000 oder 5000 Euro. Das
Konto kann nicht dar¨
uber hinaus u
¨berzogen werden.
Der Stand des Kontos kann durch Einzahlungen oder
Abhebungen positiver Betr¨age ge¨andert werden.
Weiterhin soll es m¨
oglich sein, das gesamte Konto inkl.
¨
Uberziehungsrahmen durch Aufruf einer entsprechenden
Operation zu leeren.
MPGI 3 – Softwaretechnik
7
MPGI 3 – Softwaretechnik
7
Formale Spezifikation
Object-Z
Beispiel
Typisierung
CreditCard
(limit, balance, INIT , withdraw , deposit, withdrawAvail)
Formale Spezifikation
Object-Z
Beispiel
Typisierung
Beispiel2 - System mit zwei Kreditkarten-Konten
limit : N
limit ∈ {1000, 2000, 5000}
balance : Z
balance + limit ≥ 0
INIT
balance = 0
Das System soll eine Operation anbieten, um einen Betrag
von einer Karte abzubuchen.
withdraw
∆(balance)
Es soll m¨
oglich sein, einen (positiven) Betrag von der einen
Karte auf die andere zu u
¨bertragen.
amount? : N
amount? ≤ balance + limit
Weiterhin soll eine Karte durch eine neue austauschbar sein,
¨
wobei der Stand und der Uberziehungsrahmen
erhalten bleibt.
[Vorbedingung ]
balance = balance − amount?
deposit
∆(balance)
withdrawAvail
∆(balance)
amount? : N
amount! : N
balance = balance + amount?
amount! = balance + limit
Der maximal abbuchbare Betrag einer Karte soll auf die
andere Karte u
¨bertragen werden k¨
onnen.
balance = −limit
MPGI 3 – Softwaretechnik
Formale Spezifikation
8
Object-Z
Beispiel
Typisierung
MPGI 3 – Softwaretechnik
Formale Spezifikation
TwoCards
(totalbal, INIT , withdraw1 , transfer , withdrawEither , replaceCard1 , transferAvail)
c1 , c2 : CreditCard
∆
totalbal : Z
c1 = c2
Typisierung
Bestandteile einer Klasse
[abgeleitet]
Schnittstelle (visibility list)
totalbal = c1 .balance + c2 .balance
Konstanten (axiomatic definition)
withdraw1 =
b c1 .withdraw
Zustandsschema (unbenannt)
Attribut-Deklarationen und Invarianten
transfer =
b c1 .withdraw ∧ c2 .deposit
withdrawEither =
b c1 .withdraw [] c2 .withdraw
Initialbedingung (INIT )
Pr¨adikat u
¨ber Attribute
Operationen (benannte Schemata)
replaceCard1
∆(c1 )
card? : CreditCards
card? ∈
/ {c1 , c2 }
Delta-Liste
Eingaben/Ausgaben
Pr¨adikate:
card?.limit = c1 .limit ∧ card?.balance = c1 .balance
c1 = card?
MPGI 3 – Softwaretechnik
Beispiel
¨
Object-Z Uberblick
INIT
c1 .INIT ∧ c2 .INIT
transferAvail =
b c1 .withdrawAvail
9
Object-Z
Verkn¨
upfung von Operationen (Operationskalk¨
ul)
c2 .deposit
10
MPGI 3 – Softwaretechnik
11
Formale Spezifikation
Object-Z
Beispiel
Typisierung
Formale Spezifikation
Typsystem
Object-Z
Beispiel
Typisierung
Einfache Typen
1. Basistypen:
[PERSON]
definiert einen neuen Typ.
Die Menge PERSON enth¨alt alle Elemente dieses Typs
(sog. ,,maximale Menge”).
Ein vorgegebener Basistyp ist Z,
d.h. die (maximale) Menge des Typs der ganzen Zahlen.
Object-Z ist streng typisiert, d.h.
Alle Ausdr¨
ucke haben einen definierten Typ.
Alle Bezeichner m¨
ussen deklariert werden.
Ausdr¨
ucke/Bezeichner k¨
onnen nur miteinander identifiziert
werden, wenn ihre Typen ,,passen” .
In Z sind Typen durch Mengen definiert.
MPGI 3 – Softwaretechnik
Formale Spezifikation
12
Object-Z
Beispiel
Typisierung
MPGI 3 – Softwaretechnik
Formale Spezifikation
Einfache Typen
13
Object-Z
Beispiel
Typisierung
Mathematische Typkonstruktoren
1. Basistypen:
[PERSON]
definiert einen neuen Typ.
Die Menge PERSON enth¨alt alle Elemente dieses Typs
(sog. ,,maximale Menge”).
Ein vorgegebener Basistyp ist Z,
d.h. die (maximale) Menge des Typs der ganzen Zahlen.
3. Kartesische Produkte:
Sind M und N Mengen, so ist auch M × N eine Menge:
Die Menge aller Paare (m, n) mit m ∈ M und n ∈ N.
Frage: Was ist der Typ dieser Menge von Paaren?
2. Datentypen:
NACHRICHT ::= Ok | Fehler
definiert einen Typ durch Aufz¨ahlung aller m¨oglichen Werte
(garantiert unterschiedlich!).
MPGI 3 – Softwaretechnik
13
MPGI 3 – Softwaretechnik
14
Formale Spezifikation
Object-Z
Beispiel
Typisierung
Formale Spezifikation
Object-Z
Mathematische Typkonstruktoren
Beispiel
Typisierung
Mathematische Typkonstruktoren
3. Kartesische Produkte:
Sind M und N Mengen, so ist auch M × N eine Menge:
Die Menge aller Paare (m, n) mit m ∈ M und n ∈ N.
Frage: Was ist der Typ dieser Menge von Paaren?
3. Kartesische Produkte:
Sind M und N Mengen, so ist auch M × N eine Menge:
Die Menge aller Paare (m, n) mit m ∈ M und n ∈ N.
Frage: Was ist der Typ dieser Menge von Paaren?
4. Potenzmengen:
Ist M eine Menge, so ist auch P M eine Menge: Die Menge
aller Teilmengen von M.
Wenn typ(m) = t mit m ∈ M, dann ist P t der Typ von M.
Frage: Welchen Typ hat Z?
MPGI 3 – Softwaretechnik
Formale Spezifikation
14
Object-Z
Beispiel
Typisierung
MPGI 3 – Softwaretechnik
Formale Spezifikation
14
Object-Z
Z-Typkonstruktor
Beispiel
Typisierung
Object-Z Typkonstruktor
6. Klassendeklaration:
C
5. Schematypen:
. . . sind durch Mengen von sog. Bindings beschrieben.
S
x1 : X1
..
.
...
... induziert einen neuen Typ.
Die Menge C enth¨alt alle m¨
oglichen Instanzen von C .
(Genauer: Identit¨aten, nicht Zust¨ande!)
xn : Xn
P(x1 , . . . , xn )
Hier ist die Reihenfolge der Elemente egal, Namen sind
relevant.
MPGI 3 – Softwaretechnik
15
MPGI 3 – Softwaretechnik
16
Formale Spezifikation
Object-Z
Beispiel
Typisierung
Object-Z Typkonstruktor
6. Klassendeklaration:
C
...
... induziert einen neuen Typ.
Die Menge C enth¨alt alle m¨
oglichen Instanzen von C .
(Genauer: Identit¨aten, nicht Zust¨ande!)
Dies sind alle M¨oglichkeiten in Object-Z Typen zu formen.
Konsequenz: Die meisten Namen, die in Deklarationen hinter “:” stehen,
bezeichnen keine Typen (maximale Mengen!), sondern nur Teilmengen solcher Typen.
Beispiel: N == {x : Z | x ≥ 0}, die Menge der nat¨
urlichen Zahlen
Frage: Wenn y ∈ N, welchen Typ hat dann y ?
MPGI 3 – Softwaretechnik
16
Document
Kategorie
Seele and Geist
Seitenansichten
1
Dateigröße
202 KB
Tags
1/--Seiten
melden