This flashcard is just one of a free flashcard set. See all flashcards!

Abstrakte Datentypen als algebraische Strukturen
formale Spezifikation des Verhaltens von Modulen
Verifikation der Implementieren


Vorgehen
1) Strukturieren der Spezifikation:Alle Schnittstellen eines Systems identifizieren.
Miteinander kommunizierende Teile herausfinden
Notwendige Operationen informell beschreiben.
2) Benennen der Spezifikation:Alle abstrakten Datentypen einer Spezifikation mit Namen
versehen (z.B. Liste) und entscheiden, ob sie generische Parameter benötigen.
3) Auswahl der Operationen:Bezeichnung aller Operationen festlegen.
4) Informelles Spezifizieren der Operation:Identifizierte Operationen sowie deren Auswirkungen auf System beschreiben.
5) Definieren der Syntax:Für jede identifizierte Operation Syntax formal beschreiben.
Alle Operationen zusammen mit ihren Parametern definieren. Syntax gesamter
Spezifikation: Zusammensetzung aller abstrakten Datentypen.
6) Definieren der Semantik:Definition der Semantik der Operationen: Zutreffende Bedingungen
(Axiome) für verschiedene Kombinationen von Operationen beschreiben.

Algebraische Spezifikation eines abstrakten Datentyps besteht aus Syntax- und Semantikteil:
●Syntax:Menge von Vereinbarungen von Zugriffsoperationen:
−Operationsname: Definitionsbereich Wertebereich.
●Semantik:Menge von Gleichungen, die Beziehungen zwischen Eingabe- und Rückgabewerten verschiedener Operationen in Form von Axiomen beschreiben.




Unterscheidung zwischen:

verändernde Operation / inspizierende Operation


Beispiel


Erweiterung der algebraischen
Spezifikation String um Konstanten 'a‘, 'b'
von Typ Char (formal: nullstelligeOperation a: () 'a').

equal (add (s, 'a'), add (s, 'b')) = false?
Lässt sich nicht bestimmen:

Vervollständigung von String durch zusätzliche Operation
equalC : Char, Char Bool
mit den Axiomen:
equalC ('a','a') = true
equalC ('a','b') = false
equalC ('b','a') = false
equalC ('b','b') = true
und der Ersetzung des Axioms
equal (add (s1,c), add (s2,c)) = equal (s1,s2)
durch
equal (add (s1,c1), add (s2,c2)) = equal (s1,s2) ∧equalC (c1,c2)


„Korrekt“ ?=> Die o.g. Gleichungen sind intuitiv korrekt...
… allerdings nur, wenn bestimmte Annahmen an die Intuition erfüllt sind (die im Rahmen von
Schritt 4 des Vorgehens bereits vorab informell spezifiziert worden sein sollten). Zum
Beispiel:
• Das Axiom „append (s1, add(s2,c)) = add (append(s1,s2),c)“ setzt voraus, dass die
intendierten Implementierungen von append(s1,s2) und add (s,c) konsistent bezüglich
der Reihenfolgen von s1 und s2 bzw s und c sein sollen (z.B. append(s1,s2)=[s1::s2] und
add(s,c)=[s::c] oder append(s1,s2)=[s2::s1] und add(s,c)=[c::s], aber nicht append(s1,s2)=[s1::s2]
und add(c,s)=[c::s], wobei [s1::s2] die Konkatenation von s1 gefolgt von s2 ist).
• Das Axiom „isEmpty(add (s,c)) = false“ setzt voraus, dass es kein „leeres“ Zeichen geben
soll.


Vollständig ?   Nein. Zum Beispiel: Die Gleichungen implizieren nicht:    equal(s1,s2) = false (für s1#s2 mit length(s1)=length(s2))
obwohl dies intuitiv gelten sollte.

Anmerkung:  Kommutativität von equal folgt allerdings schon aus den Folien der vorigen Folie
(Beweis per Induktion).