Logica di Hoare

Da Wikipedia, l'enciclopedia libera.

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[modifica | modifica wikitesto]

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[modifica | modifica wikitesto]

Assioma dell'Assegnamento[modifica | modifica wikitesto]

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[modifica | modifica wikitesto]

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[modifica | modifica wikitesto]

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[modifica | modifica wikitesto]