Diversi tipi di analisi statica
Come già detto, il problema di verificare una proprietà arbitraria per un programma è fondamentalmente indecidibile. Però, come per molti problemi indecidibili, è possibile comunque provare ad approssimare il problema, cercando di trovare soluzioni utili. In particolare le principali tecniche per approssimare sono le seguenti.
Interpretazione astratta
L'interpretazione astratta consiste nel fornire diverse astrazioni per un linguaggio di programmazione o di specifica. La semantica concreta rappresenta il comportamento in modo preciso del programma, descrivendo l'insieme delle tracce di esecuzione possibili. Queste però tipicamente portano a situazioni di non computabilità, quindi quello che viene fatto è derivare semantiche più astratte, come ad esempio l'insieme degli stati raggiungibili.
L'obiettivo dell'analisi statica è ottenere un'interpretazione semantica calcolabile, ad esempio rappresentando lo stato di un programma che manipola variabili intere solo tramite il loro segno (positivo o negativo). Questa astrazione può mantenere precisione per alcune operazioni, come la moltiplicazione, ma può perderla per altre, come la somma di numeri con segni opposti. Per questo si parla di sovra-approssimazione della semantica reale del programma. La perdita di precisione è talvolta necessaria per rendere la semantica decidibile, in quanto è necessario bilanciare accuratezza e costo computazionale. Le astrazioni utilizzate nella pratica sono adattate alle proprietà e ai programmi da analizzare, a seconda di cosa è interessante verificare.
Logica di Hoare
La logica di Hoare è un sistema formale che descrive un insieme di regole logiche per analizzare rigorosamente la correttezza di programmi. Si basa su una costruzione sintattica, detta tripla di Hoare, che è della forma
$$ \{P\}\quad C \quad \{Q\} $$
dove \(P\) è una formula detta precondizione, \(Q\) è una formula detta postcondizione, e \(C\) è un comando (si può pensare come un programma). L'idea è che la tripla è valida se per ogni stato iniziale che soddisfa la precondizione, allora l'esecuzione del programma parta a uno stato finale che soddisfa la postcondizione. Un esempio di tripla valida è il seguente.
$$ \{x \geq 0\}\quad x = x + 1 \quad \{x \geq 1\} $$
Assumendo che \(x\) sia un intero, ogni stato che soddisfa \(x \geq 0\), dopo l'incremento di \(x\) soddisferà anche \(x \geq 1\). La logica di Hoare definisce assiomi e regole che possono essere usate per dimostrare la correttezza di triple arbitrarie, notando che questa logica per garantire la correttezza rimane comunque indecidibile.
Model checking
Nel model checking vengono considerati sistemi con un numero di stati finito (tipicamente rappresentati come sistemi di transizione), oppure che possono essere rappresentati con un numero di stati finito grazie a un apposita astrazione. Vengono poi applicate delle metodologie formali per dimostrare proprietà riguardo questo sistema. Queste proprietà nella pratica si trasformano in formule logiche, che possono essere risolte tramite alcuni risolutori SAT o SMT. Vedremo nel prossimo capitolo più nel dettaglio questa tecnica.