Prima di iniziare, penso che valga la pena menzionare Philip Wadler "Propositions as Types ", che offre un'eccellente panoramica della storia antica della teoria della computabilità con un'enfasi sulla logica del primo ordine. Di questo c'è anche una presentazione video . Consiglio vivamente chiunque sia interessato a questo argomento, guarda il video e leggi il giornale.
Alan Turing reduced his Halting problem to this problem, by saying in his paper: "Corresponding to each computing machine 'it' we construct a formula 'Un(it)' and we show that, if there is a general method for determining whether 'Un(it)' is provable, then there is a general method for determining whether 'it' ever prints 0"
Sì, se Entscheidungsproblem è computabile allora il problema di interruzione è computabile. Il problema dell'arresto è stato provato come non classificabile, pertanto il problema di Entscheidungsproblem è inaccessibile. In altre parole, un algoritmo generale per dimostrare se qualsiasi programma arbitrario è corretto o meno non esiste. Tuttavia, ciò non significa che non esistono algoritmi per provare se alcuni programmi sono corretti o meno.
So, it implies, that a working program(algorithm) as a proof of a solution to a problem, makes the problem say computable.
Se con "lavoro" intendi "corretto" (inclusa la condizione di interruzione), allora sì, possiamo dire che un algoritmo provabilmente corretto che risolve un problema è la prova che il problema è computabile. Tuttavia, come sai che un programma è corretto? Sappiamo che non può esserci un algoritmo generale per dimostrarne la correttezza. Questo ci lascia due opzioni:
- Possiamo (provare a) fare la prova da soli. Tuttavia, l'inconoscibilità del problema Entscheidungs implica che alcune cose non sono dimostrabili. Se ci imbattiamo in uno di questi problemi, le prove formali sono un vicolo cieco. Inoltre, non c'è modo (in generale) di sapere anche se stiamo cercando di dimostrare qualcosa che è indimostrabile. Quindi potremmo spendere qualsiasi quantità di risorse verso un problema che non risolveremo mai.
- Possiamo (provare a) esprimere il programma (e il problema) come sottoinsieme dei problemi per i quali abbiamo un algoritmo per fare automaticamente la prova. Nota, tuttavia, che dobbiamo dimostrare che prover è corretto. Quindi, alla fine, qualcuno deve fare una prova a mano ad un certo punto.
Anche se teoricamente possibile, entrambe le opzioni richiedono molto tempo. Se non siamo in grado (o non vogliamo) di fare una di queste cose, il vero test è tutto ciò che ci rimane. Verificando che i risultati corretti siano prodotti almeno per alcuni dei possibili input, approssimiamo in una certa misura una prova completa.
Inoltre, ci sono molti aspetti pratici che le prove formali di correttezza non affrontano. Alcuni di loro sono:
- Prestazioni di tempo e spazio. Non ci fa bene se il nostro programma provabilmente corretto non calcola un risultato prima della morte termica dell'universo. O se fallisce a causa di un sovraccarico dello stack. O se esaurisce la memoria principale o qualche altra risorsa. Per essere pratici, avremmo bisogno di provare anche queste proprietà. La correttezza teorica di per sé non è sufficiente.
- Abbiamo espresso correttamente il problema nel sistema di correzione automatica? Ad esempio, stiamo effettivamente risolvendo il problema che pensiamo stiamo risolvendo.
- Stiamo risolvendo il problema giusto ? Un programma probabilmente corretto è inutile se risolve il problema sbagliato.
- Ogni volta che cambiano i requisiti, il problema cambia. Quindi ogni cambiamento richiede una riformulazione del problema e una nuova dimostrazione di correttezza.
Penso che questo sia il motivo per cui c'è stata relativamente poca spinta nel settore verso prove formali. Tuttavia, ciò non significa che non usiamo mai le prove. Ad esempio, il controllo di tipo statico viene utilizzato per dimostrare che un programma è ben tipizzato. Questo può eliminare una certa classe di errori, ma non può di per sé escludere tutti gli errori.
In alcuni casi, è possibile provare un programma corretto verificando che produce il risultato corretto per tutti i possibili input. In questi casi, il test stesso può effettivamente essere la prova della correttezza. La maggior parte delle volte, però, lo spazio di input è troppo grande (o addirittura infinito) perché una tale strategia sia pratica (o persino possibile). Quindi, in generale, è impossibile dimostrare un programma corretto tramite test.
Tuttavia, possiamo dimostrare che un programma è non corretto tramite test. Ciò accade osservando un fallimento in un test. Quindi l'utilità del testing si riduce ad avere "buoni" test che coprono proprietà "utili" e che hanno "molti di loro". Possiamo scrivere test a mano, ma non molti. Se disponiamo di proprietà ben definite che desideriamo testare, possiamo utilizzare strumenti come QuickCheck per generare automaticamente molti test per noi .
Quindi direi che design-by-contract, in generale, non sostituisce test, ma piuttosto complimenti .
