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 HoareModifica

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

 

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

 

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 inferenzaModifica

Assioma dell'istruzione vuotaModifica

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

 

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'assegnamentoModifica

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

 

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:

 

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

 

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

Regola della conseguenzaModifica

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:

 

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 comandiModifica

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  .

La regola afferma che:

 

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   prima di   e vale   dopo   se troviamo   che sia vero dopo   e prima di   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'iterazioneModifica

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

 

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):

 

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:

 

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.

 

BibliografiaModifica

Controllo di autoritàGND (DE4343105-7