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\}$

Bibliografia

• Mordechai Ben-Ari, Mathematical Logic for Computer Science, Londra, Springer, 1993, ISBN 978-1-4471-4128-0.
• Paolo Mancarella, Note di semantica assiomatica (PDF), p. 78. URL consultato il 6 febbraio 2016.

Controllo di autorità	GND (DE) 4343105-7