Esiste un modo per dimostrare le proprietà dei miei programmi C++?

Question

Capisco come lingue come Coq e Idris possano essere utilizzate per dimostrare le proprietà dei programmi scritti in quelle lingue (a giudicare dalla mia piccola esperienza in materia), ma mi chiedo se c'è un modo accessibile per fare lo stesso esternamente, su un base di codice già esistente.

C'è un modo per utilizzare uno strumento come Coq, o qualche altro strumento specializzato, per dimostrare la correttezza sugli algoritmi scritti in C++? Se sì, quali sono i requisiti per farlo?

Answer 1

Dipende da cosa intendi per "provare una proprietà". Per quanto ne so, ci sono molti strumenti di analisi statica per il controllo delle proprietà semplici dei programmi C, e variano molto in termini di espressività, facilità d'uso, solidità dell'analisi, ecc. Sono tipicamente usati per verificare che i programmi siano gratuiti degli errori di runtime, ma non sono molto utili per il controllo delle specifiche funzionali complete. Per questo tipo di proprietà, potrebbe essere necessario ricorrere a un rilevatore più potente che richiede di annotare manualmente una prova, invece di averne una controllata automaticamente.

Dato che si parla di Coq, vorrei fare riferimento a due strumenti basati su Coq per verificare i programmi C (tuttavia non funzionano con C++): in quest'ultima categoria, c'è lo Verified Software Toolchain, una logica per ragionamento sui programmi C che è incorporato all'interno di Coq. Puoi usarlo per scrivere prove sul comportamento del tuo programma e fare in modo che Coq li controlli, mostrando anche che un programma soddisfa le sue specifiche funzionali. Nella prima categoria, c'è lo Verasco, uno strumento automatico di analisi statica che ispeziona il tuo programma per l'assenza di errori di run-time. Una buona caratteristica di questi strumenti è che sono essi stessi programmi verificati, il che implica che si può avere un ulteriore grado di fiducia nelle analisi che forniscono.

Altri strumenti interessanti includono Frama-C, come menzionato nel commento sopra, e VCC, un analizzatore statico di Microsoft. Tuttavia, non funzionano con C++.