Il test e l'analisi del software valutano le qualità e individuano difetti per migliorarlo. Si focalizzano principalmente sulla affidabilità. Non esistono tecniche perfette, ma una serie di trade-off tra loro con punti di forza e debolezza complementari. Integrare queste tecniche migliora la verifica del software, ma spesso vengono trattate come scelte indipendenti anziché complementari. Comprendere i trade-off e le tecniche permette di selezionare e combinare le opzioni per migliorare la convenienza economica della verifica.
Le tecniche di test e analisi del software sono fondamentali per valutare e migliorare l'affidabilità del sistema.
La validazione si occupa di confrontare il sistema con i requisiti reali, assicurando che soddisfi effettivamente le esigenze degli utenti, anche oltre ciò che è specificato. In altre parole, la validazione mira a verificare che il software sia utile e risponda alle esigenze reali degli utilizzatori, nonché a individuare eventuali discrepanze tra le esigenze effettive e quelle specificate.
D'altra parte, la verifica si concentra sulla coerenza tra l'implementazione del software e la specifica, garantendo che il sistema costruito rispetti ciò che è stato pianificato, evitando discrepanze tra i requisiti specificati e ciò che è stato effettivamente implementato.
Pur essendo attività complementari, la verifica e la validazione differiscono nei loro obiettivi e approcci: la verifica verifica la correttezza dell'implementazione rispetto alla specifica, mentre la validazione valuta se il software è utile e soddisfa le esigenze reali degli utenti. È importante notare che la validazione è spesso più soggettiva e coinvolge il giudizio umano, mentre la verifica può essere più oggettiva e basata su criteri specifici.
Dato una specifica precisa e un programma, sembra che si dovrebbe essere in grado di arrivare a un argomento logicamente valido o a una prova che un programma soddisfi le proprietà specificate. Tuttavia, non è sempre possibile produrre una "prova" logica completa per la specifica completa dei programmi pratici in dettaglio completo, a causa di una delle proprietà più fondamentali del calcolo.
Alan Turing dimostrò che alcuni problemi non possono essere risolti da nessun programma informatico. L'universalità dei computer induce paradossi logici riguardanti i programmi per analizzare altri programmi, incluso il problema dell'arresto. Quasi ogni proprietà interessante riguardante il comportamento dei programmi informatici può essere dimostrata come implicante il problema dell'arresto, il che rende impossibile la verifica accurata in tempo finito.
In teoria, l'indeterminatezza di una proprietà S implica semplicemente che per ogni tecnica di verifica per verificare S, c'è almeno un programma "patologico" per cui quella tecnica non può ottenere una risposta corretta in tempo finito. Tuttavia, in pratica, il fallimento della verifica è comune e si deve accettare un grado significativo di inesattezza.
Il testing del software è una tecnica di verifica ed è vulnerabile all'indeterminatezza tanto quanto altre tecniche. Il testing esaustivo, ovvero eseguire e controllare ogni possibile comportamento di un programma, sarebbe una "prova per casi", ma richiederebbe un tempo indefinito per completarsi.
Anche se si considera il fatto che i programmi vengono eseguiti su macchine reali con rappresentazioni finiti dei valori di memoria, il testing esaustivo richiederebbe comunque tempi esorbitanti. Ad esempio, un test per una semplice classe Java richiederebbe circa 30.000 anni per completarsi.
Il testing è una tecnica ottimistica perché non può garantire la correttezza in un tempo finito. Al contrario, molte tecniche di analisi statica sono pessimistiche rispetto alle proprietà che cercano di verificare. Esistono anche tecniche che possono dare come risultato "non so", che possono essere considerate ottimistiche o pessimistiche a seconda di come viene interpretato il risultato.
Una tecnica di verifica del software che erra solo nella direzione pessimistica è chiamata analisi conservativa. Tuttavia, l'uso di un'analisi conservativa può produrre un gran numero di falsi positivi insieme a pochi risultati accurati. Di solito, solo una scelta oculata di tecniche complementari ottimistiche e pessimistiche può produrre risultati accettabili.
In aggiunta all'inesattezza pessimistica e ottimistica, è possibile un terzo compromesso: sostituire una proprietà più facilmente verificabile o vincolare la classe di programmi che possono essere controllati. Ad esempio, possiamo verificare una proprietà S₀ che è una condizione sufficiente ma non necessaria per la proprietà S. Molte volte, la sostituzione di proprietà più semplici e verificabili è possibile anche nella progettazione di linguaggi di programmazione moderni.
La decisione critica di imporre un particolare protocollo di controllo della concorrenza non è una decisione postuma che può essere presa in una fase di testing alla fine dello sviluppo. Piuttosto, il piano per le attività di verifica, con un adeguato bilancio tra costo e sicurezza, fa parte del progetto di sistema.