\begin{slide}{Schleifen, Invarianten}

 Korrektheit einer Schleife 
\begin{verbatim}
{ V } while (B) do C { N }
\end{verbatim}
 
beweist man durch geeignete \emph{Invariante} $I$:
  \begin{itemize}
  \item
    aus $V$ folgt $I$
  \item
    \verb| { I und B } C { I } |
  \item
    aus ($I$ und nicht $B$) folgt $N$ 
  \end{itemize}
 

\end{slide}
