Design by Contract in Java

Die Kontrakttypen und was sie bieten

Klasseninvariante

• flat.inv = derived.inv && base.inv
• soll nur geprüft werden wenn keine self-message vorliegt
• d.h. wenn die Methode aus einer anderen Methode der Klasse / des Objektes heraus aufgerufen wurde
• wer verursacht eine self-message? Dasselbe Objekt, dieselbe Klasse, derselbe Type (Klasse und alle Erben)
• prüfen der Klasseninvariante der direkten Super-Klasse
• alternativ können alle Superklassen (bis hin zu java.lang.Object) durchsucht werden
• ein super-call kann nicht generisch eingefügt werden
• dazu muß geprüft werden, ob super-implementierung der Kontrakt-Methode existiert
• bei Nutzung der Reflection muß der Methodenname sich von dem in der Super-Klasse unterscheiden (sonst wird immer spät gebunden)
• vor und nach dem Methoden-Körper prüfen
• nach dem Konstruktor-Körper prüfen
• vor dem Destruktor-Körper prüfen
• eigentlich bei jedem Schreib-Zugriff auf ein Attribut
• bei inneren (und anonymen ?) Klassen muß die Invariante der outer-Klasse geprüft werden
• in welcher Reihenfolge?
• flat.inv = (derived.inv && outer.inv) && base.inv
• flat.inv = (derived.inv && base.inv) && outer.inv
• prüft Attribute
• Unterscheidung in Klassen-Invariante für statische Attribute und Instanz-Invariante für nicht-statische Attribute
• flat.instance.inv = instance.inv && class.inv

Vorbedingung

• flat.pre = (derived.pre || base.pre) && flat.inv
• soll bei self-message (s.o.) nicht geprüft werden
• Möglichkeit um Prüfen der geerbten Vorbedingung zu unterdrücken
• standard ist, die geerbte Vorbedingung mitzuprüfen ("require else")
• geerbte Vorbedingung unterdrücken ("require")
• prüfen der Vorbedingung der Methode in der direkten Super-Klasse
• da die direkte Super-Klasse die Methode evtl. nur erbt, müssen alle Super-Klassen durchsucht werden
• s.o.
• wird vor dem Methoden-Körper geprüft
• nicht vor dem Konstruktor-Körper
• es sollte die Möglichkeit bestehen, eine Vorbedingung anzugeben, die nur die Parameter des Konstruktors prüft
• nicht vor dem Destruktor-Körper
• Zulassen einer Vorbedingung für den Destruktor macht evtl. doch Sinn
• Problem: der Destruktor wird von der JVM implizit aufgerufen, wenn das Objekt vielleicht schon ungültig ist. Deshalb sollte vielleicht auf das Prüfen jeglicher Kontrakte (auch Klassen-Invariante) beim Destruktor verzichtet werden
• prüft die Klassen-/Instanz-Attribute und die Parameter der Methode
• muß auch der Kontrakt einer "geerbten" statischen Klassen-Methode mit derselben Signatur eingehalten werden?

Nachbedingung

• flat.post = (derived.post && base.post) && flat.inv
• soll bei self-message (s.o.) nicht geprüft werden
• Möglichkeit um Prüfen der geerbten Nachbedingung zu unterdrücken
• standard ist, die geerbte Nachbedingung mitzuprüfen ("ensure then")
• geerbte Nachbedingung unterdrücken ("ensure")
• prüfen der Nachbedingung der Methode in der direkten Super-Klasse
• da die direkte Super-Klasse die Methode evtl. nur erbt, müssen alle Super-Klassen durchsucht werden
• s.o.
• wird nach dem Methoden-Körper geprüft
• nicht nach dem Konstruktor-Körper
• es sollte die Möglochkeit bestehen, die Klassen-/Instanz-Attribute nach Ausführen des Konstruktors mit einer Nachbedingung zu prüfen, weil verschiedene Konstruktoren auch verschiedene Semantik haben können, die über die Klasseninvariante hinausgeht
• nicht nach dem Destruktor-Körper
• prüft die Klassen-/Instanz-Attribute, die Werte der Klassen-/Instanz-Attribute vor Ausführen der Methode, den Rückgabewert
• die Werte der Attribute müssen vor Ausführen des Methoden-Körpers gesichert werden ("deep-copy")
• muß auch der Kontrakt einer "geerbten" statischen Klassen-Methode mit derselben Signatur eingehalten werden?

Struktureller Kontrakt

• für Klassen
• "muß die Methode xxx() redefinieren"
• für Methoden
• "muß super-Aufruf vor dem Methoden-Körper machen"
• "muß super-Aufruf nach dem Methoden-Körper machen"

Schleifeninvariante

• die Schleifen-Invariante gilt:
• direkt vor Ausführung der Schleife
• am Anfang des Schleifen-Körpers
• am Ende des Schleifen-Körpers
• direkt nach Ausführung der Schleife
• bei der "for"-Schleife führt das zu dem Problem, daß die Schleifen-Variable erst im Schleifen-Kopf initialisiert wird und schon vorher geprüft werden soll
• z.B. jede "for"-Schleife zuerst in "while"-Schleife umwandeln?

Schleifenvariante

• die Schleifen-Variante muß größer 0 sein
• oder größer gleich
• der Wert der Schleifen-Variante muß am Schleifen-Ende kleiner sein als am Schleifen-Anfang
• oder in jedem Schleifen durchlauf

Check / Assertion

• einfache Zusicherung im Code

Stichworte

• die erzeugten Methoden für die Kontrakte sollen "protected" sein
• wie wird Sicherung der Attribute für "old-checks" gemacht werden?
• wie wird der Methoden-Rückgabewert für "result-checks" behandelt?
• die Bedingungen der Kontrakte sollten alle keine Seiteneffekte haben
• wenn eine Klasse "final" ist, weden ihre Methoden / Attribute (?) geinlinet
• "try / finally" benutzen für die Prüfung der Nachbedingung
• wie werden Exceptions im Methoden-Körper behandelt?
• wie werden Exceptions beim Auswerden einer Kontrakt-Bedingung behandelt?
• wie werden generische Klassen / Methoden (siehe GJ) behandelt?
• wie werden abhängige Klassen erkannt / gefunden?
• was ist mit Klassen, die nicht als Source-Code vorliege?
• javadoc-Doclet anbieten

Wichtige syntaktische Strukturen in Java

Klasse

• Interface
• abstrakte Klasse
• innere Klasse
• statische innere Klasse
• nicht-statische innere Klasse
• anonyme Klasse
• Klasse ist final
• Name der Klasse
• package-Name
• importierte Klassen / packages

Attribute

• statische Attribute
• nicht-statische Attribute
• old-Werte speichern

Methoden

• Rückgabe-Typ
• Name
• Parameter (Typ-Name-Liste)
• Checked / unchecked exceptions
• ist es ein Konstruktor
• ist es ein Destruktor
• die "return"-Statements müssen gefunden werden
• statisch / nicht-statisch
• ist die Methode abstrakt
• in abstrakter Klasse oder in Interface
• welche Sichtbarkeit hat die Methode
• ist die Methode final

Lokale Variablen

• ist die Variable initalisiert?
• das ist wichtig für die Kontrakte Check, Schleifen-Invariante und Schleifen-Variante

Schleifen

• "for"-Schleife
• "while"-Schleife
• "do" ... "while"-Schleife

Lösung / Implementierung