Design by contract

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

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

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 ü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, in der das eigentliche Unterprogramm prinzipiell auch aus den 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ächst abstrakteren Programmiermethodik an.

Sprachunterstützung

Einige weniger verbreitete Programmiersprachen wie D und Eiffel unterstützen Design by Contract zumindest teilweise nativ. Für andere Programmiersprachen existieren Frameworks und Präprozessor. Beispielsweise ermöglicht OVal eine Umsetzung in Java, andere Implementierungen wie beispielsweise GContracts ^[1] für Groovy benutzten APIs für Compiler-Erweiterungen um entsprechende Sprachelemente hinzuzufügen.

Siehe auch

• Prinzipien Objektorientierten Designs - weitere Prinzipien objektorientierten Designs

Einzelnachweise

1. ↑ [1]

Weblinks

• Design by Contract als Seminarbericht (PDF-Datei; 184 kB)
• Design by Contract im Eiffel-Tutorial (englisch)