Design by Contract non è comunemente fatto, quindi tali annotazioni sarebbero abbastanza rari. Questo non significa che non verrebbero utilizzati affatto! Invece, Design by Contract è più utile quando la correttezza è della massima importanza, ad es. per l'implementazione dell'algoritmo o sistemi critici per la sicurezza.
Ma la stragrande maggioranza dello sviluppo del software non è considerata di importanza critica per la sicurezza. I tuoi requisiti saranno più probabili "In qualità di analista aziendale, posso fare clic su un pulsante per salvare il rapporto come foglio di calcolo di Excel, in modo da poter eseguire la mia analisi". La verifica formale non aggiunge alcun valore in queste circostanze e sarebbe difficile esprimere contratti utili che possono essere verificati.
L'attuale best practice del settore consiste nell'utilizzare casi di test automatizzati per verificare che i requisiti siano soddisfatti e che i sistemi si comportino correttamente. I test soffrono di limitazioni sistematiche: i test sono solo esempi e non possono dimostrare la correttezza di tutti gli input, a meno che non provi tutti gli input. Test e metodi di verifica formale quindi non si sostituiscono, ma si completano a vicenda: idealmente, li fai entrambi.
L'unico sistema di verifica formale automatizzato comunemente usato è il sistema di tipo statico del tuo linguaggio di programmazione. La tipizzazione statica può essere utilizzata per esprimere alcuni semplici contratti, sebbene vi siano limitazioni evidenti, a seconda della lingua. Ma anche la tipizzazione statica non viene utilizzata universalmente: molti sviluppi significativi (anche per i sistemi sensibili alla sicurezza come le applicazioni web) avvengono in linguaggi dinamici come PHP, Python o Ruby, che generalmente non hanno alcun tipo di analisi statica incorporata.