iContract: Design by Contract in Java

Wäre es nicht schön, wenn alle von Ihnen verwendeten Java-Klassen, einschließlich Ihrer eigenen, ihre Versprechen einhalten würden? Wäre es nicht schön, wenn Sie genau wüssten, was eine bestimmte Klasse verspricht? Wenn Sie einverstanden sind, lesen Sie weiter - Design by Contract und iContract helfen Ihnen dabei.

Hinweis: Die Codequelle für die Beispiele in diesem Artikel kann von Resources heruntergeladen werden.

Design by Contract

Die Softwareentwicklungstechnik Design by Contract (DBC) gewährleistet qualitativ hochwertige Software, indem sichergestellt wird, dass jede Komponente eines Systems ihren Erwartungen entspricht. Als Entwickler unter Verwendung von DBC, geben Sie Komponentenverträge als Teil der Schnittstelle der Komponente. Der Vertrag legt fest, was diese Komponente von Kunden erwartet und was Kunden von ihr erwarten können.

Bertrand Meyer entwickelte DBC als Teil seiner Eiffel-Programmiersprache. Unabhängig von seiner Herkunft ist DBC eine wertvolle Designtechnik für alle Programmiersprachen, einschließlich Java.

Im Zentrum von DBC steht der Begriff einer Behauptung - ein boolescher Ausdruck über den Zustand eines Softwaresystems. Zur Laufzeit werten wir die Zusicherungen an bestimmten Prüfpunkten während der Ausführung des Systems aus. In einem gültigen Softwaresystem werden alle Aussagen als wahr bewertet. Mit anderen Worten, wenn eine Behauptung als falsch bewertet wird, betrachten wir das Softwaresystem als ungültig oder fehlerhaft.

Der zentrale Begriff von DBC bezieht sich etwas auf das #assertMakro in der Programmiersprache C und C ++. DBC führt jedoch Behauptungen zig weiter.

In DBC identifizieren wir drei verschiedene Arten von Ausdrücken:

  • Voraussetzungen
  • Nachbedingungen
  • Invarianten

Lassen Sie uns jedes genauer untersuchen.

Voraussetzungen

Voraussetzungen geben Bedingungen an, die gelten müssen, bevor eine Methode ausgeführt werden kann. Daher werden sie unmittelbar vor der Ausführung einer Methode ausgewertet. Voraussetzungen sind der Systemstatus und die an die Methode übergebenen Argumente.

Voraussetzungen legen Verpflichtungen fest, die ein Client einer Softwarekomponente erfüllen muss, bevor er eine bestimmte Methode der Komponente aufrufen kann. Wenn eine Vorbedingung fehlschlägt, befindet sich ein Fehler im Client einer Softwarekomponente.

Nachbedingungen

Im Gegensatz dazu geben Nachbedingungen Bedingungen an, die nach Abschluss einer Methode gelten müssen. Folglich werden Nachbedingungen ausgeführt, nachdem eine Methode abgeschlossen ist. Nachbedingungen betreffen den alten Systemstatus, den neuen Systemstatus, die Methodenargumente und den Rückgabewert der Methode.

Nachbedingungen geben Garantien an, die eine Softwarekomponente gegenüber ihren Kunden stellt. Wenn eine Nachbedingung verletzt wird, hat die Softwarekomponente einen Fehler.

Invarianten

Eine Invariante gibt eine Bedingung an, die immer dann gelten muss, wenn ein Client die Methode eines Objekts aufrufen kann. Invarianten werden als Teil einer Klassendefinition definiert. In der Praxis werden Invarianten jederzeit vor und nach der Ausführung einer Methode für eine Klasseninstanz ausgewertet. Eine Verletzung einer Invariante kann auf einen Fehler im Client oder in der Softwarekomponente hinweisen.

Behauptungen, Vererbung und Schnittstellen

Alle für eine Klasse und ihre Methoden angegebenen Zusicherungen gelten auch für alle Unterklassen. Sie können auch Zusicherungen für Schnittstellen angeben. Daher müssen alle Zusicherungen einer Schnittstelle für alle Klassen gelten, die die Schnittstelle implementieren.

iContract - DBC mit Java

Bisher haben wir allgemein über DBC gesprochen. Sie haben wahrscheinlich schon eine Idee, wovon ich spreche, aber wenn Sie neu bei DBC sind, sind die Dinge möglicherweise noch etwas neblig.

In diesem Abschnitt werden die Dinge konkreter. iContract, entwickelt von Reto Kamer, fügt Java Konstrukte hinzu, mit denen Sie die DBC-Zusicherungen angeben können, über die wir zuvor gesprochen haben.

iContract-Grundlagen

iContract ist ein Präprozessor für Java. Um es zu verwenden, verarbeiten Sie zuerst Ihren Java-Code mit iContract und erstellen eine Reihe von dekorierten Java-Dateien. Anschließend kompilieren Sie den dekorierten Java-Code wie gewohnt mit dem Java-Compiler.

Alle iContract-Anweisungen in Java-Code befinden sich in Klassen- und Methodenkommentaren, genau wie Javadoc-Anweisungen. Auf diese Weise stellt iContract eine vollständige Abwärtskompatibilität mit vorhandenem Java-Code sicher, und Sie können Ihren Java-Code jederzeit direkt ohne die Zusicherungen von iContract kompilieren.

In einem typischen Programmlebenszyklus würden Sie Ihr System von einer Entwicklungsumgebung in eine Testumgebung und dann in eine Produktionsumgebung verschieben. In der Entwicklungsumgebung instrumentieren Sie Ihren Code mit iContract-Zusicherungen und führen ihn aus. Auf diese Weise können Sie neu eingeführte Fehler frühzeitig erkennen. In der Testumgebung möchten Sie möglicherweise weiterhin den Großteil der Zusicherungen aktiviert lassen, sollten sie jedoch aus leistungskritischen Klassen entfernen. Manchmal ist es sogar sinnvoll, einige Zusicherungen in einer Produktionsumgebung aktiviert zu lassen, jedoch nur in Klassen, die definitiv in keiner Weise für die Leistung Ihres Systems kritisch sind. Mit iContract können Sie die Klassen, die Sie mit Zusicherungen instrumentieren möchten, explizit auswählen.

Voraussetzungen

In iContract platzieren Sie mit der @preDirektive Voraussetzungen in einem Methodenheader . Hier ist ein Beispiel:

/ ** * @pre f> = 0.0 * / public float sqrt (float f) {...} 

Die Beispielvoraussetzung stellt sicher, dass das fFunktionsargument sqrt()größer oder gleich Null ist. Kunden, die diese Methode anwenden, sind dafür verantwortlich, diese Voraussetzung einzuhalten. Wenn nicht, sind wir als Implementierer von sqrt()einfach nicht für die Konsequenzen verantwortlich.

Der Ausdruck nach dem @preist ein Java-Boolescher Ausdruck.

Nachbedingungen

Nachbedingungen werden ebenfalls zum Header-Kommentar der Methode hinzugefügt, zu der sie gehören. In iContract @postdefiniert die Direktive Nachbedingungen:

/ ** * @pre f> = 0.0 * @post Math.abs ((return * return) - f) <0,001 * / public float sqrt (float f) {...} 

In our example, we have added a postcondition that ensures that the sqrt() method calculates the square root of f within a specific margin of error (+/- 0.001).

iContract introduces some specific notations for postconditions. First of all, return stands for the return value of the method. At runtime, that will be replaced by the method's return value.

Within postconditions, there often exists a need to differentiate between the value of an argument before execution of the method and afterwards, supported in iContract with the @pre operator. If you append @pre to an expression in a postcondition, it will be evaluated based on the system state before the method executes:

/** * Append an element to a collection. * * @post c.size() = [email protected]() + 1 * @post c.contains(o) */ public void append(Collection c, Object o) { ... } 

In the code above, the first postcondition specifies that the size of the collection must grow by 1 when we append an element. The expression [email protected] refers to the collection c before execution of the append method.

Invariants

With iContract, you can specify invariants in the header comment of a class definition:

/** * A PositiveInteger is an Integer that is guaranteed to be positive. * * @inv intValue() > 0 */ class PositiveInteger extends Integer { ... } 

In this example, the invariant guarantees that the PositiveInteger's value is always greater than or equal to zero. That assertion is checked before and after execution of any method of that class.

Object Constraint Language (OCL)

Although the assertion expressions in iContract are valid Java expressions, they are modeled after a subset of the Object Constraints Language (OCL). OCL is one of the standards maintained and coordinated by the Object Management Group, or OMG. (OMG takes care of CORBA and related stuff, in case you miss the connection.) OCL was intended to specify constraints within object modeling tools that support the Unified Modeling Language (UML), another standard guarded by OMG.

Because the iContract expressions language is modeled after OCL, it provides some advanced logical operators beyond Java's own logic operators.

Quantifiers: forall and exists

iContract supports forall and exists quantifiers. The forall quantifier specifies that a condition should hold true for every element in a collection:

/* * @invariant forall IEmployee e in getEmployees() | * getRooms().contains(e.getOffice()) */ 

The above invariant specifies that every employee returned by getEmployees() has an office in the collection of rooms returned by getRooms(). Except for the forall keyword, the syntax is the same as that of an exists expression.

Here is an example using exists:

/** * @post exists IRoom r in getRooms() | r.isAvailable() */ 

That postcondition specifies that after the associated method executes, the collection returned by getRooms() will contain at least one available room. The exists proceeds the Java type of the collection element -- IRoom in the example. r is a variable that refers to any element in the collection. The in keyword is followed by an expression that returns a collection (Enumeration, Array, or Collection). That expression is followed by a vertical bar, followed by a condition involving the element variable, r in the example. Employ the exists quantifier when a condition must hold true for at least one element in a collection.

Both forall and exists can be applied to different kinds of Java collections. They support Enumerations, Arrays, and Collections.

Implications: implies

iContract provides the implies operator to specify constraints of the form, "If A holds, then B must hold as well." We say, "A implies B." Example:

/** * @invariant getRooms().isEmpty() implies getEmployees().isEmpty() // no rooms, no employees */ 

That invariant expresses that when the getRooms() collection is empty, the getEmployees() collection must be empty as well. Note that it does not specify that when getEmployees() is empty, getRooms() must be empty as well.

You can also combine the logical operators just introduced to form complex assertions. Example:

/** * @invariant forall IEmployee e1 in getEmployees() | * forall IEmployee e2 in getEmployees() | * (e1 != e2) implies e1.getOffice() != e2.getOffice() // a single office per employee */ 

Constraints, inheritance, and interfaces

iContract propagates constraints along inheritance and interface implementation relationships between classes and interfaces.

Suppose class B extends class A. Class A defines a set of invariants, preconditions, and postconditions. In that case, the invariants and preconditions of class A apply to class B as well, and methods in class B must satisfy the same postconditions that class A satisfies. You may add more restrictive assertions to class B.

The aforementioned mechanism works for interfaces and implementations as well. Suppose A and B are interfaces and class C implements both. In that case, C is subject to invariants, preconditions, and postconditions of both interfaces, A and B, as well as those defined directly in class C.

Beware of side effects!

iContract will improve the quality of your software by allowing you to catch many possible bugs early on. But you can also shoot yourself in the foot (that is, introduce new bugs) using iContract. That can happen when you invoke functions in your iContract assertions that engender side effects that alter your system's state. That leads to unpredictive behavior because the system will behave differently once you compile your code without iContract instrumentation.

The stack example

Let us take a look at a complete example. I have defined the Stack interface, which defines the familiar operations of my favorite data structure:

/** * @inv !isEmpty() implies top() != null // no null objects are allowed */ public interface Stack { /** * @pre o != null * @post !isEmpty() * @post top() == o */ void push(Object o); /** * @pre !isEmpty() * @post @return == top()@pre */ Object pop(); /** * @pre !isEmpty() */ Object top(); boolean isEmpty(); } 

We provide a simple implementation of the interface:

import java.util.*; /** * @inv isEmpty() implies elements.size() == 0 */ public class StackImpl implements Stack { private final LinkedList elements = new LinkedList(); public void push(Object o) { elements.add(o); } public Object pop() { final Object popped = top(); elements.removeLast(); return popped; } public Object top() { return elements.getLast(); } public boolean isEmpty() { return elements.size() == 0; } } 

As you can see, the Stack implementation does not contain any iContract assertions. Rather, all assertions are made in the interface, meaning that the component contract of the Stack is defined in the interface in its entirety. Just by looking at the Stack interface and its assertions, the Stack's behavior is fully specified.

Now we add a small test program to see iContract in action:

public class StackTest { public static void main(String[] args) { final Stack s = new StackImpl(); s.push("one"); s.pop(); s.push("two"); s.push("three"); s.pop(); s.pop(); s.pop(); // causes an assertion to fail } } 

Next, we run iContract to build the stack example:

java -cp% CLASSPATH%; src; _contract_db; instr com.reliablesystems.iContract.Tool -Z -a -v -minv, vor, nach> -b "javac -classpath% CLASSPATH%; src" -c "javac -classpath % CLASSPATH%; Instr "> -n" javac -classpath% CLASSPATH%; _ contract_db; Instr "-oinstr / @ p / @ f. @ E -k_contract_db / @ p src / *. Java 

Die obige Aussage verdient eine kleine Erklärung.