La progettazione per contratto si basa sulla logica di Hoare, in cui una dimostrazione di correttezza di un programma viene stabilita ragionando su condizioni pre / post e invarianti.
Quali sono i mezzi e i prerequisiti di una lingua che rende possibile tale ragionamento?
Può essere controllato staticamente o è solo una forma di asserzione di runtime?
Rispondendo alla tua prima domanda non sembra esserci alcun ostacolo a progettare o estendere una lingua per supportare DbC. Tuttavia, DbC introduce non solo asserzioni su un linguaggio, ma anche un insieme di regole che indicano come combinare queste asserzioni in presenza di (multiple) eredità e ridichiarazioni. Di conseguenza, le annotazioni semplici non possono essere facilmente tradotte in codice eseguibile a meno che gli strumenti linguistici non siano in grado di farlo.
Per quanto riguarda la seconda domanda, originariamente Design by Contract ™ è stata introdotta a Eiffel e in effetti era pensata per i controlli di runtime. Nel tempo ci sono stati dei cambiamenti e ne menzionerò solo alcuni:
Compilazione regolare. Per un certo periodo Eiffel si chiama così void-safety, cioè una garanzia che non c'è mai una chiamata su Void target (cioè eccezioni di tipo NullReferenceException sono impossibili). Questa tecnologia si basa su alcune regole. Al fine di rendere fattibile la programmazione void-safe e vicino ad un normale ragionamento del programmatore, implicano asserzioni in una certa forma. Ad esempio, i metodi che attivano le eccezioni hanno post-condizioni nel formato False per indicare che qualsiasi codice dopo le chiamate a tali metodi è irraggiungibile. Il compilatore sa poi che non c'è motivo di controllare le regole di sicurezza del vuoto dopo tali chiamate perché non verrà mai eseguito.
Generazione di test. Le precondizioni e le postcondizioni possono servire da buona base per generare automaticamente test, semplicemente osservando le specifiche. Questa tecnologia è un mix di approcci sia statici che dinamici, quando l'analisi statica prende parte alle asserzioni dei test di generazione di test e di esecuzione dei test in fase di esecuzione. Un esempio di tale strumento è AutoTest .
Verifica del codice. Alcuni strumenti di verifica per lingue diverse si basano su specifiche DbC per dimostrare la correttezza. Per Java è JML, per Eiffel - AutoProof. Nell'attuale pagina web di quest'ultimo è possibile trovare un collegamento a una versione online che fornisce alcuni esempi in cui può provare a capire cosa c'è di sbagliato nel codice di esempio e risolverlo. Sfrutta DbC e utilizza alcune classi di modelli per descrivere in modo rigoroso il comportamento dei contenitori sotto forma di pre e post-condizioni normali. L'analisi è completamente statica, cioè se lo strumento dice che tutte le asserzioni sono soddisfatte, non ci saranno violazioni di asserzione in fase di esecuzione e le asserzioni possono essere tranquillamente disattivate.
Leggi altre domande sui tag code-quality design-by-contract