Pogodba pri definicijskem modulu

Obicajno pogodba ni enolicna - z drugimi besedami, sestavimo lahko vec razlicnih pogodb z istim pomenom.

Pogodba se sestoji iz petih clenov:

1.

DESC - kratek opis delovanja programa (description);

2.

PARMS - pove nam parametre funkcije (parameters);

3.

RESULT - rezultat programa (result);

4.

PRE - predpogoj, ki pove, kako naj uporabnik dela (kaj mora zagotoviti pred klicem podprograma), da bo podprogram pravilno deloval (precondition);

5.

POST - popogoj, ki pove, kaksen pogoj je izpolnjen, ko se funkcija vrne nazaj (postcondition).

Prva clena sta opisna in sta namenjena predvsem razumevanju funkcije. Zadnji trije cleni bolj natancno dolocajo funkcijo. Mi jih bomo zapisali v tako imenovani pol-formalni obliki - zapis ni povsem formalen, ki bi sicer omogocal samodejno preverjanje pravilnosti delovanja programa.