Démontrons ce théorème d la logique de Hoare :
a:= n; b:= m while b<>0 do a:=a+1; b:=b-1 {a=n+m}
| {n+m = n+m} a:=n {a+m = n+m} | Axiome 1 |
{a+m = n+m} b:=m {a+b = n+m} | Axiome 1 |
{n+m = n+m} a:=n; b:=m {a+b = n+m} | R1 |
vrai ⇒ n+m = n+m | |
{vrai} a:=n; b:=m {a+b = n+m= | Règle 4 |
corps de l'itération | |
---|---|
{a+1+b-1 = n+m} a:= a+1 {a+b-1 = n+m} | Axiome 1 |
{a+b-1 = n+m} b:= b-1 { {a+b = n+m } | Axiome 1 |
{a+1+b-1 = n+m} a:=a+1; b:=b-1 {a+b = n+m} [ Règle 1 | |
{a+b = n+m ∧ b≠0} a:=a+1; b:= b-1 {{a+b = n+m} | R1, puisque a+b=n+m ∧ b≠0 ⇒ a+1+b-1 = n+m |
{a+b = n+m} while b≠0 do [a:=a+1; b:=b-1] {a+b = n+m ∧ ¬(b≠0) } | pre- P post (R3) |
{a+b = n+m} while b≠0 do [a:=a+1; b:=b-1] {a = n+m } | Règle 4, car a+b=n+m ∧ ¬(b≠0) ⇒ a=n+m |
{vrai pre- a:=n; b:=m while b≠0 do [a:=a+1; b:=b-1] {a = n+m } post | Règle 1 |
Correction partielle : si precondition et si programme termine!
On peut, en effet, étendre la logique de Hoare pour montrer correction totale, c'est à dire correction partielle plus terminaison. Pour cela, il faut completer la règle de l'itération et en démontrer la terminaison.
En interprétant l'itération (en utilisant l'interprétation associée à la logique de Hoare) et en choisissant une expression (appelée variant ) dont les valeurs au cours de l'itération sont
{n ≥ 0} r:= 0; s:= n+1; while (s ≠ r+1) do { m:= (r+s) div 2; if m*m=n then s:= m else r:= m } {r*r ≤ n < (r+1)*(r+1) }
Exercice (à faire soi-même) : On démontre ce théorème (correction partielle) en prenant pour invariant r*r ≤ n < s*s.
Pour la preuve de terminaison, choisissons pour variant l'expression s-r. Les valeurs de cette expression sont bornées en bas par 1 (d'après l'invariant r*r ≤ n < s*s ⇒ s-r≥1). Elles sont strictement décroissantes : soient E1 et E2 tels que E2 = δ(A) E1, alors E2(s-r) < E1(s-r). CQFD.
Autres exemples pour montrer l'utilisation en pratique de la logique de Hoare pour prouver des programmes classiques :
s:=0; i:=1; while i ≠ n do { i:=i+1; s:=s+i; }
Une technique pour trouver un invariant consiste à décomposer la post-condition sous la forme p ∧ ¬b où p est l'invariant recherché et b est la condition de l'itération. Ici la post-condition est \left\{s=\sum_{k=1}^{n} k\right\}. Réécrit en \left\{s=\sum _{k=1}^{i} k \& \not\left(i\neq n\right) \right\}
On va montrer que \left\{s=\sum _{k=1}^{i} k \ \right\} est un invariant.
Démonstration (en remontant les instruction).
{vrai} ⇒ {0=∑k=1,0 k } | l'invariant de boucle est vrai sans plus forte pré-condition que {vrai} | |
s:=0 ; | { s = ∑k=1,0 k } | |
i:=0 ; | { s = ∑k=1,i k } | on avait i:=1 en cours, je crois, mais ça ne marche pas! |
---|---|---|
while i <> n do | ||
{ s + i + 1 = = ∑k=1,i+1 k } | ||
i:= i+1 | { s + i = = ∑k=1,i k } | |
s:=s+i | { s = = ∑k=1,i k } | |
} | fin de satisfaction de la condition | |
{s = ∑k=1,i k ∧ ¬(i ≠ n)} ⇒ {s =∑k=1,n k } |
Pour montrer la terminaison, il suffit de
trois pages à rajouter.