<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">\begin{slide}{Schnittstellen und Verträge}

wenn jemand eine Schnittstelle implementiert,
dann schreibt er nicht irgendwelche Methoden mit passenden Namen,
sondern erfüllt einen Vertrag:

\begin{itemize}
\item
  Implementierung soll genau das tun, \\ was beschrieben wird.
\item
  Implementierung soll nichts \\ anderes, unsinniges, teures, gefährliches tun.
\item
  Implementierung soll bescheid geben, \\ wenn Auftrag nicht ausführbar ist.
\end{itemize}
(Bsp: Pizzafehlermeldung)

\end{slide}


\begin{slide}{Design by Contract}

Betrand Meyer: \emph{Object-Oriented Software Construction},
Prentice Hall, 1997.
\url{http://archive.eiffel.com/doc/oosc/}

Aspekte eines Vertrages:
\begin{itemize}
\item
  Vorbedingungen
\item
  Nachbedingungen
\item
  Klassen-Invarianten
\end{itemize}

\end{slide}


\begin{slide}{Schnittstellen und Tests}

man überzeuge sich von
\begin{itemize}
\item
  Benutzbarkeit einer Schnittstelle
  (unabhängig von Implementierung)

  \dots wird das gewünschte Ergebnis durch eine Folge von 
  Methodenaufrufen vertraglich garantiert?
\item
  Korrekheit einer Implementierung
\end{itemize}

mögliche Argumentation:
\begin{itemize}
\item formal (Beweis)
\item testend (beispielhaft)

  \dots benutze \emph{Proxy}, der Vor/Nachbedingungen auswertet
\end{itemize}

\end{slide}


\begin{slide}{Stufen von Verträgen}

(nach K. Pugh)

\begin{itemize}
\item
  Typdeklarationen
\item
  Formale Spezifikation von Vor- und Nachbedingungen
\item
  Leistungsgarantien (für Echtzeitsysteme)
\item
  Dienstgüte-Garantien (quality of service)
\end{itemize}

\end{slide}


\begin{slide}{Typen als Verträge}

\emph{Der Typ eines Bezeichners ist seine beste Dokumentation.}

(denn der Compiler kann sie prüfen!)

Es sind Sprachen (und ihre Sprecher) arm dran,
deren Typsystem ausdrucksschwach ist.

\begin{verbatim}
int a [] = { "foo", 42 }; // ??

// Mittelalter-Java:
List l = new LinkedList (); 
l.add ("foo"); l.add (42);

// korrektes Java:
List&lt;String&gt; l = new LinkedList&lt;String&gt; (); 
\end{verbatim}


\end{slide}
</pre></body></html>