%% -*- mode: latex; TeX-master: "informatik.tex"; -*-

\begin{slide}{Schleifen-Invarianten}

\kopf{$ $Id: invariant.tex,v 1.1 2006-10-09 13:24:17 waldmann Exp $ $}

\begin{verbatim}
static int power (int b, int e) {
   int p = 1; int q = b;
   while (e > 0) { 
      if (1 == e % 2) { p = p * q; }
      q = q * q; e = e / 2;
   }
   return p;
}
\end{verbatim}
Der Ausdruck $A = p \cdot q^e$ ist \emph{invariant}:

seine Werte vor und nach Ausführen eines Schleifenkörpers
stimmen überein.
\end{slide}

\begin{slide}{Invarianten (II)}
Beweis: Falls $e>0$ und  $e$ gerade, dann
$p' = p, q' = q^2, e' = e/2$, also $p' \cdot q'^2 = p \cdot q^{2\cdot e/2}
= p \cdot q^e$.

Falls $e>0$ und $e$ ungerade: Übung.

Der Wert von $A$ \emph{vor} der Schleife ist $1 \cdot b^e$,

der Wert von $A$ \emph{nach} der Schleife ist $p \cdot q^0 = p$.

\end{slide}

\begin{slide}{Invarianten (III)}

Denken Sie \emph{zuerst} an die Invariante,
und notieren Sie sie (als Kommentar zu Beginn der Schleife).

Schreiben Sie \emph{dann} den Schleifenkörper so,
daß die behauptete Invariante tatsächlich invariant ist.

Für Sonderformen von Schleifen (do-while, break)
ist diese Analyse viel schwieriger,
deswegen sollten diese auch nicht 
ohne besonderen Grund benutzt werden.

\end{slide}
