Comme nous l'avons vu, l'objectif premier des définition et développements formels de l'activité de programmation est de garantir la correction des programmes. Alors que la sémantique d'un programme donne toute la signification de ce programme, la preuve de correction, ell, se limite à démontrer une propriété de ce programme.
Considérons le programme trivial x:=1. Sa sémantique est la fonction qui à tout état mémoire s associe (s|x→1). Une propriété vérifiée par ce programme est “quelque soit l'état initial, x est positif dans l'état final.”
Un système formel (extérieur au langage considéré) dont les formules sont de la forme {p} P {q} (on parle de triplet de Hoare) où
q[x\exp] est le prédicate q dans lequel toutes les occurrences de x ont été substituées par exp.{1>0} x:=1 {x>0} est un axiomeb then A else B {q}b then A else B {q} (en remplaçant B par skip).b do A {p :\ ~b}, où p est appelé invariante de l'itération. Intuitivement, le corps de l'itération (A) maintient p invariant, on a {p} A {p}.vrai ⇒ 1>0 et {1>0} x:=1 {x>0} est un axiome on a : {vrai} x:=1 {x>0}Cette fonction de transition est définie de la manière suivante. On notera E, E1,E2,…les états mémoire de cette machine.
| Affectation | δ(x:=exp) E1 = E2 tel que E2(v) = E1(exp) si v = x E2(v) =E1(v) si v ≠ x |
|---|---|
| Séquence | \delta\left(A;B\right) =\delta\left(B\right) \circ \delta\left(A\right) |
| Alternative | δ(if b then A else B) E = δ(A)E si E(b)=vrai δ(B)E si E(b)=faux |
| Itération | δ(while b do A ) E = Ek, où Ei := δ(A)i E et k est le plus petit entier tel que Ek(b)=faux. \delta\left(A\right)^i E = \delta\left(A\right) \circ \delta\left(A\right)^{i-1} E. |
La formule {p} P {q} est vraie dans cette interprétation si pour tout état mémoire E1, E2 tels que E1(p)=vrai et δ(P)E1=E2 alors E2(q)=vrai. Cette interprétation définit un modèle des formules {p} P {q}. Toute formule que l'on peut déduire par le système de déduction à partir des axioms est vraie dans cette interprétation.
On peut rapprocher cette interprétation de ce système formel de la sémantique dénotationnelle des langages impératifs. Dans un cas il s'agit d'une définition sémantique d'un langage. Dans l'autre il s'agit d'un système de preuve de propriétés des programmes. Mais dans les deux cas l'univers d'interprétation des énoncés est le meme, celui des fonctions sur un ensemble d'états mémoire. L'univers d'interprétation des énoncés et leur domaine sémantique sont identiques.
Dans le cas de l'itération, la fonction de transition n'est pas toujours définie. Cette interprétation associée au système formel de Hoare fournit donc une technique de correction partielle des programmes.
La formule {p} P {q} signifie intuitivement :
Si le prédicat p est vérifié dans l'état mémoire avant P, et si l'exécution de P termine, alors le prédicat q est vérifié dans l'état mémoire résultant de l'exécution de P.
| Démonstration du théorème : | |
|---|---|
| {x≥0 ∧ y>0} | initial |
| a:=0; b:= x while b ≥ y do {a:=a+1; b:= b-y} | programme |
| { x = ay + b ∧ 0≤b<y } | final |
| Formule | J ustification |
|---|---|
| {x=0y+x ∧ x≥0 } a:=0 {x = ay+x ∧ x ≥ 0 } | Axiome 1 |
| {x=ay+x ∧ x≥0 } b:= x {x = ay+x ∧ b ≥ 0 } | Axiome 1 |
| {x≥0 ∧ y>0} a:=0; b:=x {x = ay+b ∧ b ≥ 0 } | R1 (affectation) (*) |
| {x=ay+b-y ∧ b-y>0} b:= b-y { x=ay+b ∧ b ≥ 0 } | Axiome 1 |
| {x=(a+1)y+b-y ∧ b-y>0} a:=a+1 { x=ay+b ∧ b-y>0} | Ax. 1 |
| {x=ay+b ∧ b ≥ 0 ∧ b ≥ y} a:=a+1; { x=ay+b-y ∧ b-y≥0} | R4, puisque x=ay+b & b≥0 & b≥y ⇒ x(a+1)y+b-y ∧ b-y≥0 |
| {x=ay+b ∧ b ≥ 0 ∧ b ≥ y} a:=a+1;b:=b-y { x=ay+b ∧ b ≥ 0} | R1, et x=ay+b est p, l'invariante de boucle |
| {x=ay+b ∧ b ≥ 0} while b ≥ y do [a:=a+1;b:=b-y] {x=ax+b ∧ b ≥ 0 ∧ ~(b ≥ y)} | R3 |
| {x=ay+b ∧ b ≥ 0} while b ≥ y do [a:=a+1;b:=b-y] {x=ax+b ∧ 0≤b<y} | R3, puisque b≥ 0 ∧ ~(b ≥ y} ⇒ 0≤b<y |
Enfin, avec (*), on conclue: {x≥0 ∧ y>0} a:=0; b:=x; while b ≥ y do [a:=a+1;b:=b-y] {x=ax+b ∧ 0≤b<y}
Résumé de cette preuve (annotation de programme)
Trouver l'invariante 'x=ay+b ∧ b ≥0' est la principale difficulté. La preuve consiste principalement à démontrer que 'x=ay+b ∧ b ≥0' est un invariant d'itération. De manière générale, la preuve consiste essentiellement à définir un invariant de l'itération.