Dieses Kapitel beschäftigt sich damit, wie man die Korrektheit von Programmen beweist. Das grundlegende Hilfsmittel hierfür ist der Hoare-Kalkül, der es erlaubt, Beweise systematisch aus schrittweisen Deduktionen zu konstruieren.
Der Hoare-Kalkül ist ein Beweisverfahren, bei dem Algorithmen Zusicherungen, engl. assertions, bekommen. Das sind logische Aussagen, welche das Programm nicht verändern, aber beim Ablauf des Programms an der jeweiligen Stelle erfüllt sein müssen. Es läge nahe, diese Zusicherungen einfach in das Programm einzufügen und zu schauen wie es sich beim Durchlaufen verhält. Der springende Punkt liegt allerdings nicht in der Erfüllung der Zusicherung für eine bestimmte Belegung der Argumente, sondern darin, dass die Zusicherung für alle möglichen erlaubten Belegungen erfüllt ist.
Zusicherungen befinden sich vor und hinter jeder Anweisung, infolge
auch vor und hinter jeder Sequenz von Anweisungen. Darin eingeschlossen
sind Kontrollanweisungen.
Man betrachtet nun eine Sequenz S für sich allein.
Diese kann auch aus einer einzigen Anweisung bestehen. Der
wesentliche Gegenstand des Kalküls ist das Hoare-Tripel
{P} S {Q}.
Hierbei sind P und Q Zusicherungen.
Die Zusicherung P ist die Vorbedingung,
engl. precondition, und Q ist die
Nachbedingung, engl. postcondition.
Es handelt sich um die logische Aussage, dass nach Ausführung der
Sequenz die Nachbedingung erfüllt ist, sofern vor der Ausführung die
Vorbedingung galt.
Eine Vorbedingung muss nicht in jedem Fall vorhanden sein.
Entfällt die Vorbedingung P, schreibt man
P = true. Für eine Ganzzahl x
gilt bspw.
{true} y := x*x; {y ≥ 0}.
Beweisen will man, dass eine Funktion das Ergebnis liefert, was man haben möchte. Man sagt, die Korrektheit des Programms ist zu verifizieren. Zunächst muss erst einmal notiert werden, was gewünscht ist. Hierfür wird der Signatur einer Funktion eine Nachbedingung und ggf. eine Vorbedingung hinzugefügt. Man spricht von einer Spezifikation der Funktion.
Man unterscheidet zwischen zwei unterschiedlich strengen Formen der Korrektheit:
Ein Programm terminiert, wenn es sich nicht in einer
Endlosschleife verfängt und keine divergierenden Befehle wie
panic!() aufgerufen werden.
Im Hoare-Kalkül beweist man zunächst die partielle Korrektheit. Die totale Korrektheit muss gesondert gezeigt werden. Es gibt aber auch eine Adaption des Kalküls, bei der zusätzlich die Terminierung von Schleifen bewiesen wird.
Zum Beweis der Gültigkeit der Zusicherungen muss man deduktive Schlussfolgerungen machen. Diese Schlussfolgerungen wurden in Form von Schlussregeln formalisiert. Eine Schlussregel beschreibt, welche Schlussfolgerung (Konklusion) aus einer bestimmte Gestalt von Voraussetzung (Prämisse) abgeleitet werden darf. Notiert sind Schlussregeln üblicherweise in dieser Form:
Prämisse ────────── Konklusion
Bedarf es für die Konklusion mehrerer Prämissen, schreibt man diese untereinander oder getrennt nebeneinander:
Prämisse1 Prämisse2 ────────── Konklusion |
Prämisse1, Prämisse2
────────────────────
Konklusion
|
Mit der Notation P[v := e] drücken wir aus, dass in der
Formel P jedes Vorkommen der Variable v
durch den Ausdruck e ersetzt wird.
Gemäß dem Zuweisungsaxiom ist die Zusicherung P
nach einer Zuweisung v := e; gültig, sofern
P[v := e] vor der Zuweisung erfüllt war. Diese
Konklusion benötigt keine Prämissen:
─────────────────────────
{P[v := e]} v := e; {P}
Kann man für beide Zweige einer Verzweigung zeigen,
dass die Zusicherung Q hinter dem jeweiligen Zweig
erfüllt ist, falls P davor galt, so muss
Q auch nach dem Ende der Verzweigung erfüllt sein,
falls P vor der Verzweigung galt.
{P ∧ B} S1 {Q}
{P ∧ ¬B} S2 {Q}
──────────────────────────────────
{P} if B then S1 else S2 end {Q}
Die Kompositionsregel besagt wie bei Sequenzen von Anweisungen schrittweise geschlussfolgert werden darf. Ohne diese Regel ergäbe das Unterfangen keinen Sinn.
Ein Programm bestehe aus zwei Teilsequenzen S1
und S2. Die Sequnez S1 ziehe die Zusicherung
Q nach sich, falls P galt. Die
Sequenz S2 ziehe R nach sich, falls
Q galt. Dann muss die Gesamtsequenz
S1; S2 die Zusicherung R nach sich ziehen,
falls P galt.
{P} S1 {Q}
{Q} S2 {R}
────────────────
{P} S1; S2 {R}
Sei B die Schleifenbedingung und S
der Schleifenrumpf. Prämisse: Man kann die Gültigkeit einer
Zusicherung I hinter dem Schleifenrumpf folgern, sofern
I und B vor dem Schleifenrumpf gültig
sind. Konklusion: Ist I vor der Schleife gültig,
muss hinter der Schleife I und ¬B gelten.
Man bezeichnet I in diesem Zusammenhang als
Schleifeninvariante, kurz Invariante.
{I ∧ B} S {I}
───────────────────────────────
{I} while B do S end {I ∧ ¬B}
Die Auffindung einer Schleifeninvariante ist nicht immer einfach.
Betrachten wir nochmals die rekursive Definition der Potenzierung. Für eine ganze Zahl x und eine nichtnegative Zahl n ist die Potenz xn definiert gemäß
x0 := 1,
xn
:= x⋅xn−1.
Es wird nun gezeigt, wie man mit dem Hoare-Kalkül die partielle Korrektheit des iterativen Berechnungsverfahrens
fn pow(x: i32, n: u32) -> i32 {
let mut y = 1;
for _ in 0..n {y *= x;}
y
}
zeigt. Zunächst müssen wir die for-Schleife in eine äquivalente while-Schleife transformieren. Dies resultiert in:
fn pow(x: i32, n: u32) -> i32 {
let mut y = 1;
let mut i = 0;
while i != n {
y = x*y;
i = i + 1;
}
y
}
Das Ende der Berechnung liegt direkt hinter der Schleife, womit
dort i==n ist. Außerdem soll dort y das
Ergebnis der Berechnung sein, d. h. y==xn.
Demnach gilt dort y==xi. Weil sich in der
Schleife sowohl i als auch y verändern,
können wir vermuten, dass es sich bei der letzten Gleichung um
eine Schleifeninvariante handelt. Wie sich herausstellt, ist diese
Vermutung richtig und zielführend.
Nun werden zum Algorithmus die Zusicherungen annotiert.
fn pow(x: i32, n: u32) -> i32 {
let mut y = 1;
let mut i = 0;
// {y == 1 und i == 0}
// {y == xi}
while i != n {
// {y == xi}
y = x*y;
// {y == xi+1}
i = i + 1;
// {y == xi}
}
// {y == xi und nicht i != n}
// {y == xn}
y
}
Rechnen wir das durch. Die Invariante ist vor der Schleife
erfüllt, denn laut der vorherigen Zusicherung darf y==1
und i==0 in die Gleichung eingesetzt werden.
Das macht 1==x0, und laut Definition der
Potenzierung stimmt dies.
Nun nehmen wir an, die Invariante sei innerhalb der Schleife
vor dem Schleifenrumpf erfüllt. Nach der Zuweisung
y := x*y; gilt dann y==x*xi,
und laut Definition der Potenzierung ist x*xi
das Gleiche wie xi+1. Die Inkrementation
i := i+1; bewirkt, dass i in der
Zusicherung dekrementiert werden muss. Formal ausgedrückt gilt
{y == xi}[i := i+1] i := i+1; {y == xi}
laut Zuweisungsaxiom, was nach Vereinfachung die gewünschte Form
{y == xi+1} i := i+1; {y == xi}
annimmt. Daher ist die Invariante auch hinter dem Schleifenrumpf
erfüllt. Laut der while-Regel gilt hinter der Schleife folglich
die Invariante und die Negation der Bedingung i!=n.
Die Negation von i!=n ist i==n.
Am Ende gilt hiermit schließlich
y==xn, was zu beweisen war.
Diese Technik ist bedeutungsschwer, – vergleichbar wichtig wie das Verfahren der vollständigen Induktion. Wir können nun der Reihe nach unsere Algorithmen beweisen. Zumindest erst einmal die, deren Komplexität nicht zu hoch ist. Letztendlich hilft uns die Verifikation im Hoare-Kalkül, einen Algorithmus besser zu verstehen.
Wohlgemerkt wurde nur die partielle Korrektheit gezeigt.
Die totale Korrektheit gilt ohnehin nicht, denn für zu große Argumente
kommt es zum Ganzzahl-Überlauf. Der Algorithmus divergiert hierbei
nicht deshalb, weil sich die Berechnung in einer Endlosschleife
verfängt, sondern weil eine der arithmetischen Operationen zu
panic führt. Dies gilt für die arithmetischen Operationen
zumindest im in dieser Hinsicht puristischen Debug-Modus. Das ist auch
dringend notwendig, denn andernfalls wäre nicht einmal die partielle
Korrektheit sicher.
Die partielle Korrektheit genügt uns natürlich nicht. Jede partiell korrekte Funktion, die sich nicht in einer Endlosschleife verfangen kann, können wir zu einer total korrekten machen, indem die Funktion und all ihre fehlbaren Teiloperationen monadisch verhüllt werden. Wie das gemacht wird, wurde im Abschnitt ›Sichere Programmierung: Monaden‹ bereits beschrieben. Wir gelangen zum strikten Algorithmus:
fn pow(x: i32, n: u32) -> Option<i32> {
let mut y: i32 = 1;
let mut i: u32 = 0;
while i != n {
y = y.checked_mul(x)?;
i = i + 1;
}
Some(y)
}
Wie man sieht, bedarf es nur der Verhüllung der Ergebnisse. Die Argumente dürfen nackt bleiben.
Der Beweis zur Terminierung der Schleife ist recht evident.
Weil vor der Schleife i ≤ n ist und
i in jedem Durchlauf inkrementiert wird, muss irgendwann
i==n gelten. Aus diesem Grund kommt es ferner nicht zum
Überlauf in der Operation i+1.
Ein weiterer Algorithmus zur Berechnung von Potenzen ist die schnelle Potenzierung.
fn pow(mut x: i32, mut n: u32) -> i32 {
let mut y = 1;
while n>1 {
if n%2 == 1 {y = y*x;}
n /= 2; x = x*x;
}
if n == 1 {y = y*x;}
y
}
Einführung von Hilfsvariablen sorgt dafür, dass die ursprünglichen Argumente konstant bleiben. Das ist notwendig, weil diese in die Überlegung einbezogen werden müssen. Der Algorithmus wird damit transformiert zu:
fn pow(x: i32, n: u32) -> i32 {
let mut y = 1;
let mut a = x;
let mut i = n;
while i>1 {
if i%2 == 1 {y = y*a;}
i /= 2;
a = a*a;
}
if i == 1 {y = y*a;}
y
}
Der Ansatz ist wieder eine Rückwärtsbetrachtung des Programmablaufs.
Der Rückgabewert am Ende muss y==xn sein,
so wie das auch im einfachen Algorithmus war. Zunächst findet
man:
// {y == xn ∧ i == 0 ∨ y*a == xn ∧ i == 1}
if i == 1 {y = y*a;}
// {y == xn}
Im Fall i==1 reduziert sich die Vorbedingung nämlich
zu y*a==xn, die bedingte Anweisung wird
ausgeführt und das Resultat ist y==xn
laut Zuweisungsaxiom. Im Fall i!=1 muss i==0
sein, denn hinter der Schleife gilt 0≤i≤1.
In diesem Fall reduziert sich die Vorbedingung zu
y==xn, die bedingte Anweisung wird nicht
ausgeführt und das Resultat ist ebenfalls y==xn.
Nun kommt ein kritischer Schritt, dessen Auffindung ohne Übung
schwierig sein mag. Vor der Schleife gilt
ai==xn, was etwas mit der
Schleifeninvariante zu tun haben könnte. Betrachten wir nun die
Vorbedingung
{y == xn ∧ i == 0 ∨ y*a == xn ∧ i == 1}.
Ist ai==xn so modifizierbar,
dass diese gilt? Ja, nämlich zu
y*ai==xn, weil
Fall i == 0: y*ai == y*a0 == y, Fall i == 1: y*ai == y*a1 == y*a.
Die Gleichung y*ai==xn gilt auch
vor der Schleife, denn dort ist y==1. Zudem
kommen in der Gleichung alle drei Variablen vor, die sich
in der Schleife verändern. Tatsächlich ist die Gleichung eine
günstige Schleifeninvariante.
Nun zum Schleifenrumpf. Das Tripel zur ersten Anweisung ist:
// {y*ai == xn}
if i%2 == 1 {y = y*a;}
// {y*ai-1 == xn ∧ i%2 == 1 ∨ y*ai == xn ∧ i%2 == 0}
Die lange Nachbedingung kann man kompakter schreiben als
{y*ai-i%2 == xn}.
Außerdem gilt
i-i%2 == 2*(i/2).
Mit dieser Vorbereitung ist der Rest ein Kinderspiel. Gemäß Zuweisungsaxiom sind die Tripel
// {y*a2*(i/2) == xn}
i /= 2;
// {y*a2i == xn}
und
// {y*a2i == xn}
a = a*a;
// {y*ai == xn}
erfüllt. Damit ist die Invariante bewiesen. Weil nichts weiter zu beweisen verbleibt, ist auch der Algorithmus bewiesen. Der Algorithmus mit sämtlichen Zusicherungen:
fn pow(x: i32, n: u32) -> i32 {
let mut y = 1;
let mut a = x;
let mut i = n;
// {y*ai == xn}
while i>1 {
// {y*ai == xn}
if i%2 == 1 {y = y*a;}
// {y*ai-i%2 == y*a2*(i/2) == xn}
i /= 2;
// {y*a2i == xn}
a = a*a;
// {y*ai == xn}
}
// {y*ai == xn ∧ 0≤i≤1}
if i == 1 {y = y*a;}
// {y == xn}
y
}
So schön die Beweise anmuten, können auch diese von Fehlern unterlaufen sein. Ein naheliegender Weg zur Vermeidung sind Proben zur Laufzeit, denn die Zusicherungen lassen sich ja für konkrete Variablenbelegungen zur Laufzeit ausführen.
Im Algorithmus zur Potenzierung sollte es nirgends zum Überlauf kommen, sofern die ursprüngliche Definition keinen Überlauf berechnet. Eine Schleife grast nun im Folgenden den Definitionsbereich ab, wobei der Algorithmus lediglich für die verbleibenden Fälle ohne Überlauf ausgeführt wird.
// Definition der Potenzfunktion
fn pow_rec(x: i32, n: u32) -> Option<i32> {
if n==0 {Some(1)} else {x.checked_mul(pow_rec(x, n-1)?)}
}
// Partielle Funktion zu pow_rec
fn pow(x: i32, n: u32) -> i32 {
pow_rec(x, n).unwrap()
}
fn pow_iter(x: i32, n: u32) -> i32 {
let mut y = 1;
let mut a = x;
let mut i = n;
let p = pow(x, n);
assert!(y*pow(a, i) == p);
while i>1 {
assert!(y*pow(a, i) == p);
if i%2 == 1 {y = y*a;}
assert!(y*pow(a, i-i%2) == p);
i /= 2;
assert!(y*pow(a, 2*i) == p);
a = a*a;
assert!(y*pow(a, i) == p);
}
assert!(y*pow(a, i) == p && i<=1);
if i == 1 {y = y*a;}
assert!(y == p);
y
}
fn main() {
for x in -65536..65536 {
for n in 0..32 {
if let Some(y) = pow_rec(x, n) {
assert!(y == pow_iter(x, n));
}
}
}
}
Maßgeblich sind abschließend zudem die Beweise, dass im späteren
Programm die Aufrufe von pow_iter niemals Zahlen bekommen,
die zum Überlauf führen würden.