iContract: Design by Contract in Java

Non sarebbe bello se tutte le classi Java che usi, compresa la tua, mantenessero le loro promesse? In effetti, non sarebbe carino se sapessi esattamente cosa promette una determinata classe? Se sei d'accordo, continua a leggere: Design by Contract e iContract vengono in soccorso.

Nota: il codice sorgente per gli esempi in questo articolo può essere scaricato da Risorse.

Design per contratto

La tecnica di sviluppo software Design by Contract (DBC) assicura software di alta qualità garantendo che ogni componente di un sistema sia all'altezza delle sue aspettative. In qualità di sviluppatore che utilizza DBC, specifichi i contratti dei componenti come parte dell'interfaccia del componente. Il contratto specifica cosa si aspetta quel componente dai clienti e cosa i clienti possono aspettarsi da esso.

Bertrand Meyer ha sviluppato DBC come parte del suo linguaggio di programmazione Eiffel. Indipendentemente dalla sua origine, DBC è una preziosa tecnica di progettazione per tutti i linguaggi di programmazione, incluso Java.

Al centro di DBC è la nozione di asserzione , un'espressione booleana sullo stato di un sistema software. In fase di esecuzione valutiamo le asserzioni a specifici checkpoint durante l'esecuzione del sistema. In un sistema software valido, tutte le asserzioni vengono valutate come vere. In altre parole, se un'asserzione risulta falsa, consideriamo il sistema software non valido o guasto.

La nozione centrale di DBC si riferisce in qualche modo alla #assertmacro nei linguaggi di programmazione C e C ++. Tuttavia DBC porta le asserzioni a livelli infiniti.

In DBC, identifichiamo tre diversi tipi di espressioni:

  • Presupposti
  • Postcondizioni
  • Invarianti

Esaminiamo ciascuno in modo più dettagliato.

Presupposti

Le precondizioni specificano le condizioni che devono essere mantenute prima che un metodo possa essere eseguito. In quanto tali, vengono valutati appena prima dell'esecuzione di un metodo. Le precondizioni riguardano lo stato del sistema e gli argomenti passati nel metodo.

Le precondizioni specificano gli obblighi che un client di un componente software deve soddisfare prima di poter invocare un particolare metodo del componente. Se una precondizione fallisce, un bug è nel client di un componente software.

Postcondizioni

Al contrario, le postcondizioni specificano le condizioni che devono essere mantenute dopo il completamento di un metodo. Di conseguenza, le postcondizioni vengono eseguite dopo il completamento di un metodo. Le postcondizioni riguardano il vecchio stato del sistema, il nuovo stato del sistema, gli argomenti del metodo e il valore restituito dal metodo.

Le postcondizioni specificano le garanzie che un componente software fornisce ai propri clienti. Se viene violata una postcondizione, il componente software presenta un bug.

Invarianti

Un invariante specifica una condizione che deve essere mantenuta ogni volta che un client può richiamare il metodo di un oggetto. Gli invarianti sono definiti come parte di una definizione di classe. In pratica, le invarianti vengono valutate in qualsiasi momento prima e dopo l'esecuzione di un metodo su qualsiasi istanza di classe. Una violazione di un invariante può indicare un bug nel client o nel componente software.

Asserzioni, ereditarietà e interfacce

Tutte le asserzioni specificate per una classe e i suoi metodi si applicano anche a tutte le sottoclassi. È inoltre possibile specificare asserzioni per le interfacce. Pertanto, tutte le asserzioni di un'interfaccia devono valere per tutte le classi che implementano l'interfaccia.

iContract - DBC con Java

Finora abbiamo parlato di DBC in generale. Probabilmente hai un'idea di cosa sto parlando, ma se sei nuovo in DBC, le cose potrebbero ancora essere un po 'confuse.

In questa sezione, le cose diventeranno più concrete. iContract, sviluppato da Reto Kamer, aggiunge costrutti a Java che consentono di specificare le asserzioni DBC di cui abbiamo parlato in precedenza.

Nozioni di base su iContract

iContract è un preprocessore per Java. Per usarlo, devi prima elaborare il tuo codice Java con iContract, producendo una serie di file Java decorati. Quindi si compila il codice Java decorato come al solito con il compilatore Java.

Tutte le direttive iContract nel codice Java risiedono nei commenti di classe e metodo, proprio come le direttive Javadoc. In questo modo, iContract garantisce la completa compatibilità all'indietro con il codice Java esistente e puoi sempre compilare direttamente il tuo codice Java senza le asserzioni di iContract.

In a typical program lifecycle, you would move your system from a development environment into a test environment, then into a production environment. In the development environment, you would instrument your code with iContract assertions and run it. That way you can catch newly introduced bugs early on. In the test environment you may still want to keep the bulk of the assertions enabled, but you should take them out of performance-critical classes. Sometimes it even makes sense to keep some assertions enabled in a production environment, but only in classes that definitely are in no way critical to your system's performance. iContract allows you to explicitly select the classes that you want to instrument with assertions.

Preconditions

In iContract, you place preconditions in a method header using the @pre directive. Here's an example:

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

The example precondition ensures that the argument f of function sqrt() is greater than or equal to zero. Clients who use that method are responsible for adhering to that precondition. If they don't, we as implementors of sqrt() are simply not responsible for the consequences.

The expression after the @pre is a Java Boolean expression.

Postconditions

Postconditions are likewise added to the header comment of the method they belong to. In iContract, the @post directive defines postconditions:

/** * @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, pre, post> -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 

La dichiarazione di cui sopra merita una piccola spiegazione.