Dienstag, August 29, 2006

Netze spannen mit Design by Contract

Was verbirgt sich hinter diesem Methodenaufruf?

method float squareRoot(float: number)

Eine Methode namens "squareRoot" (Quadratwurzel), die zu ihrem Aufruf eine Fließkommazahl "number" erwartet und eine Fließkommazahl zurückgibt. Es ist unschwer zu erraten, was die Methode tut. Sie berechnet die Wurzel zu einer Zahl. Sicher?

Die Vermutung, was die Methode macht, begründet sich einzig auf der Namensgebung. Namen sind äußerst wichtig -- nicht nur beim Programmieren. Ein Name löst bei uns Menschen eine Menge aus. Wir verbinden mit Namen Erfahrungswerte, ordnen ihnen Bedeutung (Semantik) zu etc. Allerdings klären Namen nicht unbedingt alles ab. Akzeptiert die Methode auch negative Zahlen als Eingabe? Was passiert dann? Liefert die Methode nur die positive Lösung zu einer Wurzel oder auch die negative Lösung? (Die Wurzel aus 4 ist 2, aber auch -2 ist ein gültiges Ergebnis: -2 mal -2 = 4.)

Es gibt Techniken, Methoden wesentlich präziser zu spezifizieren als rein über die Typen, wie das z.B. bei Java, C# und vielen anderen objektorientierten Sprachen der Fall ist. Mit sogenannten Vor- und Nachbedingungen, pre-conditions und post-conditions läßt sich obiges Beispiel genauer fassen:

method float squareRoot(float: number):
pre: number >= 0
post: result >= 0 and result * result == number

Die Methode wird detailliert über die Vorbedingung, die angibt, was die Methode bei ihrem Aufruf vom Aufrufenden erwartet: "Gibst Du mir eine Fließkommazahl, die positiv ist, dann garantiere ich Dir die Einhaltung der Nachbedingung." Die Variable "result" ist vordefiniert und veweist auf den Rückgabewert der Methode, das Ergebnis. Die Methode garantiert über die Nachbedingung, dass das Ergebnis größer Null ist und mit sich selbst multipliziert gleich "number" ist.

Jetzt ist zweifelsfrei geklärt, unter welchen Bedingungen die Methode arbeitet und was sie zusichert bzw. garantiert. Dabei bleibt völlig offen, wie die Methode programmiert ist und wie sie den Wurzelwert ermittelt.

Diese Art der Spezifikation einer Methode hat einen Namen und ist als Design by Contract (DbC) bekannt; sie geht auf Betrand Meyer zurück und findet Verwendung in der von ihm entwickelten Programmiersprache Eiffel.

Leider wird DbC im Software Engineering noch viel zu wenig verwendet. Dabei ist es eine so wichtige, klarstellende und leistungsfähige Technik. Interfaces werden ähnlich schwach wie die Methode ganz oben definiert. Sie kennen das bestimmt von Java, C# oder einer anderen Programmiersprache. Die reinen Typ-Angaben spannen zwar ein Netz, innerhalb dessen die Software läuft -- und ein Compiler prüft, ob das Netz aus Typangaben auch sauber gespannt ist. Aber die Netzmaschen sind zu groß. Es können noch viele Fehlannahmen und Fehler durch das Netz fallen.

Design by Contract erlaubt es Ihnen, das Netz so engmaschig zu spannen, wie es Ihnen sinnvoll erscheint. Vielleicht hätte es bei der obigen Postcondition genügt, einzig ein positives Ergebnis zuzusichern. Man könnte das Netz aber auch engmaschiger spannen und die Genauigkeit des Ergebnisses spezifizieren (was bei endlicher Fließkomma-Arithmetik notwendig ist).

Kommentare:

maurice hat gesagt…

In Programmiersprachen wie Java, C#, etc. bleiben als "Ersatz" für pre- und post-conditions nur Quellcode-Kommentare (mindestens in der Interface-Deklaration) und die üblichen Entwicklerdokumentationen --- oder?

dh hat gesagt…

Allgemein kann man Assertions für diese Zwecke benutzen, die meisten Programmiersprachen kennen ein entsprechendes Schlüsselwort dazu. Näher an die Idee des DbC kommen Tools, die es erlauben Direktiven wie @pre und @post in Kommentaren zu z.B. Methoden zu verwenden. Per Pre-Compiler werden dann entsprechende Code-Fragmente (z.B. Assertions) in den Code eingebunden. Eine interessante Entwicklung zum Thema ist Spec# von Microsoft für .NET. Ansonsten ist es auch interessant, sich mit Sprachen wie Eiffel zu beschäftigen, die DbC "eingebaut" haben.

maurice hat gesagt…

Spec# ist in der Tat sehr interessant. Beispiel: Die Methode GetString erwartet einen Parameter, der nicht null sein darf:

public virtual string GetString(byte[] bytes);

Wird dennoch null übergeben, so wird eine Exception ausgelöst. Dies wird in der Dokumentation oder im Quellcode erwähnt:

A NullArgumentException will be thrown if bytes is null.

In Spec# könnte eine Validierung des Parameters durch eine pre-condition wie folgt aussehen:

public virtual string GetString(byte[] bytes)
requires bytes != null;

Siehe auch Exception safety for C# (PDF).

Hübsch! :-)