\begin{slide}{Axiom für Schleifen}

\begin{verbatim}
wenn  { I and B } A { I },
dann  { I } while (B) do A { I and not B }
\end{verbatim}
  
Beispiel:
\begin{verbatim}
Eingabe int p, q; 
// p = P und q = Q
int c = 0;
// inv: p * q + c = P * Q 
while (q > 0) { 
   ???
}
// c = P * Q
\end{verbatim}
Moral: erst Schleifeninvariante (Spezifikation),
dann Implementierung.

\end{slide}
