Definiamo il linguaggio di programmazione imperativo semplificato che andremo ad utilizzare. Si userà una grammatica formale.
L’elemento fondamentale di questo linguaggio è il comando, che indica o una singola istruzione o un gruppo di istruzioni strutturate. Il simbolo usato nella grammatica per indicare un comando è $C$.
Un comando viene costruito tramite le produzioni, introdotte da “$::=$”. Il comando più semplice è l’assegnamento, che usa l’operatore “$:=$” per assegnare un valore ad una variabile.
Con il simbolo $E$ indichiamo un simbolo non terminale della grammatica che sta per espressione. Una volta costruito semplici espressioni possiamo combinarle, eseguendole in sequenza, inserendo un $;$ tra due comandi.
In merito all’istruzione di scelta abbiamo l’istruzione “$if$”, seguito da un’espressione booleana, seguito da “$then$”, seguita da un comando, seguita da “$else$”, seguita da un comando, e il tutto viene concluso da “$endif$”. Qui abbiamo una prima semplificazione dicendo che l’else è obbligatorio.
Per l’iterazione abbiamo il “$while$”, seguito da un’espressione booleana, seguito da “$do$” con poi il comando, il tutto concluso da $endwhile$.
Infine abbiamo una istruzione speciale, chiamata “$skip$”, che non fa nulla e avanza il program counter (con essa posso saltare il ramo alternativo dell’if-else).
Un’espressione booleana “$B$” può essere la costante “true”, la costante “false” o del tipo “not B”, “B and B”, “B or B”, “E < E” (e le altre), “E = E”.
Non si hanno tipi di dato ma supporremo di avere a che fare solo con interi. Non si ha la funzione di nozione o di classe. Questo linguaggio è comunque Turing Complete.
Definizione: Una dimostrazione, in una logica data, è una sequenza di formule di quella logica che sono o assiomi (formule che riteniamo vere a priori) o formule derivate dalle precedenti tramite una regola di inferenza. Una regola di inferenza mi manda da un insieme di formule $\alpha_1, \alpha_2, ..., \alpha_n$ ad una nuova formula $\alpha$ e si indica con:
$$ \frac{\alpha_1, \alpha_2, ..., \alpha_n}{\alpha} $$
Che si legge come “se ho già derivato $\alpha_1, \alpha_2, ..., \alpha_n$ sono autorizzato a derivare $\alpha$”.
Nel nostro caso ogni $\alpha_i$ è una tripla della logica di Hoare.
Una dimostrazione si ottiene quindi applicando le regole di derivazione fino ad arrivare, se si riesce, ad una soluzione.