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.
Z.B. /*
i > 0 
z = i2 */
Aus einer Zusicherung und der folgenden Anweisung lässt sich dann eine weitere Zusicherung ableiten:
i = i - 1;
/*
i 
0
z = (i + 1)2 */
Bei Schleifen wird die Zusicherung P, die vor Eintritt und vor Austritt gilt, die Schleifeninvariante genannt.
/* P */
while Q {
/*
P Q */
/* P */
}
/*
P 
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);
/*
n 0 */
x = 0; y = 1; z = 1;
/*
(z = (x + 1)2 y = 2x + 1 x2 
n) = Schleifeninvariante P */
while (z <= n) /* Q */ {
/*
z = (x + 1)2 y = 2x + 1 x2 n z n (x + 1)2 n */
x = x + 1;
/*
z = x2 y = 2x - 1 x2 n */
y = y + 2;
/*
z = x2 y = 2x + 1 x2 n */
z = z + y;
/*
z = x2 + 2x + 1 y = 2x + 1 x2 n */
/*
(z = (x + 1)2 y = 2x + 1 x2 n) = P */
}
/*
(z = (x + 1)2 y = 2x + 1 x2 n z > n) = P Q */
/*
x2 n < (x + 1)2 */
/*
x = 
*/
IO.println (x);
/* Ausgabe:
*/
Terminierung
Da y immer positiv ist und z immer um y erhöht wird und n fest bleibt, muß irgendwann gelten z > n
Laufzeit
In jedem Schleifendurchlauf wird x um eins erhöht.
Da x bei 0 beginnt und bei
endet,
wird der Schleifenrumpf mal durchlaufen.
Der Schleifenrumpf selbst hat eine konstante Anzahl von
Schritten.
), wobei n der Wert der
Eingabezahl ist!Weiteres Beispiel für die Zusicherungsmethode:
int n, x, y, z;
do { n = IO.readInt(); } while (n < 0);
/* n 0 */
x = 2; y = n; z = 1;
/*
z . xy = 2n */
while (y > 0) {
/*
z . xy = 2n y > 0 */
if (y % 2 == 1) {
/*
z . xy = 2n y > 0 y ungerade */
z = z * x;
/*
. xy = 2n y > 0 y
ungerade */
y = y - 1;
/*
. xy + 1 = 2n y 0 */
/*
z . xy = 2n y 0 */
} else {
/*
z . xy = 2n y > 0 y gerade */
x = x * x;
/*
z . (x)y = 2n y > 0 y gerade */
y = y/2;
/*
z . (x)2y = 2n y 0 */
/*
z . xy = 2n y 0 */
}
/*
z . xy = 2n y 0 */
}
/*
z . xy = 2n y 0 y 0 */
/*
z . xy = 2n y = 0 z = 2n */
IO.println (z);
/* Ausgabe: 2n */
Terminierung
In jedem Schleifendurchlauf wird y kleiner
irgendwann einmal Null
Abbruch.
Laufzeit
Die Dualzahldarstellung von y schrumpft spätestens nach 2 Schleifendurchläufen um eine Stelle
Hinweis: Der naive Ansatz
n = IO.readInt("n = "); x = 1;
for (i = 0; i < n; i++) x = 2*x;
hat Laufzeit O(n), wenn n der Wert der Eingabezahl ist,
d.h. O(2k), wenn k die Länge der Dualdarstellung von n ist.