Programmkorrektheitsbeweis: Axiomatische Methode nach Hoare

Axiomatische Methode Die axiomatische Methode wird bereits während der Programmierung vorbereitet. An wichtigen Stellen des Programms werden vom Programmierer Zusicherungen eingefügt. Hierdurch wird das Programm in Abschnitte aufgeteilt: z.B. wichtige Teilaufgaben oder Sinnabschnitte. Für diese Teile wird dann einzeln und auf einander aufbauend die Korrektheit nachgewiesen. Kann der Korrektheitsbeweis nicht erbracht werden, bedeutet dies jedoch nicht zwangsläufig, daß das Programm Fehlerhaft ist. Es kann auch heißen, daß die Zusicherungen Fehlerhaft sind.

Teilprogramm

Axiomatische Methode	Die axiomatische Methode wird bereits während der Programmierung vorbereitet. An wichtigen Stellen des Programms werden vom Programmierer Zusicherungen eingefügt. Hierdurch wird das Programm in Abschnitte aufgeteilt: z.B. wichtige Teilaufgaben oder Sinnabschnitte. Für diese Teile wird dann einzeln und auf einander aufbauend die Korrektheit nachgewiesen. Kann der Korrektheitsbeweis nicht erbracht werden, bedeutet dies jedoch nicht zwangsläufig, daß das Programm Fehlerhaft ist. Es kann auch heißen, daß die Zusicherungen Fehlerhaft sind.

	Die Aufspaltung in Teilprogramme wird deshalb vorgenommen, weil es im allgemeinen sehr schwierig oder gar unmöglich ist, die Korrektheit für ein ganzes Programm nachzuweisen. Außerdem ist diese Methode einfacher anzuwenden als die Methode der Induktiven Zusicherung, bei der vor und nach jeder Anweisung eine Zusicherung eingefügt wird. Die Korrektheit der einzelnen Teile kann auf verschiedenste Art und Weise nachgewiesen werden, die beiden Folgenden sind jedoch die gängigsten.

Die Aufspaltung in Teilprogramme wird deshalb vorgenommen, weil es im allgemeinen sehr schwierig oder gar unmöglich ist, die Korrektheit für ein ganzes Programm nachzuweisen. Außerdem ist diese Methode einfacher anzuwenden als die Methode der Induktiven Zusicherung, bei der vor und nach jeder Anweisung eine Zusicherung eingefügt wird. Die Korrektheit der einzelnen Teile kann auf verschiedenste Art und Weise nachgewiesen werden, die beiden Folgenden sind jedoch die gängigsten.

Methode der schwächsten Vorbedingung	Bei dieser Art die Korrektheit einer Anweisung, Prozedur oder eines Programms nachzuweisen wird das Programm rückwärts durchgearbeitet: Es wird jeweils überprüft, welche Vorbedingungen zu der zugesicherten Nachbedingung führen können. Ist die zugesicherte Vorbedingung in der Menge der möglichen Vorbedingungen enthalten, so ist der zu prüfende Abschnitt korrekt.

Methode der stärksten Nachbedingung	Bei dieser Methode wird die Korrektheit auf genau umgekehrte Weise nachgewiesen, wie bei der Methode der schwächsten Vorbedingung. Von Vorne nach Hinten wird jeweils geprüft, welche Ergebnisse der zu prüfende Abschnitt unter der zugesicherten Vorbedingung liefern kann. Sind diese in der zugesicherten Nachbedingung enthalten, ist die Korrektheit des Abschnitts nachgewiesen.

Beispiel für das Einfügen von Zusicherungen