Design by Contract

/ Entwicklung /
Lesezeit: 13 Minuten

Design by Contract (DbC) ist ein Konzept aus der strukturierten bzw. prozeduralen Programmierung, das sich auch auf objektorientierte Programmierung und andere Paradigmen übertragen lässt. Der Begriff wurde von Bertrand Meyer geprägt und fand das erste Mal 1986 Erwähnung. In seiner Programmiersprache Eiffel ist Design by Contract als fester Bestandteil verankert.

Definition

DbC formalisiert den Schnittstellenvertrag zwischen dem Aufrufer (Client) eines Stück Codes und dem Aufgerufenen (Supplier), dem besagten Stück Code. Der Vertrag gliedert sich in Vorbedingungen (preconditions), Nachbedingungen (postconditions) und Invarianten.

Die Vorbedingungen beziehen sich auf die Eingabe- und die Nachbedingungen auf die Ausgabewerte, die Invarianten auf den Zustand vor- und nach Ausführung des Codes. Vorbedingungen, Nachbedingungen und Invarianten werden als boolesche Annahmen formuliert. Die Annahmen haben keine Seiteneffekte und entsprechen damit nach der Command Query Separation von Meyers einer Query.

Die Code-Beispiele im folgenden Abschnitt sind in C-Style-Pseudo-Code geschrieben. Ich gehe später noch darauf ein, welche Sprachen DbC unterstützen.

Vorbedingungen

Vorbedingungen machen dem Client deutlich, unter welchen Umständen und mit welchen Argumenten ein Aufruf durchgeführt werden kann. Sind die Vorbedingungen nicht erfüllt, so wird der Aufruf nicht durchgeführt. Werden die Vorbedingungen im Gegenzug erfüllt, so kann der Client davon ausgehen, dass nach dem Aufruf die Nachbedingungen ebenfalls erfüllt und die Invarianten eingehalten werden.

Die Vorbedingung für eine Methode setAge(), die eine Ganzzahl age entgegennimmt, kann z.B. lauten: Der Wert von age muss größer Null sein. Oder formaler: age > 0

Im folgenden Pseudo-Code wird diese Vorbedingung explizit für diese Funktion gesetzt:

@requires(
    age > 0
)
setAge(age: int) {
    ;
    this.age = age;
}

Ein komplizierteres Beispiel ist die Methode pop() einer Queue-Implementierung: Der Aufruf soll das erste Element der Queue zurückgeben und gleichzeitig aus der Queue entfernen. Eine Vorbedingung für diese Methode könnte wie folgt aussehen:

@requires(
    this.size() > 0
)
pop();

Nachbedingungen

Die Nachbedingungen beschreiben, was erfüllt sein muss, nachdem ein Stück Code durchgelaufen ist. Sie evaluieren damit die Korrektheit des Codes.

Das folgende Beispiel zeigt mögliche Nachbedingungen für eine Funktion, die eine zufällige Zahl in einer angegebenen Spanne zurückgeben soll:

@ensures(
    res >= min
    res <= max
)
rnd(min: int, max: int): int;

Dieses Beispiel zeigt Vor- und Nachbedingungen einer Funktion sqrt() zur Berechnung der Quadratwurzel:

@requires(
    num > 0
)
@ensures(
    res >= 0
    res = 0 if num = 0
    res = 1 if num = 1
    res > num if num < 1
    res < num if num > 1
    res * res = num
)
sqrt(num: float): float;

Die Nachbedingungen machen eine Reihe von Garantieren:

  • Das Ergebnis ist immer größer gleich Null
  • Das Ergebnis ist Null wenn der Eingabewert Null ist
  • Das Ergebnis ist Eins wenn der Eingabewert Eins ist
  • Das Ergebnis ist größer dem Eingabewert wenn der Eingabewert kleiner Eins ist
  • Das Ergebnis ist kleiner dem Eingabewert wenn der Eingabewert größer Eins ist
  • Das Ergebnis mit sich selbst multipliziert ergibt den Eingabewert

Da die Nachbedingungen 2 bis 5 in der letzten Nachbedingung implizit enthalten sind, könnte man sie auch auf die erste und die letzte reduzieren.

Invarianten

Bei den Invarianten kann es sich um Invarianten einer Klasse oder auch Schleife handeln. Für eine jede Methode einer Implementierung von vector in C++ kann beispielsweise gelten, dass die reservierte capacity immer gleich groß oder größer der size sein muss. Für eine Methode gilt: Werden die Invarianten vor ihrem Aufruf erfüllt, so müssen sie auch nach dem Aufruf erfüllt werden.

Für Konstruktoren gelten leicht andere Anforderungen: Die Aufgabe eines Konstruktors ist es, ein Objekt zu initialisieren und die Einhaltung der Invarianten herzustellen. (De-)Serialisierungsframeworks wie ORMs (Object-relational Mappers) verstoßen übrigens in der Regel gegen dieses Prinzip, da sie einen Konstruktor ohne Parameter erfordern und beim Bau des Objektes die Invarianten nicht berücksichtigen.

Schleifeninvarianten entstammen der strukturierten Programmierung und können Bedingungen während des Durchlaufs einer Schleife formalisieren. Für zwei Variablen x und y kann z.B. als Invariante x < y gelten, so dass y innerhalb der Schleife zu jeder Zeit größer als x sein muss.

Unterstützung

Eiffel ist eine der wenigen Sprachen, die DbC als natürlichen Teil der Sprache unterstützt. In Eiffel kann eine Funktion set_day_of_month() wie folgt geschrieben werden:

set_day_of_month(d: INTEGER) is
    require
        valid_day: 0 &lt; d and d &lt;= 31
    do
        day := d
    ensure
        day_updated: day = d
        month_unchanged: month = old month
        year_unchanged: year = old year
    end

Nach dem Schlüsselwort require werden die Vorbedingungen der Funktion aufgeführt. Das Schlüsselwort do markiert den eigentlichen Inhalt der Funktion, der aus einer schlichten Zuweisung besteht. Hinter dem Schlüsselwort require werden drei Nachbedingungen aufgeführt:

  • Die Variable day wurde auf den übergebenen Wert d aktualisiert
  • Die Variable month bleibt unverändert
  • Die Variable year bleibt unverändert

Tatsächlich ist der Inhalt in diesem Fall so eindeutig, dass der Inhalt entfallen kann, da er sich unmittelbar aus den Nachbedingungen ergibt. Damit wird in Eiffel eine deklarative Schreibweise ermöglicht und einfache Funktionen können auf den Schnittstellenvertrag reduziert werden. Ich habe dieses Beispiel übrigens vereinfacht: Der Maximalwert des Tages richtet sich natürlich nach dem Monat (und Schaltjahr) und beträgt nicht in jedem Fall 31.

Dafny und F* sind weitere Sprachen, die DbC unterstützen. Viele Sprachen bieten Mittel, um DbC zum größten Teil abzubilden, darunter Common Lisp, Clojure, Racket und Scala. Für viele Sprachen existieren Frameworks, die DbC zu einem gewissen Grad ermöglichen, u.a. Boost.Contract für C++, Code Contracts für C#, Contracts for Java und Java Modelling Language für Java, dbc-code-contracts für JavaScript, Class::Contract für Perl, PhpDeal für PHP, PyContracts für Python, contracts.ruby für Ruby und contracts für Rust.

Design by Contract und Polymorphie

Für DbC gilt das Liskovsche Substitutionsprinzip (LSP). Für ein Interface oder eine Klasse können Vorbedingungen, Nachbedingungen und Invarianten festgelegt werden. Wird das Interface implementiert oder die Klasse abgeleitet, so muss der Vertrag weiter erfüllt werden.

Gemäß dem LSP dürfen die Vorbedingungen dabei weder verschärft, noch die Nachbedingungen schwächer ausgelegt werden. Die Gegenteile sind aber jeweils erlaubt. Das bedeutet im Detail, wenn eine Funktion als einziges Argument eine Ganzzahl im Wertbereich von 0 bis 9 akzeptiert, so darf eine Ableitung den Wertebereich auf 0 bis 99 erweitern, ihn aber nicht auf 0 bis 5 reduzieren. Ebenso muss die Ableitung die für die Funktion geltenden Nachbedingungen weiterhin gewährleisten, darf aber andersrum zusätzliche Nachbedingungen definieren.

Diese Regeln sind in der Polymorphie begründet. Polymorphie ermöglicht es mir, eine Liste von PKW und Motorrädern als Fahrzeuge zu betrachten, wenn beide ein entsprechendes Interface implementieren bzw. von einer entsprechenden Basisklasse erben. Als Client, der mit dieser Liste arbeitet, muss ich nicht wissen, um welche konkrete Implementierung es sich handelt. Ich kann alle Einträge gleichermaßen als Fahrzeuge betrachten, was bedeutet, dass der Contract für das Fahrzeug von allen Instanzen beachtet wird. Weiß ich hingegen, um welche konkrete Implementierung es sich handelt, so kann ich von den möglicherweise lockereren Vorbedingungen oder strikteren Nachbedingungen Gebrauch machen.

Design by Contract und Defensive Programming

Defensive Programming bezeichnet einen Ansatz, sich nicht auf die korrekte Funktionsweise einer API zu verlassen und mit allem zu rechnen. Die wohl häufigste Form von Defensive Programming ist der defensive Null-Check: Eine bestimmte Funktion sollte eigentlich nie Null zurückgeben. Da es technisch aber möglich ist, weil z.B. jede Objektreferenz in Java null sein kann, sichere ich den nachfolgenden Code nach Aufruf dieser Funktion mit if (foo != null) ab.

DbC ist gewissermaßen das Gegenteil dieses Ansatzes, denn ein Contract kann eindeutig spezifizieren, ob null ein valider Rückgabewert ist oder nicht. Dies gilt zumindest für das mit DbC abgesicherte Ökosystem, für die Kommunikation nach außen kann Defensive Programming auch in Kombination mit DbC seine Berechtigung haben.

Design by Contract, oder: Guard Clauses + Unit-Tests

Eine Guard Clause prüft die Argumente einer Funktion und beendet den Aufruf unmittelbar, wenn eine bestimmte Bedingung erfüllt wird. Die Beendigung kann entweder als Erfolg (z.B. Rückgabewert) oder als Fehler (z.B. durch Auslösen einer Exception) erfolgen.

Für eine Funktion zur Bestimmung, ob eine Zahl eine Primzahl ist, kann z.B. vor dem eigentlichen Algorithmus eine Guard Clause vorgeschaltet werden, die prüft, ob das Argument kleiner zwei ist. Denn in diesem Fall ist sofort klar, dass es sich nicht um eine Primzahl handelt. Eine weitere Guard Clause kann prüfen, ob die Zahl auf 1, 3, 7 oder 9 endet. Denn wenn nicht, dann kann es sich ebenfalls nicht um eine Primzahl handeln. Erst im Anschluss an diese beiden Guard Clauses wird der eigentliche Algorithmus ausgeführt.

Guard Clauses zur Fehlerbehandlung, also ein Aufruf von pop() an einer leeren Queue, null als Wert für ein Argument, das nicht null sein darf, eine Altersangabe kleiner 18 für eine Transaktion, die ein Mindestalter des Kunden von 18 Jahren voraussetzt usw. können gleichermaßen als Vorbedingungen per DbC umgesetzt werden.

Nachbedingungen dokumentieren die Funktionsweise, es handelt sich bei ihnen um eine ausführbare Spezifikation. Damit übernehmen sie die Funktion von automatisierten (Unit-)Tests. Nachbedingungen dokumentieren, was eine Funktion tut. Der Code selbst dokumentiert, wie es getan wird.

Nachbedingungen werden üblicherweise wegen ihres performancetechnischen Overheads in Produktion ausgeschaltet, können aber im Testsystem für alle dort jemals eingehenden Werte und Zustände evaluiert werden. Damit ermöglicht DbC zu einem gewissen Grad Fuzzing, also das Testen zufälliger Werte. Dies ist kein Ersatz für echtes Fuzzing, aber unter Umständen besser, als eine reine Abdeckung durch Unit-Tests, bei der bestimmte Randfälle wie die Division durch Null vergessen wurden.

Design by Contract kann in Summe als eine Teilmenge von Guard Clauses plus Unit-Tests beschrieben werden. Gegenüber herkömmlichen automatischen Tests bietet DbC den potenziellen Vorteil, dass die Eingabewerte durch die Anwender bestimmt werden.

Design by Contract und Domain-driven Design

DbC hat gewisse Parallelen zu Domain-driven Design (DDD). DDD bildet Fachlichkeit (getrennt von der Technik) im Code ab. Die Vorbedingungen einer fachlichen Funktion beschreiben die Rahmenbedingungen, die Nachbedingungen die fachliche Transaktion selbst.

DbC gewährt per Design, dass diese Art der Dokumentation aktuell ist, denn sie wird durch die Ausführung des Codes permanent verifiziert. Gegenüber dem gibt es keine Garantie, dass eine Spezifikation, die nur auf Papier existiert, auch wirklich vom Programm erfüllt wird.

Wie drückt man aus, was eine Funktion tut? Die natürliche Sprache ist oftmals unvollständig, die Perspektive des Dokumentierenden ist subjektiv, unter einer Beschreibung können ein Dutzend Personen ein Dutzend unterschiedlicher Dinge verstehen. Wirken im Laufe der Zeit viele Personen an einem Modul mit, so kommt es unausweichlich zu Unklarheiten, Mehrdeutigkeiten und Widersprüchen. DDD setzt auf eine eindeutige Sprache, die Ubiquitous Language. DbC verfolgt über die formale, boolesche Schreibweise der Bedingungen die gleichen Ziele. Beide Ansätze wollen Klarheit, Eindeutigkeit und Unmissverständlichkeit schaffen.

Fazit

Ich finde den Ansatz Design by Contract hochspannend und würde mir von mehr Sprachen eine native Unterstützung bieten. DbC kann ein guter Beitrag zur Robustheit und Korrektheit eines Programmes sein und wie eine gute Testabdeckung kann DbC maßgeblich zur Qualität des Codes beitragen, da man mehr reflektiert und schlechte Designansätze häufiger noch zur Entwurfszeit bemerkt und überarbeiten kann. Um einen spürbaren Mehrwert zu liefern, sollte DbC aber natürlich in einer Sprache verankert werden. Viele Bibliotheken für Sprachen, die keine guten natürlichen Mittel dafür zur Verfügung stellen, wirken etwas holprig und kommen mit ihren eigenen Nachteilen, sei es weil eine native domänenspezifische Sprache fehlt und die Ausdrücke in Strings verpackt werden müssen, sei es weil die Statements mit dem Rest der Methode im Body untergebracht werden und die IDE damit nicht optimal umgehen kann, indem sie z.B. anbietet den Contract ein- und auszublenden oder beim Bewegen des Mauszeigers über eine Funktion nicht nur die Dokumentation sondern auch die „Vertragsdetails“ anzuzeigen.