Ahhoz, hogy Eclipse-ben élvezhessük a szerződés alapú fejlesztés előnyeit, néhány beállítást el kell végeznünk. Első lépésként biztosítanunk kell, hogy az Eclipse fejlesztőkörnyezetet egy JDK (ne pedig csak egy JRE) futtassa. Ezt az eclipse.ini konfigurációs állományban a -vm opció értékének kell a JDK bin könyvtárának elérési útját adni, vagyis az alábbi két sort kell megadni, a -vmargs opciót megelőzően:

-vm
<a JDK bin könyvtárának elérési útja>

Példa:

-vm
c:/Program Files/Java/jdk1.7.0_51/bin
-startup
plugins/org.eclipse.equinox.launcher_1.3.0.v20130327-1440.jar
--launcher.library
plugins/org.eclipse.equinox.launcher.win32.win32.x86_64_1.1.200.v20140116-2212
-product
org.eclipse.epp.package.java.product
--launcher.defaultAction
openFile
--launcher.XXMaxPermSize
256M
-showsplash
org.eclipse.platform
--launcher.XXMaxPermSize
256m
--launcher.defaultAction
openFile
--launcher.appendVmargs
-vmargs
-Dosgi.requiredJavaVersion=1.6
-Xms40m
-Xmx512m

A beállítást követően, amennyiben az Eclipse éppen fut, újra kell azt indítani. Emellett be kell szereznünk magát a Contracts for Java osztálykönyvtárat, amelyet a cofoja honlapjáról tölthetünk le (jelen sorok írásakor a legfrissebb változat a cofoja-1.1-r150.jar névre hallgat). Ezt mentsük el, majd adjuk ahhoz a projekthez, amelyben a szerződéseket használni szeretnénk (jobbklikk a projekt nevén → Properties → Java Build Path → Libraries fül → Add JARs... vagy Add External JARs..., attól függően, hogy a munkaterületünkre (workspace) mentettük-e a fenti jar fájlt, avagy sem)! Miután ily módon a classpath-hoz adtuk a fenti jar-t, a com.google.java.contract csomag elemei használhatóak. A cofoja használatát az alábbi egyszerű példán keresztül mutatjuk be:

package hu.unideb.inf.prt.contracts;

import com.google.java.contract.Ensures;
import com.google.java.contract.Requires;
 
public class Contracts {
    public static void main(String[] args) {
        System.out.println(new Numbers().add(-10, 5));
    }
}
 
class Numbers {
    @Requires({ 
    	"c > 0", 
    	"b > 0" 
    })
    @Ensures({ 
    	"result > a", 
    	"result > b" 
    })
    int add(int a, int b) {
        return a - b;
    }
}

Észrevehető, hogy a Numbers osztály add metódusának feltételei nem feltétlenül helyesek (például c változó sehol sem szerepel), de a bemutató szempontjából ez azért nem baj, mert így nyílik lehetőség annak bemutatására, hogy a fejlesztőkörnyezet hogyan hívja fel a figyelmet a hibákra.

A projekt tulajdonságai között (Project Properties) a Java Compiler → Annotation Processing beállítások között mindhárom jelölőnégyzet beállítása után a New... gomb segítségével vigyük fel az alábbi kulcs–érték párokat, mint ahogyan az az Annotációfeldolgozás beállítása ábrán is látható:

2.1. ábra - Annotációfeldolgozás beállítása

Ugyanitt a Factory Path beállításai között szintén be kell állítani a letöltött jar-t, ahogyan az az Annotációfeldolgozót tartalmazó jar beállítása ábrán látható.

2.2. ábra - Annotációfeldolgozót tartalmazó jar beállítása

Egyből meg is kapjuk a c változóról, hogy problémás. Ha ez nem történne meg, akkor a Window menü Preferences menüpontjának kiválasztásával a General → Workspace oldalon be kell állítani a munkaterület automatikus frissítését. Hibák a szerződésekben ábrán látható.

2.3. ábra - Hibák a szerződésekben

Ez azonban csak arra szolgál, hogy az IDE statikusan megjelölje a felderített problémákat, ettől azonban a szerződések futásidejű betartatása nem történik meg, amit könnyen ellenőrizhetünk, ha lefuttatjuk az alkalmazást. Minden további nélküli lefut. A futásidejű ellenőrzéshez ugyanis még egy parancssori virtuálisgép-argumentumot is meg kell adnunk a -javaagent:<jar fájl> opció segítségével. Ezt az Eclipse-ben a Run Configurations... ablak Arguments fülén, a VM arguments szövegmezőben adhatjuk meg. Példa: -javaagent:${project_loc}/lib/cofoja-1.1-r150.jar. A Futásidejű szerződésellenőrzés ábrán látható, hogy a pop művelet üres veremre történő meghívása a size() >= 1 előfeltétel megsértése miatt a PreconditionError hibát okozza.

2.4. ábra - Futásidejű szerződésellenőrzés

Kiinduló példának tekintsük egy verem meglehetősen egyszerű interfészét, amely két metóduból áll: az egyikkel a verem legfelső elemét ki lehet törölni, míg a másikkal egy új elemet lehet hozzáadni a veremhez.

interface Stack<T> {
  public T pop();
  public void push(T obj);
}

Erre az egyszerű interfészre azonban nem könnyű szerződéseket definiálni. Ez azért van, mert az interfész nem biztosít lekérdező metódust, amely anélkül tenné lehetővé az objektum állapotának vizsgálatát, hogy meg kellene változtatni azt. Annak érdekében, hogy egy objektum állapotára vonatkozóan szerződéseket készítsünk, először is hozzá kell férnünk ehhez az állapothoz. Egy ilyen egyszerű információ lehet a verem aktuális elemszáma. Bővítsük tehát interfészünket egy méretlekérdező metódussal:

interface Stack<T> {
  public int size();
  public T pop();
  public void push(T obj);
}

Bár a Java nyelvben az int típus előjeles egészt reprezentál, nyilvánvló, hogy egy veremben sosem lehet negatív számú elem. Elkészíthetjük hát első szerződésünket, egy osztályinvariánst, mivel ennek az állításnak az osztály minden objektumára minden időpillanatban igaznak kell lennie.

import com.google.java.contract.Invariant;

@Invariant("size() >= 0")
interface Stack<T> {
  public int size();
  public T pop();
  public void push(T obj);
}

Ennél azért többet is ki tudnánk fejezni az eszközrendszer segítségével. Például nyilvánvaló, hogy az üres veremből nem szabad törölni, vagyis a veremből törlés előfeltétele, hogy a veremben legalább egy elem legyen.

import com.google.java.contract.Invariant;
import com.google.java.contract.Requires;

@Invariant("size() >= 0")
interface Stack<T> {
  public int size();

  @Requires("size() >= 1")
  public T pop();

  public void push(T obj);
}

Jól látható, hogy a szerződések segítségével hogyan valósul meg az API-tervezés és dokumentálás, ha arra gondolunk, hogy ez a megoldás egy igen konzervatív szemléletmódot tükröz: a klienseknek biztosítaniuk kell, hogy a verem nem üres, hiszen ez a feltétel a törlés előfeltétele. Ekkor a kliens kódja valahogy így nézhet ki (feltételezve, hogy s egy Stack típusú objektum):

if (s.size() > 0)
  s.pop();

Amennyiben a kliens nem így jár el, és az előfeltétel vizsgálata nélkül végzi a pop metódus hívását, azt kockáztatja, hogy a futásidejű előfeltétel-ellenőrzésen a program elbukik. Azonban az objektum és kliensének viszonya ennél sokkal liberálisabb is lehet, például a pop abban az esetben, ha az üres veremből próbálna meg a kliens elemet kivenni,

Ezekben az esetekben a kliens nem kényszerülne rá, hogy a pop művelet meghívását a fentebb látható módon őrfeltétellel lássa el. Bármikor meghívható volna a metódus, és a visszatérési érték alapján vagy az alapján, hogy bekövetkezett-e a kivétel, dönthetné el a kliens, hogy a műveletvégzés sikeres volt-e, avagy sem. Az 1. esetben a pop művelet szerződése a következő módon alakulna (a fenti osztály 8-9. sora):

  @Ensures( "size() != 0 || result == null")
  public T pop();

Figyeljük meg, hogy az előfeltétel eltűnt, vagyis ennek a metódusnak ez esetben nincs előfeltétele, viszont megjelent egy utófeltétel, amely tulajdonképpen egy implikációt ír le: abból, hogy a méret 0 (vagyis a verem üres) következik, hogy a visszaadott értéknek (result) null-nak kell lennie. Ennek logikailag ekvivalens átirata a fenti példában látható.

A 2. esetben a pop művelet szerződésének formája a következő lehetne:

  @ThrowEnsures({"EmptyStackException", "size() == 0"})
  public T pop();

Itt a ThrowEnsures használatára láthatunk példát. Itt kivétel–utófeltétel párokat adhatunk meg, tetszőleges számban. Ha az utófeltétel igaz, az adott kivétel kiváltódására számítunk.

Jó lenne azt is leírni, hogy mit tudunk az objektum állapotáról az egyes metódusok lefutását követően. Tudjuk, hogy ha a veremből kiveszünk egy elemet, akkor a verem elemszáma eggyel csökken, míg ha bővítjük a vermet, akkor eggyel több elem lesz benne. Ezek leírására utófeltételeket használhatunk:

import com.google.java.contract.Ensures;
import com.google.java.contract.Invariant;
import com.google.java.contract.Requires;

@Invariant("size() >= 0")
interface Stack<T> {
  public int size();

  @Requires("size() >= 1")
  @Ensures("size() == old(size()) - 1")
  public T pop();

  @Ensures("size() == old(size()) + 1")
  public void push(T obj);
}

Itt a szerződésfajták megadására szolgáló annotációk mellett egy új elemmel, az old kulcsszóval találkozunk, amely egyike azoknak a bővítéseknek, amelyeket a cofoja keretrendszer támogat.

Az old kulcsszó a régi érték vizsgálatát teszi lehetővé. Régi érték alatt az old paramétereként megadott kifejezésnek a metódushívás kezdetén érvényes értékét értjük.

A szerződéseinket tovább erősíthetjük, ha nem csak az elemszámra, de a tartalomra vonatkozóan is előírásokat teszünk. A top művelet legfelső elemhez történő hozzáférést valósítja meg, anélkül, hogy az adott elemet kivennénk a veremből. Az előfeltétel persze ugyanaz, mint a pop esetében.

import com.google.java.contract.Ensures;
import com.google.java.contract.Invariant;
import com.google.java.contract.Requires;

@Invariant("size() >= 0")
interface Stack<T> {
  public int size();

  @Requires("size() >= 1")
  public T top();

  @Requires("size() >= 1")
  @Ensures("size() == old(size()) - 1")
  public T pop();

  @Ensures("size() == old(size()) + 1")
  public void push(T obj);
}

A top művelet segítségével most már lehetőségünk van a push és pop műveletek szerződését olyan módon bővíteni, hogy a tartalomra vonatkozó állítások is megjelenjenek. A pop által visszaadott elemnek (result) ugyanannak kell lennie, amely a pop hívást megelőzően a verem tetején volt, míg a push művelet esetén az utófeltétel egy olyan részfeltétellel bővül, amely azt állítja, hogy a művelet elvégzése után a verem tetején a push által beszúrt elem áll.

import com.google.java.contract.Ensures;
import com.google.java.contract.Invariant;
import com.google.java.contract.Requires;

@Invariant("size() >= 0")
interface Stack<T> {
  public int size();

  @Requires("size() >= 1")
  public T top();

  @Requires("size() >= 1")
  @Ensures({
    "size() == old(size()) - 1",
    "result == old(top())"
  })
  public T pop();

  @Ensures({
    "size() == old(size()) + 1",
    "top() == old(obj)"
  })
  public void push(T obj);
}

A példából az is látható, hogy a cofoja elvárásai szerint hogyan lehet több részfeltételt egyetlen feltételbe gyömöszölni. Értelemszerűen ez nemcsak az utó-, de az előfeltételekre és az invariánsokra is ugyanilyen módon megadható. Az egyetlen annotációban megadott részfeltételek összeéselődnek.

Készítsünk egy, a fenti interfészt megvalósító konkrét osztályt, amely a vermet egy ArrayList becsomagolásával valósítja meg!

import com.google.java.contract.Ensures;
import com.google.java.contract.Invariant;

import java.util.ArrayList;

@Invariant("elements != null")
public class ArrayListStack<T> implements Stack<T> {
  protected ArrayList<T> elements;

  public ArrayListStack() {
    elements = new ArrayList<T>();
  }

  public int size() {
    return elements.size();
  }

  public T top() {
    return elements.get(elements.size() - 1);
  }

  public T pop() {
    return elements.remove(elements.size() - 1);
  }

  @Ensures("elements.contains(old(obj))")
  public void push(T obj) {
    elements.add(obj);
  }
}

Ennek az osztálynak alig van saját jogú szerződése, azonban az általa implementált Stack interfész összes szerződését megörökli. Egy szerződéssel ellátott típus az összes szülőjének (ősosztályának, illetve az általa implementált interfészeknek) minden szerződését megörökli. Ilyen módon a szerződéseket a szuperosztály–alosztály illetve interfész–implementáló osztály viszonyrendszerekben finomítani lehet. Fontos észben tartani, hogy a felüldefiniált metódusokkal törzsével ellentétben a szerződések nem az eredeti helyett, hanem azt kiegészítve értelmezendőek. Invariánsok és utófeltételek esetén az öröklött szerződésből származó és az újonnan megadott feltételek összeéselődnek, míg az előfeltételek esetén vagy művelettel kombinálhatóak össze. Más szóval, egy metódus mindig legalább annyi állapotot és argumentumot fogad el a bemeneten, mint a szülője (vagyis az előfeltételek csak gyengíthetőek), és legalább annyi garanciát nyújtania kell, mint a szülőjének (vagyis az utófeltételek és invariánsok csak erősíthetőek), máskülönben nem volna ahelyett használható (ami ellentmondana a helyettesíthetőség elvének).

Érdemes megjegyezni, hogy az utolsó példában egy protected adattagra hivatkozó feltételeket adtunk meg. Egy szerződés hatásköre megyegyezik azon metódusdeklarációéval, amelyre vonatkozik, épp ezért pontosan azokat az adattagokat éri el és pontosan azokat a metódusokat hívhatja meg. A korlátozott hozzáféréssel rendelkező tagok elérésére tehát van lehetőség, de a szerződéseinket célszerű nyilvánossá tenni, amikor csak lehet, mert így mintegy dokumentációként is szolgálhatnak. Ezen túlmenően, a korlátozott hozzáférésű tagokra történő hivatkozás nemcsak ellenjavalt, de valójában értelme sem nagyon van.