Logica di Hoare

Questa voce o sezione sull'argomento matematica non cita le fonti necessarie o quelle presenti sono insufficienti.

---

Puoi migliorare questa voce aggiungendo citazioni da fonti attendibili secondo le linee guida sull'uso delle fonti. Segui i suggerimenti del progetto di riferimento.

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.

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

${\displaystyle \{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:

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

${\displaystyle \{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.

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

${\displaystyle \{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.

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

${\displaystyle \{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:

${\displaystyle \vdash P_{0}\;\{x:=f\}P}$

in cui x è la variabile, f l'espressione e ${\displaystyle 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:

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

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

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:

${\displaystyle {\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.

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 ${\displaystyle <C_{1};C_{2}>}$.

La regola afferma che:

${\displaystyle {\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 ${\displaystyle P}$ prima di ${\displaystyle C_{1}}$ e vale ${\displaystyle P''}$ dopo ${\displaystyle C_{2}}$ se troviamo ${\displaystyle P'}$ che sia vero dopo ${\displaystyle C_{1}}$ e prima di ${\displaystyle 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.

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

${\displaystyle \{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):

${\displaystyle \{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:

${\displaystyle 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.

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

• 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.

Portale Informatica

Portale Matematica