Logica di Hoare
# 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\}$

Il sistema per verificare le triple utilizza assiomi, ossia triple che risultano sempre soddisfatte, e regole di inferenza che permettono di semplificare il comando per induzione strutturale.

## Assiomi e regole di inferenza

### Assioma dell'istruzione vuota

È il caso base molto semplice ma utile per capire il ragionamento da fare con le triple di Hoare:

    $\{P\}\ {\textbf {skip}}\ \{P\}$

La correttezza è ovvia dato che si parte da uno stato iniziale, pre condizione P, il comando non effettua nessuna modifica e quindi si arriva nello stato finale, post condizione, P.

### 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 una verità posteriore.

### Regola per la sequenza di comandi

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.

### Regola dell'iterazione

Il comando iterativo viene eseguito se e solo se il valore dell'espressione E è valido. Nel momento in cui viene eseguito il comando C, non si sa a priori quanti cicli saranno necessari affinché il valore dell'espressione non sia più soddisfatto. Così è necessario che ci sia un'asserzione, l'invariante, che sia vera indipendentemente dal numero di cicli. Inoltre, prima dell'esecuzione del comando iterativo bisogna verificare che l'espressione E sia ben definita (deve dar luogo a un valore, numero o booleano). L'iterazione terminerà nel momento in cui il valore dell'espressione E è falso. Dunque avremo una tripla del tipo

    $\{Inv\land E\}\ {\textbf {while}}\ E\ {\textbf {do}}\ C\ {\textbf {done}}\ \{Inv\land \sim E\}$

Per quanto riguarda il comando C, prima che venga eseguito, è necessario verificare che valga sia l'invariante che l'espressione E. Dopo l'esecuzione del comando, invece, nella post condizione bisogna garantire che oltre a valere l'invarianza l'espressione E sia ben definita (ipotesi di invarianza):

    $\{Inv\land E\}\ C\ \{Inv\land def(E)\}$

Oltre all'ipotesi di invarianza, il comando iterativo comprende altre due ipotesi da verificare prima di poter affermare che una tripla con comando iterativo sia corretta: l'ipotesi di terminazione e l'ipotesi di progresso.

L'ipotesi di terminazione serve a garantire la terminazione di una tripla:

    $Inv\Rightarrow t\geq 0$

dove t è una funzione di terminazione che serve a garantire l'iterazione finché l'espressione E è soddisfatta.

Nell'ipotesi di progresso prima dell'esecuzione del comando C viene verificato che valgano l'invarianza, l'espressione E che t=V, dove V è detta variabile di specifica. Dopo l'esecuzione del comando vengono confrontati il valore della funzione di terminazione con quello della variabile di specifica V.

    $\{Inv\land E\land t=V\}\ C\ \{t<V\}$
