\begin{slide}{Termination}

  \begin{itemize}
  \item 
Geradeausprogramme halten (terminieren) immer:
\begin{verbatim}
Eingabe a, b;  int c := a; a := b; b := c; Ausgabe a, b; 
\end{verbatim}

\item 
Zählschleifen halten immer:
\begin{verbatim}
für Zahl a von 0 bis 9 { Ausgabe (a); }
\end{verbatim}

\item 
beliebige Schleifen?
\begin{verbatim}
Zahl a = 0;
while ( a*a != 125 ) { a := a + 1; }
\end{verbatim}
  \end{itemize}

\end{slide}

\begin{slide}{Termination (Beispiele)}

  \begin{itemize}\itemsep 0pt
  \item 
\begin{verbatim}
solange (a ungleich b) {
    if (a > b) { a := a - b; }
    else       { b := b - a; }
}
\end{verbatim}
beachte Invariante:   $a$ und $b$ sind positive ganze Zahlen.
$a+b>0$ und $a+b$ nimmt ab.

 \item 
\begin{verbatim}
solange (a > 0) { a := abrunden (a/2); }
\end{verbatim}
beachte:   $a$ nimmt ab.

\item
\begin{verbatim}
solange (x > 1) {
    if (x ist gerade)  { x := x/2; }
    else { x := 3 * x + 1; }
}
\end{verbatim}
\end{itemize}

\end{slide}
