|
|
Una volta scritto un programma, ma anche solo un suo pezzo, un modulo, una procedura, una funzione o semplicemente una sequenza di istruzioni, si pone il problema di stabilire se esso sia corretto. Ciò che stabilisce quale deve essere il comportamento di un pezzo di codice è la sua specifica. Dire che un pezzo di codice, che per semplicità possiamo supporre che calcoli una funzione f, è corretto rispetto alla specifica S, significa che f, (la funzione calcolata), soddisfa la specifica S. Esistono essenzialmente due soli modi per sostenere l' affermazione che f sia corretta:
verifica (formale)
verificare in modo formale, come se fosse la tesi di un teorema, che la funzione
f soddisfa la specifica S. Dimostrando cioè che f restituisce il risultato corretto
per ogni possibile ingresso;
validazione (empirica)
eseguendo una serie di prove e verificando che f restituisca il risultato
desiderato in ciascuna delle prove effettuate, in modo che sia ragionevole
aspettarsi che f restituisca il risultato desiderato anche in tutti gli altri casi.
E' evidente che la verifica è "meglio" della validazione, poiché la verifica ha una valore assoluto (se la dimostrazione è corretta), mentre la validazione ha un valore solo statistico. Tuttavia è estremamente difficile ed oneroso verificare programmi di una certa complessità. La verifica è quindi un' opzione che viene intrapresa solo quando ne esistono i presupposti economici: questo può essere il caso, per esempio, nei programmi ad alta criticità di missione, come sistemi di controllo di sonde spaziali o sistemi di sicurezza da cui dipende la vita di persone. In tutti gli altri casi di solito ci si accontenta di una validazione, magari molto approfondita. E' bene sottolineare, tuttavia, che la validazione è in grado soltanto di rivelare la presenza di un errore; non è mai in grado di garantirne l'assenza!
Per dimostrare la correttezza del codice, ovvero dimostrare
che il programma soddisfa le specifiche
formali date, bisogna dimostrare due cose:
che il programma termina per ogni ingresso x 
X (insieme degli ingressi) che soddisfa le precondizioni I(x);
la correttezza parziale del programma.
Per dimostrare la terminazione, bisogna trovare una funzione di terminazione
T : che assegna ad ogni stato M della computazione in un numero naturale N,
tale che per ogni esecuzione, se l'ingresso x soddisfa I(x), allora T(m0) >
T(m1) > …. >= 0, dove m0;m1; …..
M sono stati della computazione. La correttezza parziale di un programma corrisponde
alla semplice garanzia che, per ogni ingresso x e X che soddisfa I(x), il programma
o non termina o, se termina, produce un risultato y e Y che soddisfa le condizioni
di uscita U(x; y). Bisogna quindi trovare una proprietà P(x,m) sull'ingresso
e sullo stato della computazione, invariante rispetto allo stato. Questo
significa che ad ogni passo mi dell' esecuzione del programma, il
soddisfacimento di P(x;m) implica che, quando l' algoritmo
termina, il risultato è corretto. Spesso questa dimostrazione deve essere fatta
per induzione. Le proprietà
invarianti, oltre che nelle dimostrazioni di correttezza parziale, trovano un'
importante applicazione in una pratica comoda ed efficace di scrittura di codice.
Tale pratica consiste nell' utilizzo delle cosiddette asserzioni. Un'
asserzione è un costrutto condizionale che controlla una proprietà invariante
e, nel caso in cui questa non sia verificata, produce intenzionalmente un errore
di esecuzione che ha l' effetto di abortire l' esecuzione del programma. In
C un' asserzione potrebbe assumere la forma:
Il concetto di asserzione è talmente utile che quasi tutti i linguaggi di programmazione forniscono un costrutto sintattico apposito per inserirne una in qualsiasi punto del codice. Le asserzioni possono essere considerate, oltre che come uno strumento per garantire la correttezza parziale del codice, anche come strumenti di specifica e di documentazione, che fanno parte quindi della documentazione interna di un programma.
Quando si valida un programma, lo spirito del gioco non è dimostrare che il programma funziona, ma che non funziona. In altre parole, non si cercano casi di prova che si sa che il programma può superare, ma si tenta di costruire casi di prova capaci di trarre il programma in errore. E' quindi importante scegliere un buon insieme di dati di ingresso. Alcuni principi che dovrebbero ispirare la compilazione di un insieme di casi prova sono i seguenti:
esercitare tutto il codice: i casi di prova dovrebbero essere scelti in modo tale da far passare l'esecuzione del programma attraverso tutti i rami del suo diagramma di flusso;
provare alcuni casi tipici: solo perché rappresentano le situazioni che il progettista e il programmatore avevano in mente quando hanno realizzato il programma;
provare tutti i casi atipici: i casi insidiosi per la logica di un programma sono proprio quelli che il progettista e il programmatore non avevano in mente quando hanno realizzato il programma;
provare tutti i casi limite: sono quelli che mettono alla prova la robustezza del codice e che possono evidenziare alcune falle.
Per quanto un programma sia stato completamente validato durante il suo sviluppo, ogni modifica apportata durante la sua manutenzione richiede che le parti modificate vengano collaudate di nuovo. Questo processo, necessario ma molto costoso, è chiamato comunemente test di regressione. Lo scopo del test di regressione è controllare che le modifiche non abbiano introdotto nuovi errori in un codice già validato. L' opzione più semplice, che consiste nel rifare tutte le prove di validazione, non è economicamente molto efficiente, ragione per cui normalmente si preferisce condurre un collaudo selettivo. Sono stati proposti molti approcci selettivi al test di regressione, che possono essere classificati in tre categorie:
approcci di minimizzazione, che identificando un insieme minimale di prove che devono essere effettuate; per esempio, un approccio siffatto potrebbe selezionare una sola prova per ciascun blocco di codice modificato;
approcci di copertura, che invece di minimizzare il numero di prove, cercano di selezionare tutte le prove che esercitano il codice modificato;
approcci sicuri, che cercano di selezionare ogni prova che potrebbe far si che il programma modificato produca un risultato diverso dall' originale.
Tutto quanto riportato in questa pagina è a puro scopo informativo personale. Se non ti trovi in accordo con quanto riportato nella pagina, vuoi fare delle precisazioni, vuoi fare delle aggiunte o hai delle proposte e dei consigli da dare, puoi farlo mandando un email. Ogni indicazione è fondamentale per la continua crescita del sito.