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ú:
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:
Podobným spôsobom je možné nahliadnuť na funkciu v triede v objektovo-orientovanom programovaní:
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:
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:
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ú:
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" &gt;= 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" &gt; 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" &gt; 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á.