Design by Contract

Design by contract (kurz DbC, englisch für Entwurf gemäß Vertrag) oder Programming by Contract (‚Vertragsbasierte Programmierung‘) 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.

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

• Vorbedingungen (englisch precondition), also den Zusicherungen, die der Aufrufer einzuhalten hat
• Nachbedingungen (englisch postcondition), also den Zusicherungen, die der Aufgerufene einhalten wird, sowie den
• Invarianten (englisch class invariants), über alle Instanzen einer Klasse hinweg geltende Grundannahmen.

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 anderes 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 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.

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.

Wendet man das liskovsche Substitutionsprinzip auf Vor- und Nachbedingungen an, erhält man die folgende Aussage:

Sind vor dem Aufruf einer Methode der Unterklasse die Vorbedingungen der Oberklasse erfüllt, so muss die Methode die Nachbedingungen der Oberklasse erfüllen.

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

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

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

• Die Vorbedingungen werden disjunktiv (mit logischem ODER) verknüpft. Dadurch kann die Vorbedingung der Oberklasse nur abgeschwächt, aber nicht verschärft werden.
• Die Nachbedingungen werden konjunktiv (logisches UND) verknüpft. Hierdurch kann die Nachbedingung nur verschärft, aber nicht abgeschwächt werden.
• Invarianten werden ebenfalls konjunktiv verknüpft.

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 über Statusvariablen abbilden. Das bedeutet einerseits erhöhten Aufwand für die Programmierung der Klasse, andererseits können Verwender darauf verzichten, ein derart ausgerüstetes Objekt permanent unter ihrer Kontrolle zu halten, sondern können es an andere Funktionen weiterreichen und hinterher auf etwaige Statusänderungen reagieren. Ähnlich können Bedingungen wie „Routine A ruft in ihrem Verlauf immer auch Routine B auf“ (gerade im objektorientierten Bereich wichtig) über Nachbedingungen und Modulinvarianten gefasst werden.

Stützt sich eine Invariante auf Hilfsobjekte, kann die Invariante durch Aliasing zerstört werden. Werden Invarianten zusätzlich zu Beginn jeder Unterroutine geprüft, kann die Zerstörung der Invariante zwar verlässlich diagnostiziert werden, bevor das Programm aufgrund einer solchen Invariantenverletzung Fehlentscheidungen trifft, doch erhält der Programmierer keinen Hinweis darauf, wo der Alias erzeugt wurde und bei welcher Modifikation des Hilfsobjekts die Invariante tatsächlich zerstört wurde.

Wird die Semantik eines Unterprogramms vollständig in Vorbedingungen, Nachbedingungen, und Modulinvarianten gefasst, erhält man eine funktionale Spezifikation des Unterprogramms, aus der das eigentliche Unterprogramm prinzipiell mittels der Zusicherungen generiert werden könnte. Derartige Generatoren lassen sich aus den Compilertechniken für funktionale Programmiersprachen erstellen; insofern zeigt ein bis zur Perfektion getriebenes Vorgehen nach Design By Contract einen Schritt zur nächstabstrakteren Programmiermethodik an.

Einige weniger verbreitete Programmiersprachen wie D und Eiffel unterstützen Design by Contract zumindest teilweise nativ, auch Ada seit Ada 2012. Das .NET Framework enthält ab Version 4.0 eine Klassenbibliothek (vor allem im Namensraum System.Diagnostics.Contracts), die auch als Code Contracts bezeichnet wird, zur Implementierung von Design by Contract.^[1] Das Bean Validation Konzept bietet in Java dieselbe Möglichkeit, darüber hinaus ist es seit der Java Bean Validation 1.1 möglich, Vor- und Nachbedingungen direkt in Methodenheadern mittels Annotations umzusetzen.^[2][3] Dies war zuvor schon über das Framework OVal oder die Java Modelling Language (kurz JML)^[4] in Java möglich. Andere Implementierungen wie beispielsweise GContracts^[5] für Groovy benutzten APIs für Compiler-Erweiterungen um entsprechende Sprachelemente hinzuzufügen.

• Prinzipien objektorientierten Designs – weitere Prinzipien objektorientierten Designs

• Design by Contract als Seminarbericht (PDF; 184 kB) gruntz.ch
• Design by Contract. In: Eiffel-Tutorial (englisch)

1. ↑ msdn.microsoft.com
2. ↑ Parameter constraints mittels Java Bean Validation 1.1
3. ↑ Return value constraints mittels Java Bean Validation 1.1
4. ↑ eecs.ucf.edu Abgerufen am 6. Februar 2015
5. ↑ github.com