Die Spezifikation des Sprachkonstrukts C sieht folgendermaßen aus:
{P} C {Q}
Dies bedeutet, dass wenn P direkt vor der Ausführung von C wahr ist, dann ist Q direkt nach der Ausführung von C wahr. Allerdings werden nicht alle Aktionen von C spezifiziert. In dem Beispiel {y != 0} x := 1 / y {x = 1 / y} wird in der Nachbedingung nicht auf y eingegangen, aber nach dem Ausführen von x := 1 / y ist natürlich y != 0, da y ja gar nicht geändert wurde.
Man benötigt eine Beziehung zwischen P und Q für das Konstrukt C. Da Programmieren zielorientiert ist, d.h. der Programmierer weiss, was nach dem Ausführen von C wahr sein soll, ist die Nachbedingung Q gegeben. Nun muss der Programmierer das Sprachkonstrukt C so entwerfen/programmieren, dass es für die Vorbedingung P gilt. Dieses Vorgehen sieht rückwärts aus, ist aber direkte Folge des Zielorientierten bei Programmiersprachen.
Für das Beispiel {P} x := 1 / y {x = 1 / y} gibt es viele Vorbedingungen, z.B. y < 0, y > 0, y > 5, y != 0, aber es gibt nur eine schwächste Vorbedingung:
y != 0
y > 0 und y < 0 sind beide stärker als y != 0, da beide y != 0 implizieren.
Denn P ist per Definition schwächer als R, wenn R => P.
Die Schreibweise von der schwächsten Vorbedingung (englisch: weakest precondition)
ist:
wp(C, Q)
Die axiomatische Spezifikation der Semantik des Sprachkonstrukts C
{P} C {Q}
gilt nur, wenn P die schwächste Vorbedingung für C und Q ist. Es gilt also:
{P} C {Q} nur, wenn P → wp(C, Q)
Die axiomatische Semantik des Sprachkonstrukts C wird von Aussage zu Aussage als Funktion wp(C, _) definiert. Die Funktion wp(C, _) ist ein Prädikatentransformator, sie nimmt ein Prädikat, die Nachbedingung, als Übergabeparameter und gibt ein Prädikatenergebnis, die Vorbedingung, zurück. Somit arbeitet auch diese Funktion rückwärts, da sie die Nachbedingung nimmt und die Vorbedingung gibt.
Angewendet auf die Beispiele bedeutet dies:
wp(x := 1 / y, x = 1 / y) = {y !=0}
wp(x := x + 1, x > 0) = {x > -1}
wp(x := x + 1, x = A) = {x = A - 1}
Aber es wurde noch nicht gesagt, wie wp berechnet werden kann. Um die Semantik eines Programmes, einer Anweisung oder eines Sprachkonstrukts komplett zu bestimmen, muss man wp(x := E, Q) für jede beliebige Nachbedingung Q bestimmen können.
Es gibt vier Gesetze für die schwächste Vorbedingung wp:
Gesetz des ausgeschlossenen Wunders:
wp(C, false) = false
Ein Programmkonstrukt C kann nichts tun, damit aus false true wird.
Distributivität der Konjunktion:
wp(C, P and Q) = wp(C, P) and wp(C, Q)
Gesetz der Monotonität:
if Q → R then wp(C, Q) → wp(C, R)
Distributivität der Disjunktion:
wp(C, P) or wp(C, Q) → wp(C, P or Q)