Design by contract: differenze tra le versioni

Contenuto cancellato Contenuto aggiunto
Riga 2:
 
==Descrizione==
L'idea centrale del DBDBC è che le entità software hanno degli obblighi nei confronti di altre entità in base a regole formalizzate fra di essi. Una [[specifica funzionale]], o 'contratto', viene creato per ogni modulo nel sistema prima che sia codificato. L'esecuzione del programma è quindi vista come l'interazione fra i vari moduli vincolati da questi contratti.
 
In generale, le routine hanno ''precondizioni'' esplicite che il chiamante deve soddisfare prima di chiamare la routine, e postcondizioni esplicite che descrivono le condizioni che la routine garantirà essere vere nel momento in cui la routine finisce. Così, un contratto assume la seguente forma generale: "Se tu, il chiamante, predisponi certe precondizioni, allora io stabilirò certi altri risultati quando ti avrò terminato. Se tu violi le precondizioni, allora non ti prometto niente." L'implementazione di ogni modulo può allora essere scritta assumendo la correttezza dei moduli che usa (i suoi subappaltatori), purché soddisfi le loro precondizioni.