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 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.
Per Definition berechnet das Programm
def pow_rec(x, n):
return 1 if n == 0 else x*pow_rec(x, n - 1)
die Potenz also in korrekter Weise.
Es wird nun gezeigt, wie man mithilfe des Hoare-Kalküls die partielle Korrektheit des iterativen Berechnungsverfahrens
def pow(x, n):
y = 1
for i in range(0, n): y *= x
return y
zeigt. Zunächst müssen wir die for-Schleife in eine äquivalente while-Schleife transformieren. Dies resultiert in:
def pow(x, n):
y = 1
i = 0
while i != n:
y = x*y
i = i + 1
return 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, das heißt 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.
def pow(x, n):
y = 1
i = 0
# {y == 1 and i == 0}
# {y == xi}
while i != n:
# {y == xi}
y = x*y
# {y == xi+1}
i = i + 1
# {y == xi}
# {y == xi and not i != n}
# {y == xn}
return 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 lediglich die partielle Korrektheit gezeigt. Die totale Korrektheit gilt eigentlich ohnehin nicht, denn für zu große Argumente würde das Programm mehr Speicher benötigen als im Computer zur Verfügung steht.
Aber angenommen, dieser Speicher stünde immer zur Verfügung. Der
Beweis zur Terminierung der Schleife ist dann recht evident.
Weil vor der Schleife i ≤ n ist und
i in jedem Durchlauf inkrementiert wird, muss irgendwann
i==n gelten.
Nun kann es vorkommen, dass der Beweis selbst mit Fehlern behaftet
ist. Mithilfe der Anweisung assert können wir die
Zusicherungen für konkrete Belegungen der Parameter x
und n zur Laufzeit prüfen lassen. Zwar liefert das
keine Garantie für die Korrektheit des Beweises, jedoch sind solche
Tests nützlich, um Fehler aufzuspüren.
def pow(x, n):
y = 1
i = 0
assert y == 1 and i == 0
assert y == pow_rec(x, i)
while i != n:
assert y == pow_rec(x, i)
y = x*y
assert y == pow_rec(x, i + 1)
i = i + 1
assert y == pow_rec(x, i)
assert y == pow_rec(x, i) and not i != n
assert y == pow_rec(x, n)
return y
def test():
for x in range(-9, 10):
for n in range(0, 10): pow(x, n)
test()
Ein weiterer Algorithmus zur Berechnung von Potenzen ist die schnelle Potenzierung.
def pow(x, n):
y = 1
while n > 1:
if n%2 == 1: y = y*x
n //= 2; x = x*x
if n == 1: y = y*x
return 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:
def pow(x, n):
y = 1
a = x
i = n
while i > 1:
if i%2 == 1: y = y*a
i //= 2
a = a*a
if i == 1: y = y*a
return 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:
def pow(x, n):
y = 1
a = x
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}
return 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.
def pow_iter(x, n):
y = 1; a = x; i = n
p = pow_rec(x, n)
assert y*pow_rec(a, i) == p
while i > 1:
assert y*pow_rec(a, i) == p
if i%2 == 1: y = y*a
assert y*pow_rec(a, i-i%2) == p
i //= 2
assert y*pow_rec(a, 2*i) == p
a = a*a
assert y*pow_rec(a, i) == p
assert y*pow_rec(a, i) == p and i<=1
if i == 1: y = y*a
assert y == p
return y