Kapitola 1. Přednáška XXX - návrh podle kontraktu (specifikace) - Design by Contract.

Obsah

Design by Contract
Design by Contract - návrh podle kontraktu
DBC - jak dosáhnout

Design by Contract

Design by Contract - návrh podle kontraktu

Nejde o nic jiného, než o zajištění, aby výsledný navržený program splňoval specifikaci, tj.:

  • aby pro každý atomický, zvenčí viditelný/volatelný kus kódu (typicky metoda) byly specifikovány vstupní a výstupní podmínky

  • a aby jejich platnost byla za běhu zaručena

  • mezi zadavatelem (tj. analytikem, příp. zákazníkem) a návrhářem tak vzniká

  • dohoda (contract), že specifikace bude dodržena

DBC - jak dosáhnout

K dosažení tohoto ideálního stavu vede budto čistě formální cesta:

  • specifikace zmíněných podmínek matematickými prostředky a

  • formální dokazování korektnosti

Dále zmiňované nástroje však toto nedokážou; omezují se na běhovou kontrolu platnosti předpsaných podmínek