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 *[[invariant]]y* (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á.

## Referencie

Kategória:Softvérové inžinierstvo