Hoare-Kalkül

Wenn ein Programmsegment ${\displaystyle S}$ keine Variablen verändert, so ändern sich auch die Zusicherungen nicht, es gilt also Nachbedingung gleich Vorbedingung:

${\displaystyle {\frac {}{\{P\}S\{P\}}}}$

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

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

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

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

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

${\displaystyle \{x+1=43\}\ y:=x+1\ \{y=43\}.}$

Um sequentielle Programme zu analysieren, können die einzelnen Tripel nach folgender Regel verknüpft werden:

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

Diese 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

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

und

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

kann man die folgende Aussage daraus folgern:

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

Es gilt folgende Regel für Auswahlkonstrukte mit 2 Auswahlmöglichkeiten:[3]

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

Die Regel beweist also sowohl den if-Zweig, als auch den else-Zweig. Hat eine if-Abfrage keinen else-Zweig, so verwendet man eine leicht modifizierte Version dieser Regel:

${\displaystyle {\frac {\{P\wedge B\}\ S\ \{Q\}\ ,\ P\wedge \neg B\Rightarrow Q}{\{P\}\ \mathrm {if} \ B\ \mathrm {then} \ S\ \{Q\}}}}$

${\displaystyle {\frac {\{I\wedge B\}\ S\ \{I\}}{\{I\}\ \mathrm {while} \ B\ \mathrm {do} \ S\ \mathrm {done} \ \{I\wedge \neg B\}}}}$

Hierbei wird ${\displaystyle I}$ als die Schleifeninvariante bezeichnet, die sowohl vor, während und nach Ausführung der Schleife gültig ist. Eine Invariante muss manuell ermittelt werden.

${\displaystyle {\frac {P\Rightarrow \ P^{\prime },\ \lbrace P^{\prime }\rbrace \ S\ \lbrace Q^{\prime }\rbrace \ ,\ Q^{\prime }\Rightarrow \ Q}{\lbrace P\rbrace \ S\ \lbrace Q\rbrace }}}$

Die Konsequenzregel erlaubt es, die Vorbedingung zu verstärken und die Nachbedingung abzuschwächen und so die Anwendung anderer Beweisregeln zu ermöglichen. Insbesondere kann man auch die Vor- oder Nachbedingung durch eine äquivalente logische Formel ersetzen. Beispiel:

${\displaystyle \lbrace true\rbrace \ x:=0\ \lbrace x\geq 0\rbrace \ }$ ist partiell korrekt, denn

${\displaystyle {\frac {true\Rightarrow 0=0,\lbrace 0=0\rbrace \ x:=0\ \lbrace x=0\rbrace ,\ x=0\Rightarrow x\geq 0}{\lbrace true\rbrace \ x:=0\ \lbrace x\geq 0\rbrace }}.}$

${\displaystyle {\frac {\{I\wedge B~\wedge ~t=z\}\ S\ \{I~\wedge ~t<z\},~I\Rightarrow t\geq 0}{\{I\}\ \mathrm {while} \ B\ \mathrm {do} \ S\ \mathrm {done} \ \{I\wedge \neg B\}}}}$

Hierbei ist ${\displaystyle t}$ ein Term, ${\displaystyle I}$ die Schleifeninvariante – also das, was in jedem Schleifendurchlauf gilt – und ${\displaystyle z}$ eine Variable, die in ${\displaystyle B}$, ${\displaystyle t}$, ${\displaystyle S}$ und ${\displaystyle I}$ nicht frei vorkommt. Sie dient dazu, den Wert des Terms vor der Schleife mit dem nach der Schleife zu vergleichen. Die Bedingung ${\displaystyle I\Rightarrow t\geq 0}$ stellt sicher, dass ${\displaystyle t}$ nicht negativ wird. Die Idee hinter der Regel ist, dass, wenn ${\displaystyle t}$ mit jedem Schleifendurchlauf abnimmt, aber nie kleiner als Null wird, die Schleife irgendwann enden muss. ${\displaystyle t}$ muss dabei aus einer fundierten Menge sein.