Jo Meder

(schaefer@inf.fu-berlin.de)

Berlin, 7.11.1995

Spezifikation leichtgemacht

am Beispiel eines ADT

Anhand eines Beispiels (Aufgabe 3, Blatt 2) sollen hier alle Teile einer formalen Spezifikation, wie sie in der Vorlesung vorgestellt wurde, noch einmal aufgeführt werden. Die Spezifikation gliedert sich in drei große Teile, nämlich Signatur, Modell und

Semantik.

Der Teil Signatur gibt an, wie der zu spezifizierende Typ benannt sein soll, welche Typen in der Spezifikation verwendet werden sollen und welche Operationen auf diesen Typen definiert werden. Im Modell-Teil der Spezfikation wird definiert welches Konstrukt (z.B. Mengen) als Modell für den in Frage stehenden ADT verwendet werden soll. Im letzten Teil (Semantik) wird durch die Angabe formaler Definitionen (axiomatisch / algebraisch) für die in der Signatur aufgezählten Operationen deren Funktionsweise definiert. Alternativ kann - nicht ganz so formal - auch modellierend spezifiziert werden. Dabei wird eine mögliche Implementation in einer Sprache (z.B. Miranda) mit den jeweils für die einzelnen Teile des Algorithmus geltenden Vor- und Nachbedingungen angegeben. Obwohl diese Methode auf den ersten Blick reizvoller erscheinen mag, da sie nicht ganz so formal vorgeht, wie die beiden anderen, ist sie auch gefährlicher in dem Sinne, daß die Vollständigkeit der Modellierung (außer bei wirklich konsequenter Anwendung von Vor- und Nachbedingungen) noch weniger leicht zu sichern ist, als bei der axiomatischen oder der algebraischen Spezifikation.

Das Beispiel Als Beispiel soll hier der in Aufgabe 3 von Blatt 2 zu spezifizierende Array-Typ verwendet werden.

• Signatur::
– Typ:: array_{T} [T]
– Sorten:: array_{T} T num
– Operationen::
▷ alloc: (num,num) → array_{T}
▷ store: (T,num,array_{T}) → array_{T}
▷ fetch: (num,array_{T}) → T
▷ bottom: (array_{T}) → T
▷ top: (array_{T}) → T
• Modell:: array_{T} = Abbildung a : {n ∈ ℕ} → t ∈ T
• abstrakte Invariante: (des Algorithmus)

– ∀ A ∈ array_{T} ∃l, n, m ∈ ℕ : A(n) ist definiert für l ≤ n ≤ m

(das heißt: Arrays sind endlich)
• Semantik::

– axiomatisch ( ˆ= algebraisch^{1})

– Axiome::

▷ ∀x ∈ T ▷ ∀a, b, p ∈ ℕ ▷ ∀a, b : a ≤ b

▷ alloc(a,b)=A, A ∈ array_{T}, |A|= b − a + 1
▷ fetch(p,store(x,p,alloc(a,b))=x

∀p : a ≤ p ≤ b

  fetch(p,store(x,p,alloc(a,b))=undefiniert

∀p : p < a ∨ p > b

▷ bottom(store(x,a,alloc(a,b))) = fetch(a,(store(x,a,alloc(a,b))))
▷ top(store(x,b,alloc(a,b))) = fetch(b,(store(x,a,alloc(a,b))))

– Abstraktionsfunktion und konkrete Invariante

– konkrete Invariante: (der Implementierung)

1 In der Literatur wird teilweise zwischen algebraischer und axiometischer Spezifikation unter-

schieden. In der Vorlesung werden die beiden Begriffe synonym verwendet.

▷ Z.B. Restriktionen bezüglich der Größe des Arrays oder seiner einzelnen Elemente. Die konkrete Invariante kann erst dann festgelegt werden, wenn die Repräsentation des ADT in der Implementierung feststeht, da sie sich gerade darauf bezieht. Beispiel:

(* Eine Beispielimplementierung in Modula...*)
TYPE T = CARDINAL;
(* konkrete Invariante: für alle t vom Typ T: t ist numerisch
und 0 <= t <= MAXCARDINAL^{2} *)
CONST ArrayMax = m; ArrayMin = n;
VAR ArrayRepr: ARRAY [ArrayMin..ArrayMax] OF T;
index: CARDINAL;
(* konkrete Invariante: ArrayMin <= index <= ArrayMax und
alle ArrayRepr[i] sind initialisiert und ArrayMin,ArrayMax
> 0, da index vom Typ CARDINAL ist*)
– Abstraktionsfunktion abstr::
▷ abstr:: array_{T} → partielle Abbildung a:a→T (siehe Modell)
▷ abstr:: alloc(a,b)=A, A∈array_{T}, a≤b →
sei M=Definitionsbereich von a, ∀m ∈ M: a ≤ m ≤ b
▷ abstr:: store → definiere Zuordnung
(Beispiel: store(x,p,Array) → sei a(p) = x)
▷ abstr:: fetch → werte Funktion aus (Beispiel: a(p))

▷ abstr:: top → t : t = a(p)∧ ∄p′ : (p′ < p ∧ a(p′) ist definiert) ▷ abstr:: bottom → t : t = a(p)∧ ∄p′ : (p′ > p ∧ a(p′) ist definiert)

– modellierend

▷ Hier könnte z.B. eine Miranda-Implementation der obigen Definitionen stehen. Wichtig ist, dabei immer die Vor- und Nachbedingungen der einzelnen Teile des Algorithmus mit anzugeben.

Was sich nun noch anschließen müßte, wären Überlegungen zur Korrektheit der algebraischen Spezifikation nach dem in der Vorlesung vorgestellten Modell: Seien X eine Operation auf array_{T} und p deren Parameter, so müßte gelten:

abstr (X (p)) = abstr (X) (abstr (p))

Beispiel: abstr(fetch(p))=abstr(fetch)(p) ↔ (fetch(p)=a ∈ T) = a(p)(∈ T) Ein Nachweis wäre für jede der spezifizierten Operationen zu führen und sei hier allen Beteiligten erspart.

2 In der auf Blatt 2, Aufgabe 3 geforderten Implementierung wäre diese Invariante unzulässig,

da der Array-Inhalt, also der Typ T, nicht von auf numerische Werte und vor allem nicht auf numerische Werte eines bestimmten Typs beschränkt war