Preuves de correction (suite)

Exemple

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
Résumé de la preuve (par annotation du programme)
  • {vrai} ⇒ {n+m = n+m} : pre-condition
  • a:= n;
  • {a+m = n+m}
  • b:= m;
  • {a+b = n+m}
  • while b≠0 do
    • {
    • {a+b = n+m ∧ b≠0} ⇒ {a+1+b-1 = n+m}
    • a:= a+1
    • {a+b-1 = n+m}
    • b:= b-1
    • {a+b =n+m}} : invariant
  • }
  • {a+b = n+m ∧ ¬(b≠0) } ⇒ {a = n+m} : post-condition

Correction partielle : si precondition et si programme termine!

Extension de la logique de Hoare

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.

Preuve de 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

  • bornées inférieurement
  • strictement décroissantes à chaque étape de l'itération.
Exemple : racine carrée entière
{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 :

Somme des n premiers entiers
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

  • prendre {n≥0} comme pré-condition initiale
  • ajouter {0 ≤ i ≤ n } à l'invariant
  • prendre n-i comme variant (0 = borne inf.)

Minimum d'un tableau de nombres

PGCD de 2 nombres entiers

FIXME trois pages à rajouter.

 
m1ilc/semantics_7.txt · Dernière modification: 2010/05/24 13:49 par suitable
 
Sauf mention contraire, le contenu de ce wiki est placé sous la licence suivante :CC Attribution-Noncommercial-Share Alike 3.0 Unported
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki