Vertragsmodell

Design by contract (englisch Entwurf gemäß Vertrag) oder kurz DBC ist ein Konzept aus dem Bereich der Softwareentwicklung. Ziel ist das reibungslose Zusammenspiel einzelner Programmmodule durch die Definition formaler "Verträge" zur Verwendung von Schnittstellen, die über deren statische Definition hinausgehen. Entwickelt und eingeführt wurde es von Bertrand Meyer mit der Entwicklung der Programmiersprache Eiffel.

Grundprinzip

Das reibungslose Zusammenspiel der Programmmodule wird durch einen "Vertrag" erreicht, der beispielsweise bei der Verwendung einer Methode einzuhalten ist. Dieser besteht aus

• Vorbedingungen (engl. precondition), also den Zusicherungen, die der Aufrufer einzuhalten hat
• Nachbedingungen (engl. postcondition), also den Zusicherungen, die der Aufgerufene einhalten wird sowie den
• Invarianten (engl. class invariants), quasi dem Gesundheitszustand einer Klasse.

Der Vertrag kann sich auf die gesamte verfügbare Information beziehen, also auf Variablen- und Parameter-Inhalte ebenso wie auf Objektzustände des betroffenen Objekts oder anderer zugreifbarer Objekte. Sofern sich der Aufrufende an Vorbedingungen und Invarianten hält, können keine Fehler auftreten und die Methode liefert garantiert keine unerwarteten Ergebnisse.

Eine abgeschwächte Form von Verträgen wird in typisierten Sprachen bereits durch die Typisierung der Ein- und Ausgabeparameter erreicht. Der Typ legt dabei Wertebereiche fest, die als Vor- und Nachbedingungen interpretiert werden können. Ein Typsystem ist jedoch nicht in der Lage, Zusammenhänge mehrerer Parameter oder Zusammenhänge zwischen Ein- und Ausgabewerten zu erfassen. Es stellt daher gegenüber Design by contract eine deutlich abgeschwächte Form der Absicherung dar, greift dafür jedoch in der Regel bereits zur Übersetzungszeit, während die in Verträgen getroffenen Zusicherungen erst bei Verletzung zur Laufzeit greifen.

Durch die Definition von Klasseninvarianten, Vor- und Nachbedingung kann ein Modul durch ein beliebiges ausgetauscht werden, wenn dieses denselben "Vertrag" erfüllt. Hierzu müssen jedoch ggf. auch verwendete Bezeichner und syntaktische Details als Vor- und Nachbedingungen aufgefasst werden.

Invarianten

Invarianten sind logische Aussagen, die für alle Instanzen einer Klasse über den gesamten Objektlebenszyklus hinweg gelten. Sie treten meist in Form von Klasseninvarianten auf, die auch auf private Eigenschaften der betroffenen Klasse zugreifen dürfen. Man spricht daher auch von Implementationsinvarianten. Da eine Überprüfung von Invarianten in aktuellen Systemen jeweils nur vor und nach einem Methoden-Aufruf erfolgen kann, dürfen Invarianten innerhalb von Methoden durchaus temporär verletzt werden. Sie stellen insofern implizite Vor- und Nachbedingungen jedes Methoden-Aufrufs dar. Eine Alternative zu diesem Ansatz bestünde darin, jegliche Variablenzugriffe mittels Methoden der Metaprogrammierung abzufangen und somit auch temporäre Verletzungen der Invarianten zu verbieten. Dieser Ansatz wird in gängigen Realisierungen von Design by contract bislang jedoch nicht verfolgt.

Vor- und Nachbedingungen

Jedem Unterprogramm werden Vorbedingungen (preconditions) und Nachbedingungen (postconditions) zugeordnet. Die Vorbedingungen legen fest, unter welchen Umständen das Unterprogramm aufrufbar sein soll. Beispielsweise darf ein Unterprogramm zum Lesen aus einer Datei nur dann aufgerufen werden, wenn die Datei vorher erfolgreich geöffnet wurde. Die Nachbedingungen legen die Bedingungen fest, die nach Abschluss des Unterprogrammaufrufs gegeben sein müssen.

Vor- und Nachbedingungen werden als boolesche Ausdrücke formuliert. Ist eine Vorbedingung nicht erfüllt (d.h. ihre Auswertung ergibt false, also "nicht zutreffend"), liegt ein Fehler im aufrufenden Code vor: Dort hätte dafür gesorgt werden müssen, dass die Vorbedingung erfüllt ist. Ist eine Nachbedingung nicht erfüllt, liegt ein Fehler im Unterprogramm selbst vor: Das Unterprogramm hätte dafür sorgen müssen, dass die Nachbedingung erfüllt ist.

Vor- und Nachbedingung bilden daher eine Art Vertrag (englisch contract): wenn der aufrufende Code die Vorbedingung erfüllt, dann ist das Unterprogramm verpflichtet, die Nachbedingung zu erfüllen.

Subklassenbildung und Verträge

Liskov'sches Substitutionsprinzip

Wendet man das liskovsche Substitutionsprinzip (nach Barbara Liskov, LSP) auf Vor- und Nachbedingungen an, erhält man die folgende Aussage:

Sind vor dem Aufruf des Unterprogramms der Unterklasse die Vorbedingungen der Oberklasse erfüllt, so muss das Unterprogramm die Nachbedingungen der Oberklasse erfüllen.

Dies bedeutet, dass ein Unterprogramm einer Unterklasse bei der Gestaltung seiner Vor- und Nachbedingungen nicht frei ist: es muss mindestens den durch die Vor- und Nachbedingungen formulierten "Vertrag" erfüllen. Das heißt, es darf die Vorbedingungen nicht verschärfen (es darf vom aufrufenden Code nicht mehr verlangen als in der Oberklasse verlangt), und es darf die Nachbedingungen nicht aufweichen (es muss mindestens so viel garantieren wie die Oberklasse).

Zusammenfassung der Vertragsbedingungen von Subklassen

Unterklassen müssen bei Design by Contract folgende Regeln bezüglich der Oberklassen befolgen:

• gleiche oder stärkere Invariante
• gleiche oder schwächere Vorbedingungen (bezüglich der Methoden)
• gleiche oder stärkere Nachbedingungen (bezüglich der Methoden)

Formal lässt sich die Beziehung von Super- und Subklasse hinsichtlich der Vor- und Nachbedingungen wie folgt ausdrücken:

Vorbedingungsuper → Vorbedingungsub
Nachbedingungsub  → Nachbedingungsuper

Überprüfung der Vertragsbedingungen von Subklassen

Die Erfüllung der im vorigen Absatz beschriebenen logischen Implikationen lassen sich algorithmisch jedoch nur sehr aufwändig überprüfen (Erfüllbarkeitsproblem). Man greift daher bei aktuellen Realisierungen auf einen Trick zurück:

• Die Vorbedingungen werden disjunktiv verknüpft. Hierdurch kann auch eine Abschwächung der Vorbedingung der Superklasse eintreten.
• Die Nachbedingungen werden konjunktiv verknüpft. Hierdurch kann die Nachbedingung allenfalls verschärft werden.
• Invarianten werden ebenfalls konjunktiv verknüpft.

Grenzen des Verfahrens

Design By Contract kann nur auf Softwareeigenschaften angewandt werden, die sich auch als Vor- und Nachbedingung formulieren lassen. Bedingungen wie "vor Routine A muss Routine B aufgerufen worden sein" lassen sich (einigermaßen mühsam) über Hilfsvariablen abbilden. Ähnlich können Bedingungen wie "Routine A ruft in ihrem Verlauf immer auch Routine B auf" (gerade im objektorientierten Bereich wichtig) über Nachbedingungen und Modulinvariante gefasst werden.

Wird die Semantik eines Unterprogramms vollständig in Vorbedingungen, Nachbedingungen, und Modulinvarianten gefasst, erhält man eine funktionale Spezifikation des Unterprogramms. Compiler für funktionale Programmiersprachen können solche Nachbedingungen in einigen Fällen direkt in ausführbaren Code umsetzen; insofern zeigt ein bis zur Perfektion getriebenes Vorgehen nach Design By Contract einen Schritt zur nächst abstrakteren Programmiermethodik an.

Weblinks

• Design by Contract als Seminarbericht
• Design by Contract im Eiffel-Tutorial (englisch)