Die symbolische Ausführung ist eine Validierungsmethode, mit der die partielle Korrektheit eines Programmfragments gezeigt werden kann. Das Verfahren verwendet zwei Prädikate, die Vor- und die Nachbedingung. Es wird versucht zu beweisen, dass wenn vor der Ausführung des Programmfragments die Vorbedingung gilt, nach der Ausführung die Nachbedingung erfüllt ist.

Zunächst muss im ersten Schritt des Verfahrens der Ausführungsbaum des Programmstücks aufgestellt werden. Der Ausführungsbaum ist ein Baum mit drei verschiedenen Knotentypen:

• Startzustand und Endzustände werden durch Kreise repräsentiert,
• gewöhnliche Anweisungen durch Rechtecke und
• Verzweigungen durch Rauten.

Startzustand, Endzustände und Anweisungsknoten werden mit Variablenbelegungen (nach Ausführung der Anweisung) annotiert. An die Kanten des Baums wird die gültige Vor- bzw. Nachbedingung geschrieben, diese Bedingung wird Pfadbedingung genannt.

Folgendes Beispielprogramm berechnet den Betrag des Werts der Variablen x:

  if x < 0 then y = -x; else y = x;.

Das Beispielprogramm führt zu dem Ausführungsbaum in Abbildung 1.

Es ist nun zu zeigen, dass die in der Spezifikation gegebene Nachbedingung aus der Variablenbelegung und Pfadbedingung jedes Endknotens folgt.

Allgemein lässt sich das Verfahren der symbolischen Ausführung beschreiben, in dem man betrachtet, wie die symbolische Ausführung bei einfachen Anweisungen, Sequenzen, Fallunterscheidungen und Schleifen durchgeführt wird.


Einfache Anweisung

Für eine einfache Anweisung S mit der Vorbedingung P und der Nachbedingung Q (kurz: {P} S {Q}) ermittelt man zunächst die Menge der beteiligten Variablen. Der Einfachheit halber sei das nur die Variable x. Man bildet zu jeder Variable eine neue, bisher nicht verwendete Variable, hier z.B. a. Die Substitution sub ist dann [x/a], die Belegung E1 ist [x:a] und man erhält den in Abbildung 2 gezeigten Ausführungsbaum. Im Endknoten gilt sub(P) & E2. Aus der letzten Pfadbedingung und der letzten Belegung muss nun die Nachbedingung Q folgen.


Sequenz

Sequenzen von Anweisungen werden entsprechend behandelt (siehe Abbildung 3).

Das Code-Fragment

  {x > 2}
  y = c0
  y = y * x + c1
  y = y * x + c2
  x = x + 2

führt (wenn man c0, c1 und c2 als Konstanten betrachtet) zu den folgenden Belegungen:

  E1 = [x:a, y:b]
  E2 = [x:a, y:c0]
  E3 = [x:a, y:(c0 * a + c1)]
  E4 = [x:a, y:((c0 * a + c1) * a + c2)]
  E5 = [x:(a + 2), y:((c0 * a + c1) * a + c2)]

Die Vorbedingung x > 2 wird zur Ungleichung a > 2, mit der alle Kanten im Ausführungsbaum annotiert werden.


Fallunterscheidung

Bedingte Anweisungen führen zu Verzweigungen im Ausführungsbaum (siehe Abbildung 4). Bei einer Verzweigung bleibt die Belegung gleich, aber die Pfadbedingung ändert sich.


Schleife

Schleifen werden gesondert behandelt. Zum Beweis, dass die Schleife

  {P} while c do {I} S1 end while S2 {Q}

das gewünschte Verhalten hat, wird eine Schleifeninvariante I eingeführt und es werden zwei getrennte Ausführungsbäume betrachtet.

Der erste Baum (Abbildung 5) beweist, dass die Schleifeninvariante aus der Vorbedingung folgt und verifiziert die Schleife für den Fall von Null Durchläufen. Der zweite Baum (Abbildung 6) beweist, dass die Schleifeninvariante tatsächlich eine Invariante ist.

Für die mit I bezeichneten Endknoten ist zu zeigen, dass die Invariante folgt, für die mit Q bezeichneten Endkonten muss die Nachbedingung folgen.

Abbildung 1: Ausführungsbaum für die Berechnung des Betrags.



Abbildung 2: Ausführungsbaum für eine einfache Anweisung.



Abbildung 3: Ausführungsbaum für eine Sequenz von Anweisungen.



Abbildung 5: Ausführungsbaum für die nicht durchlaufene Schleife.



Abbildung 4: Ausführungsbaum für eine Fallunterscheidung.



Abbildung 6: Ausführungsbaum für die Schleifeninvariante.