Programování

iContract: Návrh podle smlouvy v Javě

Nebylo by hezké, kdyby všechny třídy Java, které používáte, včetně vašich vlastních, splnily své sliby? Ve skutečnosti by nebylo hezké, kdybyste věděli přesně, co daná třída slibuje? Pokud souhlasíte, přečtěte si - na pomoc přicházejí Design by Contract a iContract.

Poznámka: Zdroj kódu pro příklady v tomto článku lze stáhnout z prostředků.

Návrh podle smlouvy

Technika vývoje softwaru Design by Contract (DBC) zajišťuje vysoce kvalitní software tím, že zaručuje, že každá součást systému splní jeho očekávání. Jako vývojář využívající DBC určíte komponentu smlouvy jako součást rozhraní komponenty. Smlouva specifikuje, co tato složka od klientů očekává a co od ní mohou klienti očekávat.

Bertrand Meyer vyvinul DBC jako součást svého programovacího jazyka Eiffel. Bez ohledu na svůj původ je DBC cennou konstrukční technikou pro všechny programovací jazyky, včetně Javy.

Ústředním bodem DBC je pojem tvrzení - booleovský výraz o stavu softwarového systému. Za běhu vyhodnocujeme tvrzení na konkrétních kontrolních bodech během provádění systému. V platném softwarovém systému se všechna tvrzení hodnotí jako pravdivá. Jinými slovy, pokud se nějaké tvrzení vyhodnotí jako nepravdivé, považujeme softwarový systém za neplatný nebo poškozený.

Ústřední pojem DBC do jisté míry souvisí s #assert makro v programovacím jazyce C a C ++. DBC však posouvá tvrzení o další úroveň.

V DBC identifikujeme tři různé druhy výrazů:

  • Předpoklady
  • Postkondice
  • Invarianty

Podívejme se na každý podrobněji.

Předpoklady

Předpoklady určují podmínky, které musí platit před provedením metody. Jako takové jsou vyhodnoceny těsně před provedením metody. Předpoklady zahrnují stav systému a argumenty předané do metody.

Předpoklady specifikují povinnosti, které musí klient softwarové komponenty splnit, než může vyvolat konkrétní metodu komponenty. Pokud selže předpoklad, je chyba v klientovi softwarové komponenty.

Postkondice

Naproti tomu postconditions určují podmínky, které musí platit po dokončení metody. Následně se postkondice provedou po dokončení metody. Postconditions zahrnují starý stav systému, nový stav systému, argumenty metody a návratovou hodnotu metody.

Postconditions specifikují záruky, které softwarová součást poskytuje svým klientům. Pokud dojde k porušení dodatečné podmínky, obsahuje softwarová součást chybu.

Invarianty

Invariant určuje podmínku, která musí platit kdykoli, kdy by klient mohl vyvolat metodu objektu. Invarianty jsou definovány jako součást definice třídy. V praxi se invarianty vyhodnocují kdykoli před a po provedení metody na jakékoli instanci třídy. Porušení invariantu může znamenat chybu v klientovi nebo softwarové komponentě.

Tvrzení, dědičnost a rozhraní

Všechna tvrzení uvedená pro třídu a její metody platí také pro všechny podtřídy. Můžete také určit tvrzení pro rozhraní. Jako taková musí všechna tvrzení rozhraní platit pro všechny třídy, které implementují rozhraní.

iContract - DBC s Javou

Dosud jsme mluvili o DBC obecně. Pravděpodobně už máte nějakou představu, o čem mluvím, ale pokud jste v DBC noví, může to být stále trochu mlhavé.

V této části se věci stanou konkrétnějšími. iContract, vyvinutý Reto Kamerem, přidává do Javy konstrukce, které umožňují specifikovat tvrzení DBC, o kterých jsme hovořili dříve.

Základy iContract

iContract je preprocesor pro Javu. Chcete-li jej použít, nejprve zpracujete svůj kód Java pomocí aplikace iContract a vytvoříte sadu zdobených souborů Java. Potom kompilováte ozdobený kód Java jako obvykle pomocí kompilátoru Java.

Všechny směrnice iContract v kódu Java jsou umístěny v komentářích tříd a metod, stejně jako směrnice Javadoc. Tímto způsobem iContract zajišťuje úplnou zpětnou kompatibilitu s existujícím kódem Java a svůj kód Java můžete vždy přímo zkompilovat bez tvrzení iContract.

V typickém životním cyklu programu byste přesunuli systém z vývojového prostředí do testovacího prostředí a poté do produkčního prostředí. Ve vývojovém prostředí byste svůj kód vybavili tvrzeními iContract a spustili jej. Tímto způsobem můžete nově chycené chyby chytit brzy. V testovacím prostředí možná budete chtít ponechat většinu tvrzení povolených, ale měli byste je vyjmout z tříd kritických pro výkon. Někdy dokonce dává smysl ponechat některá tvrzení povolená v produkčním prostředí, ale pouze ve třídách, které rozhodně nejsou v žádném případě kritické pro výkon vašeho systému. iContract umožňuje výslovně vybrat třídy, které chcete vybavit tvrzeními.

Předpoklady

V iContract umístíte předpoklady do záhlaví metody pomocí @před směrnice. Zde je příklad:

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

Ukázková podmínka zajišťuje, že argument F funkce sqrt () je větší nebo rovno nule. Za dodržení této podmínky jsou odpovědní klienti, kteří tuto metodu používají. Pokud ne, my jako realizátoři sqrt () prostě nejsou zodpovědní za následky.

Výraz po @před je logický výraz Java.

Postkondice

Postconditions jsou také přidány do komentáře záhlaví metody, ke které patří. V iContractu @pošta direktiva definuje postconditions:

/ ** * @pre f> = 0,0 * @post Math.abs ((návrat * návrat) - f) <0,001 * / veřejný float sqrt (float f) {...} 

V našem příkladu jsme přidali postcondition, který zajišťuje, že sqrt () metoda vypočítá druhou odmocninu z F v rámci určité meze chyby (+/- 0,001).

iContract zavádí některé specifické notace pro postconditions. Předně, vrátit se znamená návratovou hodnotu metody. Za běhu bude nahrazeno návratovou hodnotou metody.

V rámci postconditions často existuje potřeba rozlišovat mezi hodnotou argumentu před provedení metody a poté, podporováno v iContract s @před operátor. Pokud připojíte @před k výrazu v postkondicii, bude vyhodnocen na základě stavu systému před provedením metody:

/ ** * Přidat prvek do kolekce. * * @post c.size () = [email protected] () + 1 * @post c.contains (o) * / public void append (Collection c, Object o) {...} 

Ve výše uvedeném kódu první postcondition určuje, že velikost kolekce musí narůst o 1, když přidáme prvek. Výraz c @ pre odkazuje na sbírku C před provedením připojit metoda.

Invarianty

S iContract můžete zadat invarianty v komentáři záhlaví definice třídy:

/ ** * PositiveInteger je celé číslo, u kterého je zaručeno, že bude kladné. * * @inv intValue ()> 0 * / třída PositiveInteger rozšiřuje celé číslo {...} 

V tomto příkladu invariant zaručuje, že PositiveIntegerHodnota je vždy větší nebo rovna nule. Toto tvrzení se kontroluje před a po provedení jakékoli metody dané třídy.

Object Constraint Language (OCL)

Ačkoli výrazy výrazu v iContractu jsou platné výrazy Java, jsou modelovány podle podmnožiny jazyka Object Constraints Language (OCL). OCL je jedním ze standardů udržovaných a koordinovaných skupinou Object Management Group nebo OMG. (OMG se postará o CORBA a související věci, pokud vám chybí spojení.) OCL bylo určeno k určení omezení v nástrojích pro modelování objektů, které podporují Unified Modeling Language (UML), další standard střežený OMG.

Protože jazyk výrazů iContract je modelován po OCL, poskytuje některé pokročilé logické operátory nad rámec vlastních logických operátorů Java.

Kvantifikátory: vše a existuje

iContract podporuje pro všechny a existuje kvantifikátory. The pro všechny kvantifikátor určuje, že podmínka by měla platit pro každý prvek v kolekci:

/ * * @invariant forall IEmployee e in getEmployees () | * getRooms (). contains (e.getOffice ()) * / 

Výše uvedený invariant určuje, že každý zaměstnanec se vrátil getEmployees () má kancelář ve sbírce pokojů vrácených uživatelem getRooms (). Až na pro všechny klíčové slovo, syntaxe je stejná jako syntaxe existuje výraz.

Zde je příklad použití existuje:

/ ** * @post existuje IRoom r v getRooms () | r.isAvailable () * / 

Tato podmínka určuje, že po provedení přidružené metody se kolekce vrátí getRooms () bude obsahovat alespoň jednu dostupnou místnost. The existuje pokračuje typ Java prvku kolekce - IRoom v příkladu. r je proměnná, která odkazuje na libovolný prvek v kolekci. The v za klíčovým slovem následuje výraz, který vrací kolekci (Výčet, Polenebo Sbírka). Za tímto výrazem následuje svislá čára, za kterou následuje podmínka zahrnující proměnnou prvku, r v příkladu. Zaměstnávejte existuje kvantifikátor, když podmínka musí platit alespoň pro jeden prvek v kolekci.

Oba pro všechny a existuje lze použít na různé druhy sbírek Java. Podporují Výčets, Poles a Sbírkas.

Důsledky: naznačuje

iContract poskytuje naznačuje operátor určit omezení formuláře, "Pokud A platí, pak B musí také platit." Říkáme: „A znamená B.“ Příklad:

/ ** * @invariant getRooms (). isEmpty () znamená getEmployees (). isEmpty () // žádné pokoje, žádní zaměstnanci * / 

Ten invariant to vyjadřuje, když getRooms () sbírka je prázdná, getEmployees () kolekce musí být také prázdná. Všimněte si, že to neurčuje, když getEmployees () je prázdný, getRooms () musí být také prázdné.

Můžete také kombinovat právě zavedené logické operátory a vytvořit složitá tvrzení. Příklad:

/ ** * @invariant pro všechny IEmployee e1 v getEmployees () | * všichni IEmployee e2 v getEmployees () | * (e1! = e2) znamená e1.getOffice ()! = e2.getOffice () // jedna kancelář na zaměstnance * / 

Omezení, dědičnost a rozhraní

iContract šíří omezení podél vztahů dědičnosti a implementace rozhraní mezi třídami a rozhraními.

Předpokládejme třídu B rozšiřuje třídu A. Třída A definuje sadu invariants, preconditions, and postconditions. V takovém případě invarianty a předpoklady třídy A platí pro třídu B a také metody ve třídě B musí vyhovovat stejným podmínkám jako tato třída A splňuje. Do třídy můžete přidat přísnější tvrzení B.

Výše uvedený mechanismus funguje také pro rozhraní a implementace. Předpokládat A a B jsou rozhraní a třída C implementuje obojí. V tom případě, C podléhá invarianty, předběžným podmínkám a dodatečným podmínkám obou rozhraní, A a B, stejně jako ty, které jsou definovány přímo ve třídě C.

Pozor na vedlejší účinky!

iContract zlepší kvalitu vašeho softwaru tím, že vám umožní včas zachytit mnoho možných chyb. Ale můžete si také zastřelit nohu (tj. Představit nové chyby) pomocí iContract. To se může stát, když ve svých tvrzeních iContract vyvoláte funkce, které způsobují vedlejší účinky, které mění stav vašeho systému. To vede k nepředvídatelnému chování, protože systém se bude chovat jinak, jakmile kompilujete svůj kód bez instrumentace iContract.

Příklad zásobníku

Podívejme se na úplný příklad. Definoval jsem Zásobník rozhraní, které definuje známé operace mé oblíbené datové struktury:

/ ** * @inv! isEmpty () znamená top ()! = null // nejsou povoleny žádné objekty null * / veřejné rozhraní zásobníku {/ ** * @pre o! = null * @post! isEmpty () * @post top () == o * / void push (Objekt o); / ** * @pre! isEmpty () * @post @return == top () @ pre * / Object pop (); / ** * @pre! isEmpty () * / Object top (); boolean isEmpty (); } 

Poskytujeme jednoduchou implementaci rozhraní:

import java.util. *; / ** * @inv isEmpty () implikuje elements.size () == 0 * / veřejná třída StackImpl implementuje Stack {private final LinkedList elements = new LinkedList (); public void push (Objekt o) {elements.add (o); } public Object pop () {final Object popped = top (); elements.removeLast (); návrat vyskočil; } public Object top () {return elements.getLast (); } public boolean isEmpty () {return elements.size () == 0; }} 

Jak vidíte, Zásobník implementace neobsahuje žádná tvrzení iContract. Spíše jsou všechna tvrzení prováděna v rozhraní, což znamená, že kontrakt komponenty Stack je definován v rozhraní jako celek. Pouhým pohledem na Zásobník rozhraní a jeho tvrzení, ZásobníkChování je plně specifikováno.

Nyní přidáme malý testovací program, abychom viděli iContract v akci:

public class StackTest {public static void main (String [] args) {final Stack s = new StackImpl (); s.push ("jeden"); s.pop (); s.push ("dva"); s.push ("tři"); s.pop (); s.pop (); s.pop (); // způsobí selhání tvrzení}} 

Dále spustíme iContract, abychom vytvořili příklad zásobníku:

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 

Výše uvedené prohlášení vyžaduje trochu vysvětlení.

$config[zx-auto] not found$config[zx-overlay] not found