Correction partielle et logique de Hoare

Pour la correction partielle on ne s'intéresse pas à la terminaison.

On définit:

$\{P\} \mathtt{I} \{Q\}$

• $P$ est une précondition (assertion sur les variables du programme)
• $Q$ est une postcondition (assertion sur les variables du programme)
• $\mathtt{I}$ est une instruction.

$\{P\} \mathtt{I} \{Q\}$ signifie que si l'état du système vérifie l'assertion P alors après exécution de $S$, si l'instruction termine l'état du système vérifiera Q.

Plus précisément, les assertions considérées sont des assertions sur l'état du système (ici l'état des variables). En notant $S\models P$ le fait que $P$ est vrai dans l'état $S$, on aura (on suppose que pour tout $P$, $\bot \models P$):

$$(\{P \} \mathtt{Inst} \{ Q \}) \Longleftrightarrow (\forall S... ...dels P \Longrightarrow \mathcal{I}(\mathtt{Inst})(S)\models Q)$$

$\{P\} \mathtt{I} \{Q\}$ peut servir à spécifier et à documenter les programmes. Mais, $P$ et $Q$ ne sont pas définis de façon unique.

Exemple: On a:

$$\{x\geq 0\} \mathtt{x:= x+1} \{x \geq 0\}$$

Mais aussi:

$$\{x\geq 0\} \mathtt{x:= x+1} \{x > 0\}$$

Ou encore

$$\{y > 0\} \mathtt{x:= x+1} \{y \geq 0\}$$

Vérifions par exemple la première assertion. Soit un état $S$ qui vérifie $x\geq 0$, après l'affectation $\mathtt{x := x+1}$ la valeur de la variable $\mathtt{x}$ est supérieure ou égale à $1$ et on a donc aussi $x\geq 0$: le nouvel état $S'$ vérifie donc $S'\models x \geq 0$.

Remarques:

• $True$ est vérifié dans tout état et donc pour tout $P$, toute instruction $\mathtt{Ins}$, on a:
  
  $$\{P \} \mathtt{Ins} \{ True \}$$
  
  
  De même $False$ ne peut jamais être vrai aussi, pour tout $P$, toute instruction $\mathtt{Ins}$, on a:
  
  $$\{False \} \mathtt{Ins} \{ P \}$$
  
  

Plus généralement on a peut vérifier les propriétés suivantes:

• (1) Si $\{P \} \mathtt{Ins} \{ Q\}$ et si $Q \Rightarrow S$ alors $\{P \} \mathtt{Ins} \{ S\}$
• (2) Si $\{P \} \mathtt{Ins} \{ Q\}$ et si $P \Rightarrow S$ alors $\{S \} \mathtt{Ins} \{ Q\}$
• (3) Si $\{P \} \mathtt{Ins_1} \{ Q\}$ et $\{Q \} \mathtt{Ins_2} \{ R\}$ alors on a $\{P \} \mathtt{Ins_1;Ins_2} \{ R\}$

Prouvons par exemple (1): Soit $S$ tel que $S\models P$, et $S'=\mathcal{I}(\mathtt{Ins})(S)$, par hypothèse $S'\models Q$, or $Q \Rightarrow S$ et donc $S'\models Q$ (tout état vérifiant $Q$ vérifie a fortiori $S$.

Les autres propriétés se prouveraient de la façon similaire en se ramenant à la sémantique opérationnelle du langage de programmation.

On peut définir la substitution dans les assertions: si $x$ est une variable figurant dans l'assertion $P$, $P[x\leftarrow c]$ est $P$ dans lequel toutes les occurrences de $x$ ont été remplacées par $c$. (Attention, il s'agit d'une définition informelle une définition complète devra différencier entre une variable libre et une variable liée). On a alors:

• (4) $\{P \}[x\leftarrow c] \mathtt{x:=c} \{P \}$

Exemple: Vérifier que en utilisant (4) que:

$$\{x\geq 0\} \mathtt{x:= x+1} \{x > 0\}$$