iContract: Дизайн по договор в Java

Не би ли било хубаво, ако всички класове Java, които използвате, включително и вашите собствени, изпълняват обещанията си? Всъщност не би ли било хубаво, ако всъщност знаехте точно какво обещава даден клас? Ако сте съгласни, прочетете - Проектиране по договор и iContract идват на помощ.

Забележка: Източникът на кода за примерите в тази статия може да бъде изтеглен от ресурси.

Проектиране по договор

Техниката за разработка на софтуер Design by Contract (DBC) осигурява висококачествен софтуер, като гарантира, че всеки компонент на системата отговаря на очакванията си. Като разработчик, използващ DBC, вие посочвате договори за компоненти като част от интерфейса на компонента. Договорът определя какво очаква този компонент от клиентите и какво клиентите могат да очакват от него.

Бертран Майер разработи DBC като част от езика си за програмиране Айфел. Независимо от произхода си, DBC е ценна техника за проектиране за всички езици за програмиране, включително Java.

От основно значение за DBC е понятието за твърдение - булев израз за състоянието на софтуерна система. По време на изпълнение оценяваме твърденията на конкретни контролни точки по време на изпълнението на системата. В валидна софтуерна система всички твърдения се оценяват като истина. С други думи, ако дадено твърдение се окаже невярно, ние считаме софтуерната система за невалидна или повредена.

Централното понятие на DBC донякъде се отнася до #assertмакроса в програмния език C и C ++. DBC обаче приема твърденията още милион нива.

В DBC идентифицираме три различни вида изрази:

  • Предпоставки
  • Постусловия
  • Инварианти

Нека разгледаме всеки по-подробно.

Предпоставки

Предпоставките определят условията, които трябва да са налице, преди методът да може да изпълни. Като такива те се оценяват непосредствено преди изпълнението на метода. Предпоставките включват състоянието на системата и аргументите, предадени в метода.

Предпоставките определят задълженията, които клиентът на софтуерен компонент трябва да изпълни, преди да може да се позове на определен метод на компонента. Ако предварително условие се провали, грешка е в клиента на софтуерен компонент.

Постусловия

За разлика от това, следусловията определят условия, които трябва да се изпълняват, след като методът завърши. Следователно, последващите условия се изпълняват, след като методът завърши. Подусловията включват старото състояние на системата, новото състояние на системата, аргументите на метода и връщаната стойност на метода.

Postconditions посочват гаранции, които софтуерният компонент дава на своите клиенти. Ако дадено условие е нарушено, софтуерният компонент има грешка.

Инварианти

Инвариантът посочва условие, което трябва да съдържа всеки път, когато клиентът може да извика метода на обекта. Инвариантите се дефинират като част от дефиниция на клас. На практика инвариантите се оценяват по всяко време преди и след изпълнение на метод на произволен екземпляр на клас. Нарушението на инвариант може да означава грешка в клиента или софтуерния компонент.

Твърдения, наследяване и интерфейси

Всички твърдения, посочени за клас и неговите методи, се прилагат и за всички подкласове. Можете също така да посочите твърдения за интерфейси. Като такива, всички твърдения за интерфейс трябва да се съхраняват за всички класове, които реализират интерфейса.

iContract - DBC с Java

Досега говорихме за DBC като цяло. Вероятно вече имате някаква представа за какво говоря, но ако сте нов в DBC, нещата все още може да са малко мъгливи.

В този раздел нещата ще станат по-конкретни. iContract, разработен от Reto Kamer, добавя конструкции към Java, които ви позволяват да посочите DBC твърденията, за които говорихме по-рано.

Основи на iContract

iContract е препроцесор за Java. За да го използвате, първо обработвате вашия Java код с iContract, създавайки набор от декорирани Java файлове. След това компилирате декорирания Java код както обикновено с Java компилатора.

Всички директиви на iContract в кода на Java се намират в коментари за клас и метод, точно както директивите на Javadoc. По този начин iContract осигурява пълна обратна съвместимост със съществуващия Java код и винаги можете директно да компилирате своя Java код без твърдения на iContract.

В типичен жизнен цикъл на програмата бихте преместили системата си от среда за разработка в тестова среда, след това в производствена среда. В средата за разработка бихте инструментирали кода си с твърдения на iContract и го стартирате. По този начин можете да уловите нововъведени грешки в началото. В тестовата среда все още може да искате да запазите по-голямата част от твърденията активирани, но трябва да ги извадите от критични за изпълнението класове. Понякога дори има смисъл да поддържате някои твърдения активирани в производствена среда, но само в класове, които определено не са по никакъв начин критични за производителността на вашата система. iContract ви позволява изрично да изберете класовете, които искате да инструментирате с твърдения.

Предпоставки

В iContract поставяте предпоставки в заглавката на метода, използвайки @preдирективата. Ето пример:

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

Примерното предварително условие гарантира, че аргументът fна функцията sqrt()е по-голям или равен на нула. Клиентите, които използват този метод, са отговорни за спазването на тази предпоставка. Ако не го направят, ние като изпълнители на sqrt()просто не носим отговорност за последствията.

Изразът след @preе логически израз на Java.

Постусловия

Пост условия се добавят по същия начин към заглавния коментар на метода, към който принадлежат. В iContract @postдирективата дефинира 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%; _ договор_db; instr "-oinstr / @ p / @ f. @ E -k_contract_db / @ p src / *. Java 

Изложението по-горе изисква малко обяснение.