Design by contract

Design by contract (DBC/DbC) alebo programming by contract (doslova približne „kontraktové programovanie“), je dizajnová metodológia pre vývoj počítačového softvéru. Vývojárom ukladá za povinnosť špecifikovať jasné rozhrania systémových komponentov na základe teórie abstraktných údajových typov a konceptuálnej metafory, ktorá vychádza z definície obchodného kontraktu – dohody.

„Design by Contract“ je obchodnou značkou Eiffel Software (časť Interactive Software Engineering Inc. resp. ISE), dizajnérov programovacieho jazyka Eiffel.

História

Pojem bol vytvorený Bernardom Meyerom v spojení s dizajnom programovacieho jazyka Eiffel a po prvýkrát bol popísaný v roku 1986 v článku , ďalej v a v dvoch edíciách jeho knihy Object-Oriented Software Construction.

Táto metodológia má svoje korene v prácach o formálnej verifikácii, formálnych špecifikáciách a Hoarovej logike. Základnými stavebnými prvkami sú:

• jasná metafora (pohľad), ktorý riadi proces dizajnu komponentu;
• zameranie na dedičnosť, hlavne vo vzťahu k metodológii pre redefiníciu a dynamické priradzovanie;
• využitie spracovania výnimiek;
• spojenie s automatickým vytváraním dokumentácie.

Opis

Základnou ideou DBC je pohľad na to, ako medzi sebou spolupracujú jednotlivé elementy softvérového systému. Na základe analýzy tohto chovania je možné izolovať vzájomné záväzky a výhody. Tento pohľad prichádza z obchodného sveta, kde sa „odberateľ“ a „dodávateľ“ dohodnú na „kontrakte“, ktorá sa definuje napr. ako:

• dodávateľ má poskytnúť určitý produkt (teda má záväzok) a má nárok na výhodu – platbu od odberateľa;
• odberateľ má záväzok (musí zaplatiť poplatok za produkt) a má nárok na výhodu – produkt dodávateľa;
• obidve strany musia splniť aj ďalšie záväzky (v tomto prípade napríklad zákonné požiadavky na obchod), ktoré sa vzťahujú ku všetkých kontraktom určitého druhu (iné požiadavky musí spĺňať vnútroštátny obchod, iné medzinárodný atď).

Podobným spôsobom je možné nahliadnuť na funkciu v triede v objektovo-orientovanom programovaní:

• úlohou funkcie je poskytnúť nejakú funkcionalitu (záväzok funkcie) a má nárok na zmysluplné vstupné parametre (záväzok voči funkcii). V DbC je tento záväzok označovaný ako prepodmienka (precondition);
• funkcia pre tieto dáta garantuje zmysluplný výsledok (výhoda pre volajúceho); v DbC je tento záväzok označovaný ako postpodmienka (postcondition);
• ďalšie záväzky sú určené rámcom „zmluvy“ – triedou, v ktorej sa metóda nachádza; v DbC sú tieto záväzky označované ako invarianty (invariants); tieto záväzky musia byť splnené pred a po vykonaní kontraktu – volaní metódy.

Kontrakt je formalizácia týchto výhod a záväzkov. DbC je možné sumarizovať troma otázkami, ktoré si musí neustále klásť dizajnér komponentu:

• Čo očakáva?
• Čo garantuje?
• Aký stav udržiava?

Veľa programovacích jazykov má podporu pre podobné podmienky – asercie. Novátorský prístup DbC sa prejavuje v tom, že uznáva tieto kontrakty za natoľko dôležité pre vývoj správneho softvéru, že by mali byť zahrnuté do procesu dizajnu.

Zápis kontraktu sa pripája na úrovni funkcie – kontrakt pre každú funkciu potom bude obsahovať nasledovné informácie:

• prípustné a neprípustné vstupné hodnoty a ich význam,
• prípustné a neprípustné návratové hodnoty a ich význam,
• chybové hodnoty a výnimky, ktoré sa môžu vyskytnúť a ich význam,
• bočné efekty,
• prepodmienky,
• postpodmienky,
• invarianty.

Pri použití metodológie DbC sa programový kód nikdy nesmie pokúšať o validáciu podmienok kontraktu – celá myšlienka stojí na formalizácii a zápise týchto podmienok tak, aby kód mohol okamžite spadnúť a ukázať na porušenie podmienok kontaktu. Táto myšlienka veľmi napomáha ladeniu, pretože model chovania pre každú metódu je jasne špecifikovaný.

Kontraktové podmienky by nemali byť nikdy porušené počas behu programu – z tohto dôvodu je možné ich zahrnúť len do kódu určeného pre ladenie a vo finálnej verzii vypustiť pre zlepšenie výkonu.

Príklad

Predstavme si, že navrhujeme triedu, ktorá bude implementovať jednoduchý LIFO zásobník. Základnými metódami zásobníka sú:

• Push (vložiť položku),
• Pop (vybrať položku),
• Peek (získať položku na vrchole zásobníka),
• Count (získať počet položiek v zásobníku),
• IsEmpty (získať príznak, či je zásobník prázdny).

Rámcom kontraktov pre zásobník bude trieda, ktorá tento zásobník implementuje – Stack:

 class Stack'
    method void Push(object newObject);
    method object Pop();
    method object Peek();
    method int Count();
    method boolean IsEmpty();

Začnime invariantmi. Zjavným invariantom bude, že počet položiek bude stále väčší alebo rovný 0:

 @invariant Count >= 0'
 class Stack

Metódy Count a IsEmpty nemajú žiadne prepodmienky. Invariant zároveň plní úlohu zjavnej postpodmienky metódy Count, postpodmienkou metódy IsEmpty je, že výsledná hodnota (result) by mala byť true, ak je Count == 0, inak false:

 @postcondition 'result == (Count == 0)'
 method boolean IsEmpty();

Pre metódu Push definujme prepodmienku že vkladaný objekt nesmie byť null. Postpodmienkou bude, že počet položiek v zásobníku sa má zvýšiť o 1 (metóda old() vracia stav pôvodného objektu):

 @precondition 'newObject != null'  
 @postcondition Count = old().Count   1'  
 method void Push(object newObject);

Metóda Peek. Prepodmienka je, že v zásobník nesmie byť prázdny, a vzhľadom na to, že nie je možné vložiť objekt null, definujeme aj rovnakú postpodmienku:

 @precondition Count > 0'  
 @postcondition 'result != null'
 method object Peek();

Prejdime k metóde Pop. Kontrakt je rovnaký ako v prípade metódy Peek, ďalšou postpodmienkou je, že počet položiek v zásobníku sa má znížiť o 1 (metóda old() vracia stav pôvodného objektu):

 @precondition Count > 0'
 @postcondition 'result != null'
 @postcondition ' Count = old().Count - 1'
 method object Pop();

Takýmto spôsobom vieme formalizovať chovanie triedy bez toho, aby sme museli napísať čo i len riadok kódu. Ďalšou výhodou je to, že odpadá testovanie na zjavné chybové stavy – správna reakcia na ne je zaručená.