\begin{slide}{Partielle und totale Korrektheit}

\begin{itemize}
\item
  partielle Korrektheit:

  \emph{wenn} Vorbedingung erfüllt und $P$ ausgeführt wird,
  \emph{dann} gilt schließlich Nachbedingung
\item
  totale Korrektheit:

  \emph{wenn} Vorbedingung gilt,
  \emph{dann} ist $P$ tatsächlich komplett ausführbar 
  \emph{und} es gilt schließlich die Nachbedingung
\end{itemize}

für Schleifen:
\begin{itemize}
\item
  partielle Korrektheit: \glqq Invarianz der Invariante\grqq
\item
  totale Korrektheit: \dots außerdem \emph{Termination}
\end{itemize}


\end{slide}

\begin{slide}{Termination: Beispiel}

Termination von Programmen ist schwer (genauer: unentscheidbar)

\bigskip

\begin{verbatim}
import java.util.Stack;
void dauert_lange (int start) {
  Stack<Integer> s = new Stack<Integer> ();
  s.push (start); 
  for (int k = 1; ! s.empty(); k++) {
    int top = s.pop ();
    if (top > 0) {
      for (int j=0; j<k; j++) {
        s.push (top - 1);
} } } }
\end{verbatim}

Hält \verb|dauert_lange(4)|? Nach wievielen Schritten?


\end{slide}

\begin{slide}{Termination \glqq von selbst\grqq}

am sichersten sind Programme,
die \glqq von selbst\grqq\ terminieren:
\begin{itemize}
\item
  ganz ohne Schleifen/Rekursion
\item
  nur mit \glqq einfachen\grqq\ Schleifen:
\begin{verbatim}
for (int k = 0; k < 100; k++) { .. }

Collection <T> c; for (T x : c) { .. }
\end{verbatim}
  solche Schleifen dürfen auch geschachtelt sein

  \dots sog. \emph{primitiv rekursive Funktionen}
\end{itemize}

\end{slide}

\begin{slide}{Termination für Ersetzungs-Systeme}

Regelmenge (z. B. $R = \{ab \to bba\}$) \\
definiert Relation auf Wörtern

$R$ terminiert $\iff$ es gibt keine unendlich lange $R$-Ableitung
($=$ Folge von Regel-Anwendungen)

\begin{itemize} \itemsep 2pt
\item
  wieviele Schritte von $a^k b$ aus?
\item
  terminieren diese Systeme?
  \begin{itemize}
  \item
    $\{10000 \to 000011110\}$,
  \item
    $\{aa\to bc, bb\to ac, cc\to ab\}$
  \item
    $\{101 \to 000, 000 \to 111\}$ (ist offen, gibt Preis!)
  \end{itemize}
\item
  für welche $p,q,r,s$ terminiert
  $a^p b^q \to b^r a^s$?

  Beispiel: $p=q=2, r=s=3$.
\end{itemize}

\newpage

\begin{itemize} \itemsep 0pt
\item
  Workshop on Termination
  \url{http://www-i2.informatik.rwth-aachen.de/WST04/}
\item
  Matchbox
  \url{http://dfa.imn.htwk-leipzig.de/matchbox/}
\item
  RTA list of open problems~
  \url{http://www.lsv.ens-cachan.fr/rtaloop/problems/21.html}
\end{itemize}


\end{slide}
