Logica di Hoare

La Logica di Hoare è un sistema formale che rientra tra le semantiche assiomatiche pubblicato per la prima volta nel 1969 da C. A. R. Hoare che si prefigge, definendo un insieme iniziale di assiomi e di regole su di essi, di valutare la correttezza di programmi utilizzando il rigore dei formalismi matematici.

La logica è stata sviluppata per essere utilizzata con un semplice linguaggio di programmazione imperativo ed ha subito sviluppi ulteriori per merito dello stesso Hoare e di altri ricercatori per la gestione di casistiche particolari quali la concorrenza, i puntatori e le procedure.

Tripla di Hoare

L'intero sistema si basa sul concetto di tripla di Hoare. Questa tripla definisce come l'esecuzione di un comando modifichi la verità in merito al programma, ed è definita come

$\{P\}\;C\;\{Q\}$

In cui P e Q vengono chiamate asserzioni e C è un comando. Nel caso specifico P viene definita precondizione e Q postcondizione.

Nel suo documento originale Hoare definisce il significato della tripla come:

« Se l'asserzione P è vera prima dell'esecuzione di un comando o di una serie di comandi C, allora Q è vera dopo l'esecuzione. »

(C. A. R. Hoare, An Axiomatic Basis for Computer-Programming)

Nel caso in cui non vi siano precondizioni da rispettare scriviamo semplicemente

$true\;C\;\{Q\}$

Regole

Assioma dell'Assegnamento

Il caso più caratteristico di operazione in un linguaggio di programmazione è chiaramente l'assegnamento, abbiamo quindi la seguente situazione:

$\{P\}\;\{x := f\}\;\{Q\}$

dove x è una variabile e f è un'espressione senza effetti collaterali che però può contenere x.

L'esecuzione del comando non può implicare niente per quanto riguarda le precondizioni ma ogni postcondizione del programma che riguarda x ed è vera dopo l'esecuzione, dovrà essere vera per f prima dell'esecuzione dato che il comando sostituisce al valore di x quello valutato dall'espressione f.

Formalmente abbiamo:

$\vdash P_0\;\{x := f\}P$

in cui x è la variabile, f l'espressione e $P_0$ è ottenuto da P sostituendo ad ogni occorrenza di x l'espressione f.

Usando la rappresentazione con il relabeling possiamo anche esprimere l'assioma con la sua classica notazione:

$\frac{}{\{P[E/x]\}\ x:=E \ \{P\} }$

Si noti che l'assioma è in realtà una classe di assiomi che rispettano un determinato schema.

Regola della Conseguenza

La regola della conseguenza permette di dedurre ulteriori verità partendo da altre già specificate. Supponiamo che un frammento di programma Q abbia come postcondizione R: naturalmente dopo l'esecuzione del frammento sarà vero anche tutto ciò che è implicato da R. Viceversa supponiamo che un frammento Q abbia come precondizione P: in questo caso possiamo affermare con certezza che prima dell'esecuzione di Q sarà vero anche tutto ciò che implica P.

Formalmente possiamo scrivere la regola di inferenza come:

$\frac { P^\prime \rightarrow\ P\ ,\ \lbrace P \rbrace\ Q\ \lbrace R \rbrace\ ,\ R \rightarrow\ R^\prime } { \lbrace P^\prime\ \rbrace\ Q\ \lbrace R^\prime\rbrace }$

Il concetto espresso da questa regola viene detto weakest-precondition o strongest-postcondition per il fatto che possiamo effettivamente generalizzare nel caso di una verità precedente al frammento e specializzare nel caso di un verità posteriore.

Regola della Composizione

Generalmente, in un linguaggio di programmazione, abbiamo un operatore utilizzato per esprimere la concatenazione tra più istruzioni. Scegliamo il punto e virgola e supponiamo due istruzioni in sequenza $<C_1; C_2>$.

La regola afferma che:

$\frac {\{P\}\ C_1\ \{P'\}\ , \ \{P'\}\ C_2\ \{P''\} } {\{P\}\ <C_1;C_2>\ \{P''\}}$

Possiamo così valutare la verità di una sequenza di istruzioni cercando predicati veri tra una e l'altra e quindi comporre via via le proprietà che stiamo cercando per un frammento composto da più operazioni da eseguire. Abbiamo che se vale $P$ prima di $C_1$ e vale $P''$ dopo $C_2$ se troviamo $P'$ che sia vero dopo $C_1$ e prima di $C_2$ possiamo dedurre le condizioni della sequenza intera.

Si noti che in questo caso abbiamo usato il punto e virgola e le parentesi angolate per definire la sequenza di più operazioni ma il ragionamente è ovviamente applicabile a qualsiasi operatore.