Axiomatische Semantik der Beispielsprache

Übersicht: Axiomatische Semantik der Beispielsprache

• Axiomatische Semantik der Beispielsprache
• Assignment Statements
• Assignment Statements Beispiele
• Statement-Listen
• Statement-Listen Beispiel
• If-Anweisung
• If-Anweisung Beispiel
• While-Schleifen
• While-Schleifen Beispiele

Axiomatische Semantik der Beispielsprache

P → L
L → L1 ';' L2 | S
S → I ':=' E
    | 'if' E 'then' L1 'else' L2 'fi'
    | 'while' E 'do' L 'od'

Legende:

Assignment Statements

Die Definition von assignment statements ist folgende:

wp(I := E, Q) = Q[E/I]

Die neue Notation Q[E/I] bedeutet, dass alle E alle freien Vorkommen von I ersetzt. Freie Vorkommen bedeutet, dass I nicht drch All- oder Existenzquantoren gebunden ist. (Ein Beispiel für freie und nicht-freie Vorkommen: Q = (for all i, a[i] > a[j]) j ist frei, i ist gebunden)
Wenn keine Quantoren vorhanden sind, dann bedeutet Q[E/I] einfach, dass alle I durch E ersetzt werden.

Assignment Statements Beispiele

Beispiel 1:

Statement-Listen

Für Statement-Listen gilt folgendes:

wp(L1; L2, Q) = wp(L1, wp(L2, Q))

Das bedeutet, dass die Vorbedingung von L2 die Nachbedingung von L1 ist. Also muss man wieder rückwärts gehen, nämlich die Vorbedingung von L2 ausrechnen, diese dann benutzen, um die Vorbedingung von L1 zu berechnen. Die Positionen von L1 und L2 werden nicht, wie das in der denotationellen Semantik passiert, getauscht.

Statement-Listen Beispiel

Ergebnis:
wp(y := 3 * x + 1; x := y + 3, x < 10) = (x < 2)

If-Anweisungen

Die Semantik der If-Anweisung in der Beispielsprache war:

if E then L1 else L2 fi

Dies bedeutet, dass wenn E > 0 ist, dann wird L1 ausgeführt, bei E <= 0 wird L2 ausgeführt. Also:

wp(if E then L1 else L2 fi, Q) = (E > 0 → wp(L1, Q)) and (E <= 0 → wp(L2, Q))

If-Anweisungen Beispiel

wp(if x then x := 1 else x := -1 fi, x = 1) = (x > 0 → wp (x := 1, x = 1)) and (x <= 0 → wp(x := -1, x = 1))

Als nächtes werden die schwächsten Vorbedingungen ausgerechnet:

wp(x := 1, x = 1) = Q[1 / x] = (1 = 1)
wp(x := -1, x = 1) = Q[-1 / x] = (-1 = 1)

Setzt man dies in die erste Gleichung ein, erhält man

Ergebnis:
wp(if x then x := 1 else x := -1 fi, x = 1) = (x > 0)

While-Schleifen

Die while Schleifen

while E do L od

wird ausgeführt, so lange E > 0 ist. While-Schleifen sind das schwierigste Konstrukt, da man für die Schleifendurchläufe eine induktive Definition auf Basis der Schleife geben muss.

Hi(while E do L od, Q)

sei der Ausdruck, dass die Schleife i mal ausgeführt wird und dann in einem Status, der Q befriedigt terminiert. Dann ist für null Schleifendurchläufe

H0(while E do L od, Q) = E <= 0 and Q

und für einen Schleifendurchlauf

Verallgemeinert man diesen Ansatz, kommt man zu

Hi+1(while E do L od, Q) = E > 0 and wp(L, Hi(while E do L od, Q))

Nun definiert man

wp(while E do L od, Q) = es gibt ein i, für das gilt Hi(while E do L od, Q)

Diese Definition benötigt allerdings terminierende while-Schleifen. Nichtterminierende while-Schleifen haben immer false als Vorbedingung, da die Nachbedingung nie wahr werden kann:

wp(while 1 do L od, Q) = false, für alle L und Q

While-Schleifen Beispiele

Für diese Beispiele geht man von Integer-Werten aus. Ferner werden Vergleiche (da in der Beispielsprache der Datentyp boolean fehlt) nach C-Syntax (true bedeutet >= 1, false bedeutet < 1) ausgewertet: wird ein Vergleich als true ausgewertet, dann kommt der Wert 1 heraus, bei false 0.

Beispiel 1:

Gegeben ist die folgende while-Schleife mit Nachbedingung

while y != x do y := y + 1 od {y = x}

Um eine Vorbedingung zu finden kann man eine Methode ähnlich der Ermittlung der induktiven Hypothese in der mathematischen Induktion benutzen: Es wird die Bedingung für ein paar Fälle berechnet, mit der Hoffnung, dass man ien Muster erkennt.

Daraus kann man erkennen, dass

Hi(while y != x do y := y + 1 od, x = y) = ((y < x) and (i >= 1))
und
H0 = (y = x)

Kombiniert man beides, so erhält man

Hi = ((y <= x) and (i >= 0))

Diese while-Schleife terminiert immer, da, egal wie viel kleiner y als x ist, irgendwann ist y = x erreicht.

Beispiel 2:

while s > 1 do s := s / 2 od{s = 1}

Durch den gleichen Ansatz rechnet man H0 bis H3 aus:

Daraus kann gefolgert werden, dass

Hi = ((s >= 2i) and (s < 2i+1))

Im Vergleich zum ersten Schleifen-Beispiel hat man mit dieser Methode nicht die schwächste Vorbedingung gefunden. Die Vorbedingung (s > 1) ist z.B. wesentlich schwächer.