\begin{slide}{Programming by contract}

jedes (Teil-)Produkt muß seine Spezifikation erfüllen,
diese ist ein Kontrakt (Vertrag):
\begin{itemize}
\item
  \emph{wenn} Vorbedingungen (an Programmzustand, Argumente) erfüllt,
\item
  \emph{dann} nach Arbeit des Produktes:

  Nachbedingungen (an Programmzustand, Resultat) erfüllt
\end{itemize}

eingebaut z. B. in Sprache Eiffel von Bertrand Meyer,
\url{http://www.eiffel.com/}

\newpage

Beispiel: Funktion merge (aus mergesort):
\begin{itemize}
\item \emph{wenn} \verb|xs| und \verb|ys| jeweils aufsteigend geordnete Listen,
\item \emph{dann} gilt für \verb|zs = merge(xs, ys)| :
  \begin{itemize}
  \item \verb|zs| ist aufsteigend geordnete Liste
  \item \verb|zs| ist Permutation von \verb|append(xs, ys)|
  \end{itemize}
\end{itemize}
Erfüllung des Kontrakts soll man
\begin{itemize}
\item
  beweisen (\emph{verifizieren}) \dots
\item
  \dots und wer das nicht kann, 
  dem bleibt nur mehr oder weniger systematisches Raten,
  genannt   \emph{testen} (assert, JUnit, Eiffel \dots, siehe später)
\end{itemize}

\end{slide}
