Korrektheit und Terminierung

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. /* $i > 0\wedge z=i^{2}$ */

Aus einer Zusicherung und der folgenden Anweisung lässt sich dann eine weitere Zusicherung ableiten:

i = i - 1;
$\Rightarrow$ /* $i \geq 0\ \ \wedge$ $z=(i+1)^{2}$ */

Bei Schleifen wird die Zusicherung $P$, die vor Eintritt und vor Austritt gilt, die Schleifeninvariante genannt.

/* $P$ */
while Q {
     /* $P\ \wedge\ Q$ */
     $\vdots$
     $\vdots$
     /* $P$ */
}
/* $P\ \wedge\ \neg 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 \geq \ 0$ */
x = 0; y = 1; z = 1;
/* $(z = (x + 1)^{2}\ \wedge\ y = 2x + 1 \ \wedge\ x^{2} \leq n) \ = \mbox{\rm Schleifeninvariante } P$ */
while (z <= n) /* $Q$ */ {
     /* $z = (x + 1)^{2}\ \wedge\ y = 2x + 1\ \wedge\ x^{2} \leq n\ \wedge\ z \leq n \Rightarrow (x + 1)^2 \leq n$ */
     x = x + 1;
     /* $z = x^{2}\ \wedge\ y = 2x - 1\ \wedge\ x^{2} \leq n$ */
     y = y + 2;
     /* $z = x^{2}\ \wedge\ y = 2x + 1\ \wedge\ x^{2} \leq n$ */
     z = z + y;
     /* $z = x^{2} + 2x + 1\ \wedge\ y = 2x + 1 \ \wedge\ x^{2} \leq n$ */
     /* $(z = (x + 1)^{2}\ \wedge\ y = 2x + 1 \ \wedge\ x^{2} \leq n) \ =P$ */
}
/* $(z = (x + 1)^{2}\ \wedge\ y = 2x + 1 \ \wedge\ x^{2} \leq n \ \wedge\ z>n) \ = P \ \wedge \neg Q$ */
/* $x^{2} \leq n < (x + 1)^{2}$ */
/* $x = \lfloor \sqrt{n} \rfloor$ */
IO.println (x);
/* Ausgabe: $\lfloor \sqrt{n} \rfloor$ */

Terminierung

Da $y$ immer positiv ist und $z$ immer um $y$ erhöht wird und $n$ fest bleibt, muß irgendwann gelten $z > n$

$\Rightarrow$

Abbruch gesichert

$\Rightarrow$

totale Korrektheit.

Laufzeit

In jedem Schleifendurchlauf wird $x$ um eins erhöht.

Da $x$ bei $0$ beginnt und bei $\lfloor \sqrt{n} \rfloor$ endet, wird der Schleifenrumpf $\sqrt{n}$ mal durchlaufen. Der Schleifenrumpf selbst hat eine konstante Anzahl von Schritten.

$\Rightarrow$

Laufzeit $O(n^{\frac{1}{2}})$, 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 \geq \ 0$ */
x = 2; y = n; z = 1;
/* $z \cdot x^{y} = 2^{n} \wedge\ y \geq 0$ */
while (y > 0) {
     /* $z \cdot x^{y} = 2^{n}\ \wedge\ y > 0$ */
     if (y % 2 == 1) {
          /* $z \cdot x^{y} = 2^{n}\ \wedge\ y > 0 \ \wedge\ y$ ungerade */
          z = z * x;
          /* $\frac{z}{x} \cdot x^{y} = 2^{n}\ \wedge\ y > 0 \ \wedge\ y$ ungerade */
          y = y - 1;
          /* $\frac{z}{x} \cdot x^{y+1} = 2^{n}\ \wedge\ y \geq 0$ */
     /* $z \cdot x^{y} = 2^{n} \wedge\ y \geq 0$ */
     } else {
          /* $z \cdot x^{y} = 2^{n}\ \wedge\ y > 0 \ \wedge\ y$ gerade */
          x = x * x;
          /* $z \cdot (x^{\frac{1}{2}})^{y} = 2^{n}\ \wedge\ y > 0 \ \wedge \ y$ gerade */
          y = y/2;
          /* $z \cdot (x^{\frac{1}{2}})^{2y} = 2^{n}\ \wedge\ y \geq\ 0$ */
          /* $z \cdot x^{y} = 2^{n} \wedge\ y \geq 0$ */
     }
     /* $z \cdot x^{y} = 2^{n} \wedge\ y \geq 0$ */
}
/* $z \cdot x^{y} = 2^{n}\ \wedge\ y \geq 0 \wedge\ y \leq 0$ */
/* $z \cdot x^{y} = 2^{n}\ \wedge\ y = 0 \Rightarrow z = 2^n$ */
IO.println (z);
/* Ausgabe: $2^n$ */

Terminierung

In jedem Schleifendurchlauf wird $y$ kleiner $\Rightarrow$ irgendwann einmal Null $\Rightarrow$ Abbruch.

Laufzeit

Die Dualzahldarstellung von $y$ schrumpft spätestens nach $2$ Schleifendurchläufen um eine Stelle

$\Rightarrow$

$O( \log n)$ Durchläufe, wobei $n$ der Wert der Eingabezahl ist, d.h. $O(n)$, wenn $n$ die Länge der Dualdarstellung der Eingabe ist.

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(2^{k})$, wenn $k$ die Länge der Dualdarstellung von $n$ ist.