Programovanie

iContract: Návrh podľa zmluvy v Jave

Nebolo by pekné, keby všetky triedy Java, ktoré používate, vrátane svojich vlastných, splnili svoje sľuby? V skutočnosti by nebolo pekné, keby ste skutočne presne vedeli, čo daná trieda sľubuje? Ak súhlasíte, prečítajte si ďalej - na pomoc prichádzajú Design by Contract a iContract.

Poznámka: Zdroj kódu pre príklady v tomto článku si môžete stiahnuť zo stránky Zdroje.

Návrh podľa zmluvy

Technika vývoja softvéru Design by Contract (DBC) zaisťuje vysoko kvalitný softvér tým, že zaručuje, že každá súčasť systému spĺňa svoje očakávania. Ako vývojár využívajúci DBC určíte komponent zmluvy ako súčasť rozhrania komponentu. Zmluva špecifikuje, čo táto zložka od klientov očakáva a čo od nej môžu klienti očakávať.

Bertrand Meyer vyvinul DBC ako súčasť svojho programovacieho jazyka Eiffel. Bez ohľadu na svoj pôvod je DBC cennou technikou návrhu pre všetky programovacie jazyky vrátane Java.

Pre DBC je ústredný pojem tvrdenie - boolovský výraz o stave softvérového systému. Počas behu vyhodnocujeme tvrdenia na konkrétnych kontrolných bodoch počas vykonávania systému. V platnom softvérovom systéme sa všetky tvrdenia hodnotia ako pravdivé. Inými slovami, ak sa nejaké tvrdenie vyhodnotí ako nepravdivé, považujeme softvérový systém za neplatný alebo poškodený.

Centrálna predstava DBC sa trochu týka #assert makro v programovacom jazyku C a C ++. DBC však berie tvrdenia o niekoľko miliárd úrovní ďalej.

V DBC identifikujeme tri rôzne druhy výrazov:

  • Predpoklady
  • Dodatočné podmienky
  • Invarianty

Pozrime sa na každú podrobnejšie.

Predpoklady

Predpoklady určujú podmienky, ktoré musia byť splnené, aby sa metóda mohla vykonať. Preto sa hodnotia tesne pred vykonaním metódy. Predpoklady zahŕňajú stav systému a argumenty odovzdané do metódy.

Predpoklady určujú povinnosti, ktoré musí klient softvérového komponentu splniť, aby mohol uplatniť konkrétnu metódu komponentu. Ak predbežná podmienka zlyhá, chyba je v klientovi softvérového komponentu.

Dodatočné podmienky

Naproti tomu postconditions určujú podmienky, ktoré musia platiť po dokončení metódy. Následne sa vykonajú postconditions po dokončení metódy. Postconditions zahŕňajú starý stav systému, nový stav systému, argumenty metódy a návratovú hodnotu metódy.

Postconditions špecifikujú záruky, ktoré softvérový komponent poskytuje svojim klientom. Ak dôjde k porušeniu dodatočnej podmienky, softvérový komponent obsahuje chybu.

Invarianty

Invariant určuje podmienku, ktorá musí platiť kedykoľvek, keď by klient mohol vyvolať metódu objektu. Invarianty sú definované ako súčasť definície triedy. V praxi sa invarianty hodnotia kedykoľvek pred a po vykonaní metódy v ktorejkoľvek inštancii triedy. Porušenie invariantu môže naznačovať chybu v klientovi alebo softvérovom komponente.

Tvrdenia, dedičstvo a rozhrania

Všetky tvrdenia uvedené pre triedu a jej metódy sa rovnako vzťahujú na všetky podtriedy. Môžete tiež určiť tvrdenia pre rozhrania. Preto musia všetky tvrdenia o rozhraní platiť pre všetky triedy, ktoré rozhranie implementujú.

iContract - DBC s Java

Doteraz sme hovorili o DBC všeobecne. Pravdepodobne už máte určitú predstavu, o čom hovorím, ale ak ste v DBC nováčikom, môže to byť stále trochu hmlisté.

V tejto časti sa veci stanú konkrétnejšími. iContract, vyvinutý Reto Kamerom, pridáva do Javy konštrukty, ktoré vám umožňujú určiť tvrdenia DBC, o ktorých sme hovorili už skôr.

iContract základy

iContract je preprocesor pre Javu. Ak ho chcete použiť, najskôr spracujete svoj kód Java pomocou programu iContract a vytvoríte sadu zdobených súborov Java. Potom ozdobený kód Java skompilujete ako obvykle pomocou kompilátora Java.

Všetky smernice iContract v kóde Java sú obsiahnuté v komentároch tried a metód, rovnako ako smernice Javadoc. Týmto spôsobom iContract zaisťuje úplnú spätnú kompatibilitu s existujúcim kódom Java a svoj kód Java môžete kedykoľvek priamo zostaviť bez tvrdení iContract.

V typickom životnom cykle programu by ste svoj systém presunuli z vývojového prostredia do testovacieho prostredia a potom do produkčného prostredia. Vo vývojovom prostredí by ste svoj kód vybavili tvrdeniami iContract a spustili by ste ho. Týmto spôsobom môžete čoskoro chytiť novo zavedené chyby. V testovacom prostredí možno budete chcieť ponechať väčšinu tvrdení povolených, mali by ste ich však vyradiť z tried kritických pre výkon. Niekedy má dokonca zmysel ponechať niektoré tvrdenia povolené v produkčnom prostredí, ale iba v triedach, ktoré rozhodne nie sú nijako dôležité pre výkon vášho systému. iContract vám umožňuje výslovne zvoliť triedy, ktoré chcete vybaviť tvrdeniami.

Predpoklady

V iContracte dávate predpoklady do hlavičky metódy pomocou @ pr smernice. Tu je príklad:

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

Príklad predpokladá, že argument f funkcie sqrt () je väčšie alebo rovné nule. Za dodržanie tejto podmienky sú zodpovední klienti, ktorí používajú túto metódu. Ak to neurobia, sme ako realizátori sqrt () jednoducho nie sú zodpovední za následky.

Výraz po @ pr je logický výraz Java.

Dodatočné podmienky

Postconditions sa tiež pridajú do komentára k hlavičke metódy, ku ktorej patria. V aplikácii iContract @ príspevok smernica definuje následné podmienky:

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

V našom príklade sme pridali postcondition, ktorá zaisťuje, že sqrt () metóda počíta druhú odmocninu z f v rámci konkrétnej chyby (+/- 0,001).

iContract zavádza niektoré špecifické notácie pre postconditions. Po prvé, návrat znamená návratovú hodnotu metódy. Za behu bude nahradená návratovou hodnotou metódy.

V rámci postconditions často existuje potreba rozlišovať medzi hodnotou argumentu predtým vykonanie metódy a potom, podporované v iContract s @ pr operátor. Ak pridáš @ pr k výrazu v postcondition, bude vyhodnotený na základe stavu systému pred vykonaním metódy:

/ ** * Pripojiť prvok do zbierky. * * @post c.size () = [email protected] () + 1 * @post c.contains (o) * / public void append (kolekcia c, objekt o) {...} 

V kóde vyššie prvá postcondition určuje, že veľkosť kolekcie musí po pripojení prvku narásť o 1. Výraz c @ pre odkazuje na zbierku c pred vykonaním pridať metóda.

Invarianty

Pomocou aplikácie iContract môžete určiť invarianty v komentári k záhlaví definície triedy:

/ ** * PositiveInteger je celé číslo, ktoré bude zaručene pozitívne. * * @inv intValue ()> 0 * / trieda PositiveInteger rozširuje celé číslo {...} 

V tomto príklade invariant zaručuje, že: PositiveIntegerhodnota je vždy väčšia alebo rovná nule. Toto tvrdenie sa kontroluje pred a po vykonaní akejkoľvek metódy tejto triedy.

Object Constraint Language (OCL)

Aj keď sú výrazy výrazu v iContract platné výrazy Java, sú modelované podľa podmnožiny jazyka Object Constraints Language (OCL). OCL je jedným zo štandardov udržiavaných a koordinovaných skupinou Object Management Group alebo OMG. (OMG sa stará o CORBA a súvisiace veci, ak vám chýba spojenie.) Cieľom OCL bolo špecifikovať obmedzenia v rámci nástrojov na modelovanie objektov, ktoré podporujú Unified Modeling Language (UML), ďalší štandard strážený OMG.

Pretože jazyk výrazov iContract je modelovaný podľa OCL, poskytuje niektoré pokročilé logické operátory nad rámec vlastných logických operátorov Javy.

Kvantifikátory: všetko a existuje

iContract podporuje pre všetkých a existuje kvantifikátory. The pre všetkých kvantifikátor určuje, že podmienka by mala platiť pre každý prvok v kolekcii:

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

Vyššie uvedený invariant určuje, že každý zamestnanec sa vrátil do getEmployees () má kanceláriu v zbierke miestností vrátených používateľom getRooms (). Okrem pre všetkých kľúčové slovo, syntax je rovnaká ako v prípade existuje výraz.

Tu je príklad použitia existuje:

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

Táto podmienka určuje, že po vykonaní pridruženej metódy sa kolekcia vráti getRooms () bude obsahovať najmenej jednu voľnú izbu. The existuje pokračuje typ Java prvku kolekcie - IRoom v príklade. r je premenná, ktorá odkazuje na akýkoľvek prvok v zbierke. The v za kľúčovým slovom nasleduje výraz, ktorý vráti kolekciu (Vymenovanie, Polealebo Zbierka). Za týmto výrazom nasleduje zvislá čiara a za ňou podmienka zahŕňajúca premennú prvku, r v príklade. Zamestnať existuje kvantifikátor, keď podmienka musí platiť aspoň pre jeden prvok v zbierke.

Oboje pre všetkých a existuje možno použiť na rôzne druhy zbierok Java. Podporujú Vymenovanies, Poles a Zbierkas.

Dôsledky: naznačuje

iContract poskytuje naznačuje operátor určiť obmedzenia formulára, "Ak platí A, potom musí platiť aj B." Hovoríme: „A znamená B.“ Príklad:

/ ** * @invariant getRooms (). isEmpty () znamená getEmployees (). isEmpty () // žiadne miestnosti, žiadni zamestnanci * / 

Tento invariant vyjadruje, že keď getRooms () zbierka je prázdna, getEmployees () zbierka musí byť tiež prázdna. Upozorňujeme, že nešpecifikuje, že keď getEmployees () je prázdny, getRooms () musí byť tiež prázdny.

Môžete tiež kombinovať práve zavedené logické operátory a vytvárať zložité tvrdenia. Príklad:

/ ** * @invariant všetci IEmployee e1 v getEmployees () | * všetci IEmployee e2 v getEmployees () | * (e1! = e2) znamená e1.getOffice ()! = e2.getOffice () // jedna kancelária na zamestnanca * / 

Obmedzenia, dedičstvo a rozhrania

iContract šíri obmedzenia pozdĺž vzťahov dedenia a implementácie rozhrania medzi triedami a rozhraniami.

Predpokladajme, že trieda B rozširuje triedu A. Trieda A definuje množinu invariantov, predbežných podmienok a postconditions. V tom prípade invarianty a predpoklady vyučovania A aplikovať do triedy B a metódy na hodine B musí vyhovovať rovnakým podmienkam ako táto trieda A uspokojuje. Do triedy môžete pridať prísnejšie tvrdenia B.

Vyššie uvedený mechanizmus funguje aj pre rozhrania a implementácie. Predpokladajme A a B sú rozhrania a trieda C. realizuje oboje. V tom prípade, C. podlieha invariantom, predbežným podmienkam a následným podmienkam oboch rozhraní, A a B, ako aj tých, ktoré sú definované priamo v triede C..

Pozor na vedľajšie účinky!

iContract zlepší kvalitu vášho softvéru tým, že vám umožní včas zachytiť veľa možných chýb. Môžete si však tiež zastreliť nohu (to znamená zaviesť nové chyby) pomocou aplikácie iContract. To sa môže stať, keď vo svojich tvrdeniach iContract vyvoláte funkcie, ktoré vyvolávajú vedľajšie účinky, ktoré menia stav vášho systému. To vedie k nepredvídateľnému správaniu, pretože systém sa bude správať inak, keď skompilujete svoj kód bez prístrojovej techniky iContract.

Príklad zásobníka

Pozrime sa na úplný príklad. Definoval som Stoh rozhranie, ktoré definuje známe operácie mojej obľúbenej dátovej štruktúry:

/ ** * @inv! isEmpty () znamená top ()! = null // nie sú povolené žiadne objekty null * / verejné rozhranie Stack {/ ** * @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 jednoduchú implementáciu rozhrania:

import java.util. *; / ** * @inv isEmpty () implikuje elements.size () == 0 * / public class 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; } verejný objekt top () {návrat elements.getLast (); } public boolean isEmpty () {return elements.size () == 0; }} 

Ako vidíte, Stoh implementácia neobsahuje žiadne tvrdenia iContractu. Všetky tvrdenia sa skôr robia v rozhraní, čo znamená, že zmluva o komponentoch v zásobníku je definovaná v rozhraní ako celok. Už len pri pohľade na Stoh rozhranie a jeho tvrdenia, Stohsprávanie je úplne špecifikované.

Teraz pridáme malý testovací program, aby sme videli iContract v akcii:

public class StackTest {public static void main (String [] args) {final Stack s = new StackImpl (); s.push („jeden“); s.pop (); s.push ("dva"); s.push ("tri"); s.pop (); s.pop (); s.pop (); // spôsobí zlyhanie tvrdenia}} 

Ďalej spustíme program iContract, aby sme vytvorili príklad zásobníka:

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 

Vyššie uvedené vyhlásenie si vyžaduje trochu vysvetlenia.

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