\begin{slide}{Korrektheit, Spezifikation}

\begin{itemize}
\item
  jeder Algorithmus hat eine \emph{Spezifikation},

  die die gewünschte Beziehung zwischen Ein- und Ausgabe beschreibt.
\item
  Forderung an die Eingaben: Vorbedingung

  Forderung an die Ausgaben: Nachbedingung

  Schreibweise: \verb|{ V } A { N }|
\item
  Algorithmus heißt \emph{korrekt}, wenn er seine Spezifikation erfüllt.
\item
  \emph{erst} spezifizieren, \emph{dann} implementieren!
\end{itemize}

\end{slide}

