\begin{slide}{Korrektheit: Spezifikationen}

Algorithmen werden benutzt, weil sie Probleme lösen.

\emph{Lösen} heißt:
Fur alle (sinnvollen) Eingaben
erwartet man die korrekte (richtige) Ausgabe.

Das \emph{gewünschte} Verhältnis von Ein- zu Ausgaben
nennt man \emph{Spezifikation} des Algorithmus.


Bemerkungen: 

Trennung von Spezifikation und Implementierung
ist auch in anderen technischen Bereichen sinnvoll und üblich ---

sie erlaubt erst den Entwurf und Herstellung komplexer Systeme:
Module werden zunächst spezifiziert, 
dann (unabhängig voneinander) implementiert.

\end{slide}

\begin{slide}{Korrektheit: Beweise}

Vor Benutzung eines Algorithmus muß man  sich 
auf geeignete Weise davon überzeugen,
daß er seine Spezifikation erfüllt.

In sicherheitskritischen Bereichen ist sind dazu
tatsächlich \emph{formale Beweise} vorgeschrieben.

\end{slide}

\begin{slide}{Korrektheit: Invarianten}

\begin{verbatim}
static int mal (int a, int b) {
  int q = a; int p = b; int c = 0;
  while ( q > 0 ) {
    int r = q % 2; c = c + r * p; q = q / 2; p = p * 2;
  }
  return c;
}
\end{verbatim}
Behauptung: Die Aussage \verb|a * b = q * p + c| 
ist \emph{direkt vor}, \emph{während}, und \emph{direkt nach} 
der Schleife wahr (sie ist \emph{invariant}).

Beweis: Fallunterscheidung nach $q$ gerade oder ungerade
($\to$ $r = 0$ oder $r = 1$)

Anwendung: der Algorithmus erfüllt die Spezifikation der Multiplikation
(die Ausgabe $c$ ist tatsächlich gleich $a \cdto b$).

\end{slide}
