iContract: Design by Contract w Javie

Czy nie byłoby miło, gdyby wszystkie klasy Java, których używasz, w tym własne, spełniały swoje obietnice? Właściwie, czy nie byłoby miło, gdybyś wiedział dokładnie, co obiecuje dana klasa? Jeśli się zgadzasz, czytaj dalej - z pomocą przychodzą Design by Contract i iContract.

Uwaga: źródło kodu dla przykładów w tym artykule można pobrać z zasobów.

Zaprojektuj według umowy

Technika tworzenia oprogramowania Design by Contract (DBC) zapewnia wysoką jakość oprogramowania, gwarantując, że każdy element systemu spełnia jego oczekiwania. Jako programista korzystający z DBC, określasz kontrakty komponentów jako część interfejsu komponentu. Umowa określa, czego ten składnik oczekuje od klientów i czego klienci mogą się po nim spodziewać.

Bertrand Meyer opracował DBC jako część swojego języka programowania Eiffel. Niezależnie od pochodzenia, DBC jest cenną techniką projektowania dla wszystkich języków programowania, w tym Java.

Centralne znaczenie dla DBC ma pojęcie asercji - logicznego wyrażenia dotyczącego stanu systemu oprogramowania. W czasie wykonywania oceniamy asercje w określonych punktach kontrolnych podczas wykonywania systemu. W prawidłowym systemie oprogramowania wszystkie stwierdzenia są prawdziwe. Innymi słowy, jeśli jakiekolwiek stwierdzenie zostanie ocenione jako fałszywe, uważamy, że system oprogramowania jest nieprawidłowy lub uszkodzony.

Główne pojęcie DBC w pewnym stopniu odnosi się do #assertmakra w języku programowania C i C ++. Jednak DBC idzie o miliony poziomów dalej.

W DBC identyfikujemy trzy różne rodzaje wyrażeń:

  • Warunki wstępne
  • Warunki końcowe
  • Niezmienniki

Przyjrzyjmy się każdemu bardziej szczegółowo.

Warunki wstępne

Warunki wstępne określają warunki, które muszą być spełnione, zanim metoda będzie mogła zostać wykonana. W związku z tym są oceniane tuż przed wykonaniem metody. Warunki wstępne dotyczą stanu systemu i argumentów przekazanych do metody.

Warunki wstępne określają obowiązki, które klient składnika oprogramowania musi spełnić, zanim będzie mógł wywołać określoną metodę składnika. Jeśli warunek wstępny zawiedzie, w kliencie składnika oprogramowania występuje błąd.

Warunki końcowe

Z kolei warunki końcowe określają warunki, które muszą zostać spełnione po zakończeniu metody. W rezultacie warunki końcowe są wykonywane po zakończeniu metody. Warunki końcowe obejmują stary stan systemu, nowy stan systemu, argumenty metody i wartość zwracaną przez metodę.

Warunki końcowe określają gwarancje, które składnik oprogramowania zapewnia swoim klientom. Jeśli zostanie naruszony warunek końcowy, w komponencie oprogramowania występuje błąd.

Niezmienniki

Niezmienny określa warunek, który musi obowiązywać za każdym razem, gdy klient może wywołać metodę obiektu. Niezmienniki są definiowane jako część definicji klasy. W praktyce niezmienniki są oceniane w dowolnym momencie przed i po wykonaniu metody w dowolnej instancji klasy. Naruszenie niezmiennika może wskazywać na błąd w kliencie lub w komponencie oprogramowania.

Asercje, dziedziczenie i interfejsy

Wszystkie potwierdzenia określone dla klasy i jej metod mają również zastosowanie do wszystkich podklas. Możesz również określić potwierdzenia dla interfejsów. W związku z tym wszystkie potwierdzenia interfejsu muszą być utrzymywane dla wszystkich klas implementujących interfejs.

iContract - DBC z Javą

Do tej pory rozmawialiśmy ogólnie o DBC. Prawdopodobnie masz już jakiś pomysł, o czym mówię, ale jeśli jesteś nowy w DBC, sprawy mogą być nieco mgliste.

W tej sekcji sprawy staną się bardziej konkretne. iContract, opracowany przez Reto Kamer, dodaje konstrukcje do Javy, które pozwalają określić twierdzenia DBC, o których mówiliśmy wcześniej.

Podstawy iContract

iContract to preprocesor dla języka Java. Aby z niego skorzystać, najpierw przetwarzasz kod Java za pomocą iContract, tworząc zestaw ozdobionych plików Java. Następnie w zwykły sposób kompilujesz ozdobiony kod Java za pomocą kompilatora Java.

Wszystkie dyrektywy iContract w kodzie Java znajdują się w komentarzach klas i metod, podobnie jak dyrektywy Javadoc. W ten sposób iContract zapewnia pełną kompatybilność wsteczną z istniejącym kodem Java i zawsze możesz bezpośrednio skompilować swój kod Java bez asercji iContract.

W typowym cyklu życia programu należy przenieść system ze środowiska programistycznego do środowiska testowego, a następnie do środowiska produkcyjnego. W środowisku programistycznym możesz instrumentować swój kod za pomocą asercji iContract i uruchamiać go. W ten sposób możesz wcześnie wychwycić nowo wprowadzone błędy. W środowisku testowym możesz nadal chcieć pozostawić włączoną większość asercji, ale powinieneś usunąć je z klas krytycznych dla wydajności. Czasami nawet ma sens, aby niektóre asercje były włączone w środowisku produkcyjnym, ale tylko w klasach, które z pewnością nie są w żaden sposób krytyczne dla wydajności systemu. iContract umożliwia jawne wybieranie klas, do których mają być przypisane asercje.

Warunki wstępne

W iContract warunki wstępne umieszcza się w nagłówku metody za pomocą @predyrektywy. Oto przykład:

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

Przykładowy warunek wstępny zapewnia, że ​​argument ffunkcji sqrt()jest większy lub równy zero. Klienci korzystający z tej metody są odpowiedzialni za przestrzeganie tego warunku wstępnego. Jeśli tego nie zrobią, my jako realizatorzy sqrt()po prostu nie odpowiadamy za konsekwencje.

Wyrażenie po @preznaku jest wyrażeniem logicznym Java.

Warunki końcowe

Warunki końcowe są również dodawane do komentarza nagłówka metody, do której należą. W iContract @postdyrektywa definiuje warunki końcowe:

/ ** * @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 

Powyższe stwierdzenie zasługuje na trochę wyjaśnienia.