Durch Testen kann nachgewiesen werden, dass sich ein Programm für endlich viele Eingaben korrekt verhält. Durch eine Verifikation kann nachgewiesen werden, dass sich ein Programm für alle Eingaben korrekt verhält.
Bei der Zusicherungsmethode sind zwischen den Statements so genannte Zusicherungen eingestreut, die eine Aussage darstellen über die momentane Beziehung zwischen den Variablen.
Syntaktisch lassen sich diese Zusicherungen am einfachsten als Kommentare formulieren. Z.B.
//
Aus einer Zusicherung und der folgenden Anweisung lässt sich dann eine weitere Zusicherung ableiten:
i = i - 1;
//
Bei Schleifen wird die Zusicherung , die vor Eintritt und vor Austritt
gilt, die Schleifeninvariante genannt.
//
while Q {
//
//
}
//
Beginnend mit einer ersten, offensichtlich richtigen Zusicherung, lässt sich als letzte Zusicherung eine Aussage über das berechnete Ergebnis ableiten = partielle Korrektheit.
Zusammen mit dem Nachweis der Terminierung ergibt sich die totale Korrektheit. Beispiel für die Zusicherungsmethode:
int n, x, y, z;
do n = IO.readInt(); while (n < 0);
//
x = 0; y = 1; z = 1;
//
while (z <= n) /* */ {
//
//
x = x + 1;
//
y = y + 2;
//
z = z + y;
//
//
}
//
//
//
IO.println (x);
// Ausgabe:
Terminierung
Da immer positiv ist und
immer um
erhöht wird und
fest bleibt,
muß irgendwann gelten
Laufzeit
In jedem Schleifendurchlauf wird um eins erhöht.
Da bei
beginnt und bei
endet,
wird der Schleifenrumpf
mal durchlaufen.
Der Schleifenrumpf selbst hat eine konstante Anzahl von
Schritten.
Weiteres Beispiel für die Zusicherungsmethode:
int n, x, y, z;
do { n = IO.readInt(); } while (n < 0);
//
x = 2; y = n; z = 1;
//
while (y > 0) {
//
if (y % 2 == 1) {
//
ungerade
z = z * x;
//
ungerade
y = y - 1;
//
//
} else {
//
gerade
x = x * x;
//
gerade
y = y/2;
//
//
}
//
}
//
//
IO.println (z);
// Ausgabe:
Terminierung
In jedem Schleifendurchlauf wird kleiner
irgendwann einmal Null
Abbruch.
Laufzeit
Die Dualzahldarstellung von schrumpft spätestens nach
Schleifendurchläufen um eine Stelle
Hinweis: Der naive Ansatz
n = IO.readInt("n = "); z = 1; for (i = 0; i < n; i++) z = 2*z;hat Laufzeit