==== 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 E<sub>1</sub> et E<sub>2</sub> tels que E<sub>2</sub> = δ(A) E<sub>1</sub>, alors E<sub>2</sub>(s-r) < E<sub>1</sub>(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 <jsm>\left\{s=\sum_{k=1}^{n} k\right\}</jsm>.  Réécrit en <jsm> \left\{s=\sum _{k=1}^{i} k \& \not\left(i\neq n\right) \right\}</jsm>

On va montrer que  <jsm> \left\{s=\sum _{k=1}^{i} k \ \right\}</jsm> est un invariant.

Démonstration (en remontant les instruction).

| {vrai} => {0=∑<sub>k=1,0</sub> k } | l'invariant de boucle est vrai sans plus forte pré-condition que {vrai} |
| s:=0 ; | { s = ∑<sub>k=1,0</sub> k } |
| i:=0 ; | { s = ∑<sub>k=1,i</sub> k } ^ on avait i:=1 en cours, je crois, mais ça ne marche pas! |
| while i <> n do |  |
| { s + i + 1 = = ∑<sub>k=1,i+1</sub> k }  |  |
| i:= i+1 | { s + i = = ∑<sub>k=1,i</sub> k } |
| s:=s+i  | { s = = ∑<sub>k=1,i</sub> k } |
| }  | fin de satisfaction de la condition |
| {s = ∑<sub>k=1,i</sub> k  ∧ ¬(i ≠ n)} => {s =∑<sub>k=1,n</sub> 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.