Logica di Hoare: Nozioni Preliminari

La Logica di Hoare e' un sistema formale che si puo' utilizzare per fornire la semantica di linguaggi di programmazione imperativi.
La semantica dei linguaggi di programmazioni fornita con sistemi come la Logica di Hoare viene chiamata semantica assiomatica.
La Logica di Hoare, come le semantiche operazionali, e' utilizzabile anche come strumento per dimostrare proprieta' di programmi.

I giudizi della Logica di Hoare sono della forma

{P} C {Q}

dove

• C e' un programma (o una singola istruzione)

• P e Q sono asserzioni

Le asserzioni non sono altro che formule ben formate della logica dei predicati, le cui variabili libere sono variabili utilizzate nel programma (ed eventualmente anche le locazioni di memoria), o nell'istruzione.

In un giudizio {P} C {Q}, l'asserzione {P} viene detta pre-condizione, mentre l'asserzione {Q} viene detta post-condizione. :


Prima di introdurre cosa sono i giudizi validi, introduciamo il concetto di stato (della computazione).
Un programma imperativo calcola eseguendo istruzioni in sequenza. Ogni istruzione modifica le variabili del programma o le locazioni di memoria. Lo stato, ad un certo istante, rappresenta il contenuto che in tale istante hanno le variabili del programma e le locazioni di memoria (nel caso del linguaggetto WHILE si considerano solo le variabile del programma).
Lo stato puo' essere quindi visto come una funzione σ che associa valori (del tipo di quelli manipolati dai programmi del linguaggio) ad identificatori (di variabili), cioe', nel caso del linguaggio WHILE che manipola numeri interi,

Notare come uno stato non sia altro che un ambiente (nel senso della Definizione 4.6 del testo [SM]) per la struttura corrispondente, nel caso del linguaggio WHILE, ai numeri interi.

Una asserzione P e' soddisfatta da uno stato σ, che indichiamo con

se l'asserzione P (che, ricordiamo, e' una formula ben formata della logica dei predicati) e' soddisfatta nella struttura dei numeri interi (nel caso del nostro linguaggio WHILE) rispetto all'ambiente corrispondente a σ (cioe', in notazione logica, [[P]]^Z_σ = 1).
Per esempio, se prendiamo uno stato σ' che associa il valore 3 alla variabile X1 ed il valore 2 alla variabile X2, e facile controllare che l'asserzione (X1 > 0 ∧ X2>0 ∧ Pari(X2)) e'soddisfatta dall'ambiente σ', cioe' σ' |= (X1 > 0 ∧ X2 > 0 ∧ Pari(X2)).
Un programma, o anche una singola istruzione, se eseguito partendo da una situazione delle proprie variabili (e della memoria) descritta da uno stato σ, durante la sua esecuzione modifichera' lo stato. Indichiamo con φ_C(σ) lo stato che si ottiene partendo dallo stato σ al termine dell'esecuzione del programma (o istruzione) C.

Un giudizio {P} C {Q} e' valido (che indichiamo con |= {P} C {Q} ) se per ogni stato σ

cioe', per ogni stato σ che soddisfa la pre-condizione ed a partire dal quale l'esecuzione di C termina, σ modificato dall'esecuzione di C soddisfa la post-condizione.
E' facile controllare informalmente come il seguente giudizio sia valido

Esempio di uso della regola (iterazione)

Una volta studiato il testo [US], vediamo un po' in dettaglio un esempio che in pratica e' la soluzione dell'esercizio 70 in [US].

Vediamo un esempio di come si possa utilizzare la regola

{A ∧ E} I {A}
----------------------------------
{A} while E do I end {A ∧ ¬E}

Regola all'apparenza strana, poiche', per cicli while, permette di asserire, al termine di un ciclo, praticamente solo formule che sono anche pre-condizioni.
In realta', asserzioni che valgono sia prima che dopo un ciclo e che valgono sia prima che dopo le istruzioni che formano il corpo del ciclo e che vengono dette invarianti possono fornire informazioni estremamente importanti sul comportamento di un programma.
Prendiamo in considerazione, come semplice esempio, il seguente frammento di codice:

q := 0;
r := a;
while r ≥ b do
q := q+1;
r := r - b
endw

Supponiamo di aver scritto questo frammento di codice (magari all'interno di un programma piu' grande) poiche' sappiamo che all'inizio dell'esecuzione di tale frammento il valore contenuto in a sara' maggiore o uguale a zero, mentre quello di b maggiore di zero, e perche' al termine vogliamo che la variabile q contenga il quoziente della divisione intera tra a e b, mentre dentro r vogliamo che ci sia il resto di tale divisione. A tale scopo infatti il nostro frammento di codice implementa l'algoritmo della divisione intera per sottrazioni successive.
Per essere pero' certi che il nostro frammento di codice esegua esattamente cio' che vogliamo, potremmo dimostrare, nella Logica di Hoare per il linguaggio WHILE che

dove con C indichiamo il nostro frammento di codice.
Notiamo come la post-condizione sia la formula del calcolo dei predicati che rappresenta esattamente il fatto che q ed r sono, rispettivamente, il quoziente ed il resto della divisione intera tra a e b.
Per dimostrare questo giudizio si puo' utilizzare la regola per il while della Logica di Hoare, facendo uso di una asserzione invariante.

Intanto e' facile dimostrare che

utilizzando l'assioma per gli assegnamenti e la regola per la sequenza di comandi (in realta' occorre anche utilizzare la regola che permette di rafforzare la precondizione).
Intuitivamente e' ovvio che se la pre-condizione e' vera la post-condizione lo e' dopo i due assegnamenti, visto che q diventa 0 e r e' posto uguale a b.
Dimostriamo ora che

dove C' e' l'istruzione while del nostro codice.
Vediamo come questo si possa fare utilizzando la regola (iterazione), usando come asserzione A la formula

e come condizione E ovviamente la formula r ≥ b.

{r≥0 ∧ b>0 ∧ (a= b*q + r) ∧ r≥b} I {r≥0 ∧ b>0 ∧ (a= b*q + r)}
---------------------------------------------------------------------
{r≥0 ∧ b>0 ∧ (a = b*q + r)} C' {r≥0 ∧ b>0 ∧ (a= b*q + r) ∧ ¬(r≥b)}

dove nel nostr caso I e' il frammento di codice q := q+1; r := r - b.
Notate come la formula

sia equivalente a

Questo significa che la regola (iterazione) ci permette di derivare

se siamo capaci di derivare

Questo ultimo giudizio si puo' dimostrare usando due volte la regola per l'assegnamento e la regola per la sequenza di istruzioni (farlo come esercizio!). A questo punto abbiamo quindi dimostrato che

e che

Usando ora la regola per la sequenza di istruzioni possiamo derivare cio' che ci eravamo prefissi, cioe'