Hoare-Kalkül

Hoare-Logik (oder Hoare-Kalkül) ist ein Formales System, entwickelt von dem Britischen Informatiker C.A.R. Hoare und später verfeinert von Hoare und anderen Wissenschaftlern. Sie wurde 1969 in einem Artikel mit dem Titel "An axiomatic basis for computer programming" veröffentlicht. Der Zweck des Systems ist es, eine Mege von logischen Regeln zu liefern, die es erlauben, Aussagen über die Korrektheit von Computer-Programmen zu treffen und sich dabei der mathematischen Logik bedienen. Hoare knüpft an frühere Beiträge von Robert Floyd an, der ein ähnliches System für Flussdiagramme veröffentlichte.

Das zentrale Element der Hoare-Logik ist das Hoare-Triple, das beschreibt, wie ein Programmteil den Zustand einer Berechnung verändert:

\{P\}\;S\;\{Q\}

Dabei nennt man P und Q Zusicherungen (englisch assertions). S ist ein Programmsegment. P heißt die Vorbedingung (englisch precondition) , Q heißt die Nachbedingung (englisch postcondition). Zusicherungen sind Formeln der Prädikatenlogik. Ein Tripel kann auf folgende Weise verstanden werden: Falls P gilt für den Programmzustand vor der Ausführung von S, dann gilt Q danach. Falls S nicht terminiert, dann gibt es kein "danach", also kann in diesem Fall Q jede beliebige Aussage sein. Tatsächlich kann man für Q die Aussage false wählen, um auszudrücken, dass S nicht terminiert. Man spricht hier von "partieller Korrektheit". Falls S terminiert und nach Terminierung ist Q wahr, dann spricht man von "totaler Korrektheit". Die Terminierung muss unabhängig bewiesen werden.

Die Hoare-Logik besteht aus Axiomen und Ableitungsregeln für alle Konstrukte einer einfachen imperativen Programmiersprache:

Das Zuweisungsaxiom besagt, dass nach einer Zuweisung jede Aussage für die Variable gilt, welche vorher für die rechte Seite der Zuweisung galt:

{\frac {}{\{P[E/x]\}\ x:=E\ \{P\}}}

$P[E/x]$ ist die Aussage, die dadurch entsteht, dass man in $P$ jedes Vorkommen von $x$ durch $E$ ersetzt.

Genau genommen ist das Zuweisungsaxiom kein einzelnes Axiom, sondern ein Schema für eine unendliche Menge von Axiomen, denn $x$ , $E$ und $P$ können jede mögliche Form annehmen, und $P[E/x]$ kann daraus konstruiert werden.

Ein Beispiel für ein durch das Zuweisungsaxiom beschriebenes Tripels ist:

\{x+1=43\}\ y:=x+1\ \{y=43\}

Sequenzregel

{\frac {\{P\}\ S\ \{Q\}\ ,\ \{Q\}\ T\ \{R\}}{\{P\}\ S;T\ \{R\}}}

Eine Regel kann auf folgende Weise angewendet werden: Wenn die über dem Strich stehenden Aussagen bewiesen worden sind, kann die unter dem Strich stehende Aussage auch als bewiesen angesehen werden.

Betrachtet man zum Beispiel die folgenden beiden Aussagen, die aus dem Zuweisungsaxiom folgen

\{x+1=43\}\ y:=x+1\ \{y=43\}

und

\{y=43\}\ z:=y\ \{z=43\}

kann man die folgende Aussage daraus folgern:

\{x+1=43\}\ y:=x+1;z:=y\ \{z=43\}

Auswahlregel (if-then-else-Regel)

{\frac {\{B\wedge P\}\ S\ \{Q\}\ ,\ \{\neg B\wedge P\}\ T\ \{Q\}}{\{P\}\ if\ B\ then\ S\ else\ T\ \{Q\}}}

Iterationsregel (while-Regel)

{\frac {\{P\wedge B\}\ S\ \{P\}}{\{P\}\ while\ B\ do\ S\ od\ \{\neg B\wedge \ P\}}}

Konsequenzregel

{\frac {P^{\prime }\rightarrow \ P\ ,\ \lbrace P\rbrace \ S\ \lbrace Q\rbrace \ ,\ Q\rightarrow \ Q^{\prime }}{\lbrace P^{\prime }\ \rbrace \ S\ \lbrace Q^{\prime }\rbrace }}

Festzuhalten bleibt aber, dass es sich hierbei nur um die Regeln für die partielle Korrektheit handelt. Zur totalen Korrektheit, wie sie bei Programmen benötigt wird, die z.B. Atomkraftwerke steuern, muss man in der While-Regel noch zwei Sachen hinzufügen.

Zum Einen einen Terminierungsausdruck, den man in einer Freien Variablen (z) abspeichert. Nach jedem Schleifendurchlauf muss sichergestellt sein, dass der Terminierungsausdruck (t) echt kleiner geworden ist. Das Zweite ist, dass die zu bestimmende Invariante dahingehend modifiziert werden muss (bzgl. der Invariante der partiellen Korrektheit), dass aus der Invariante folgt, dass der Terminierungsausdruck stets größer oder gleich 0 ist.

Whileregel für totale Korrektheit:

{\frac {\{P\wedge b\wedge z=t\}\ S\ \{P\wedge z>t\},I\rightarrow t\geq 0}{\{P\}\ while\ b\ \{S\ \}\{\neg b\wedge \ P\}}}

Siehe auch

References

C. A. R. Hoare. "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576-585, October 1969. [1]