iContract: Dizajn prema ugovoru na Javi

Ne bi li bilo lijepo kada bi svi satovi Java koje koristite, uključujući i vaš vlastiti, ispunili svoja obećanja? Zapravo, ne bi li bilo lijepo kad biste zapravo znali što tačno predavanje obećava? Ako se slažete, pročitajte - Dizajn po ugovoru i iContract dolaze u pomoć.

Napomena: Izvor koda za primjere u ovom članku možete preuzeti s Resursa.

Dizajn po ugovoru

Tehnika razvoja softvera Design by Contract (DBC) osigurava visokokvalitetni softver jamčeći da svaka komponenta sustava ispunjava svoja očekivanja. Kao programer koji koristi DBC, specificirate ugovore o komponentama kao dio sučelja komponente. Ugovorom se precizira što ta komponenta očekuje od klijenata i što klijenti mogu očekivati ​​od nje.

Bertrand Meyer razvio je DBC kao dio svog Eiffelovog programskog jezika. Bez obzira na svoje podrijetlo, DBC je vrijedna tehnika dizajniranja za sve programske jezike, uključujući Java.

Za DBC je središnji pojam tvrdnje - logički izraz o stanju softverskog sustava. Tijekom izvođenja vremena procjenjujemo tvrdnje na određenim kontrolnim točkama tijekom izvršavanja sustava. U valjanom softverskom sustavu sve se tvrdnje smatraju istinitima. Drugim riječima, ako se bilo koja tvrdnja smatra neistinitom, smatramo da je softverski sustav nevaljan ili pokvaren.

Središnji pojam DBC-a donekle se odnosi na #assertmakronaredbe u programskom jeziku C i C ++. Međutim, DBC iznosi tvrdnje na zilion razina dalje.

U DBC-u identificiramo tri različite vrste izraza:

  • Preduvjeti
  • Postuslovi
  • Invarijante

Ispitajmo detaljnije svaku.

Preduvjeti

Preduvjeti određuju uvjete koji moraju biti ispunjeni prije nego što se metoda može izvršiti. Kao takvi, ocjenjuju se neposredno prije izvođenja metode. Preduvjeti uključuju stanje sustava i argumente prenesene u metodu.

Preduvjeti određuju obveze koje klijent softverske komponente mora ispuniti prije nego što se može pozvati na određenu metodu komponente. Ako preduvjet ne uspije, bug se nalazi u klijentu softverske komponente.

Postuslovi

Suprotno tome, postuslovi određuju uvjete koji moraju biti ispunjeni nakon dovršetka metode. Slijedom toga, postuslovi se izvršavaju nakon dovršenja metode. Postuslovi uključuju staro stanje sustava, novo stanje sustava, argumente metode i povratnu vrijednost metode.

Postuslovi određuju jamstva koja softverska komponenta daje svojim klijentima. Ako je prekršen postuslov, softverska komponenta ima pogrešku.

Invarijante

Invarijant specificira uvjet koji mora biti u svakom trenutku kada bi klijent mogao pozvati metodu objekta. Invarijante su definirane kao dio definicije klase. U praksi se invarijante procjenjuju bilo kad prije i nakon izvršavanja metode na bilo kojoj instanci klase. Kršenje invarijante može ukazivati ​​na grešku u klijentu ili softverskoj komponenti.

Tvrdnje, nasljeđivanje i sučelja

Sve tvrdnje navedene za klasu i njene metode primjenjuju se i na sve potklase. Također možete odrediti tvrdnje za sučelja. Kao takve, sve tvrdnje o sučelju moraju sadržavati sve klase koje implementiraju sučelje.

iContract - DBC s Javom

Do sada smo razgovarali o DBC-u općenito. Vjerojatno već imate neku ideju o čemu govorim, ali ako ste novi u DBC-u, stvari bi mogle biti pomalo maglovite.

U ovom će dijelu stvari postati konkretnije. iContract, koji je razvio Reto Kamer, na Javu dodaje konstrukte koji vam omogućavaju da odredite DBC tvrdnje o kojima smo ranije govorili.

Osnove iContract-a

iContract je pretprocesor za Javu. Da biste ga koristili, prvo obradite svoj Java kôd s iContractom, stvarajući skup ukrašenih Java datoteka. Zatim uređujete uređeni Java kôd kao i obično s Java kompajlerom.

Sve iContract direktive u Java kodu nalaze se u komentarima klasa i metoda, baš kao i Javadoc direktive. Na taj način iContract osigurava potpunu kompatibilnost s postojećim Java kodom, a svoj Java kôd uvijek možete izravno kompajlirati bez iContract tvrdnji.

U tipičnom programskom životnom ciklusu sistem biste premjestili iz razvojnog okruženja u testno, a zatim u proizvodno okruženje. U razvojnom okruženju trebali biste svoj kôd urediti tvrdnjama iContract i pokrenuti ga. Na taj način možete rano uhvatiti novouvedene bugove. U testnom okruženju možda ćete i dalje htjeti zadržati omogućen veći dio tvrdnji, ali trebali biste ih izbaciti iz klasa kritičnih za izvedbu. Ponekad čak ima smisla neke tvrdnje omogućiti u proizvodnom okruženju, ali samo u razredima koji definitivno nisu na presudan način za izvedbu vašeg sustava. iContract vam omogućuje izričito odabir klasa koje želite argumentirati tvrdnjama.

Preduvjeti

U iContractu postavljate preduvjete u zaglavlje metode pomoću @predirektive. Evo primjera:

/ ** * @pre f> = 0.0 * / javni plutajući sqrt (float f) {...} 

Primjer preduvjeta osigurava da je argument ffunkcije sqrt()veći ili jednak nuli. Klijenti koji koriste tu metodu odgovorni su za poštivanje tog preduvjeta. Ako to ne učine, mi kao izvršitelji sqrt()jednostavno nismo odgovorni za posljedice.

Izraz iza @preje logički izraz Java.

Postuslovi

Postuslovi se također dodaju zaglavlju komentara metode kojoj pripadaju. U iContractu @postdirektiva definira postuslove:

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

U naš smo primjer dodali postuslov koji osigurava da sqrt()metoda izračuna kvadratni korijen funutar određene margine pogreške (+/- 0,001).

iContract uvodi neke specifične zapise za postkondicije. Prije svega, returnpredstavlja povratnu vrijednost metode. Tijekom izvođenja to će biti zamijenjeno povratnom vrijednošću metode.

Unutar postkondicija često postoji potreba za razlikovanjem vrijednosti argumenta prije izvođenja metode i nakon toga, podržanih u iContractu s @preoperatorom. Ako dodate @preizraz u postkondiciji, on će se procijeniti na temelju stanja sustava prije izvođenja metode:

/** * 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%; _ ugovor_db; instr "-oinstr / @ p / @ f. @ E -k_contract_db / @ p src / *. Java 

Gornja izjava zahtijeva malo objašnjenja.