title: Logica di Hoare
text: # 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\}$
  