===== III. Preuves de correction des programmes =====

==== Sémantique et preuve ====
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.

=== Exemple ===
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."//

==== La logique de Hoare ====

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ù
  * P est un énoncé dans un langage donné (dans la théorie de Hoare, ce langage est un langage impératif structuré)
  * {p} et {q} sont des formules du calcul des prédicats du premier ordre, appelés respectivement pre- et post-conditions de l'énoncé P
  * muni d'un certain nombre d'axiomes et de règles de déduction

=== Axiomes ===

  * Axiome 1 : __affectation__
    * {q[x\exp]} x:= exp {q} où ''q[x\exp]'' est le prédicate q dans lequel toutes les occurrences de x ont été substituées par ''exp''.
    * exemple : ''{1>0} x:=1 {x>0} '' est un axiome
  * Axiome 2 : __instruction vide__
    * {p} skip {p}

=== Règles ===

  * Règle 1 : __séquence__
    * {p} A {r}, {r} B {q} => {p} A;B {q}
  * Règle 2 : __altérnative__
    * {p /\ b} A {q}, {p /\ ~b} B {q} => {p} if ''b'' then A else B {q}
    * cas particulier de la conditionnelle :
      * {p /\ b} A {q}, {p /\ ~b} => {q} 
        *  => {p} if ''b'' then A else B {q} (en remplaçant B par skip).
  * Règle 3 : __itération__
    * {p /\ b} A {q} =>
      * {p} while ''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}.
  * Règle 4 : __ conséquence__
    * p =>> p', {p'} A {q'}, q' => q
      * => {p} A {q}
    * exemple : puisque ''vrai'' => 1>0 et {1>0} x:=1 {x>0} est un axiome on a : {vrai} x:=1 {x>0}

==== Interprétation associée à ce système formel ====

  * les prédicats p et q sont interprétés classiquement dans la logique du premier ordre
    * tout prédicat est une application dans {vrai, faux}
    * les opérations booléennes sont définies par les tables de vérité classiques.
  * l'énoncé P est interprété  par 
    * une fonction de transition notée δ(P) entre les états mémoire d'une machine abstraite.  
 
Cette fonction de transition est définie de la manière suivante. On notera E, E<sub>1</sub>,E<sub>2</sub>,...les états mémoire de cette machine.

^ Affectation | δ(x:=exp) E<sub>1</sub> = E<sub>2</sub> tel que \\ E<sub>2</sub>(v) = E<sub>1</sub>(exp) si v = x \\   E<sub>2</sub>(v) =E<sub>1</sub>(v)  si v ≠ x |
^ Séquence | <jsm>\delta\left(A;B\right) =\delta\left(B\right) \circ \delta\left(A\right)</jsm> |
^ 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 = E<sub>k</sub>, où E<sub>i</sub> := δ(A)<sup>i</sup> E et k est le plus petit entier tel que E<sub>k</sub>(b)=faux. \\ <jsm>\delta\left(A\right)^i E = \delta\left(A\right) \circ \delta\left(A\right)^{i-1} E</jsm>.|

La formule {p} P {q} est vraie dans cette interprétation si pour tout état mémoire E<sub>1</sub>, E<sub>2</sub> tels que E<sub>1</sub>(p)=vrai et δ(P)E<sub>1</sub>=E<sub>2</sub> alors E<sub>2</sub>(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.

=== Remarque ===
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.

==== Exemple ====

^  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)
  - {x≥0 ∧ y>0} => {x=0y+x ∧ x≥0}
  - a:=0
  - {x=ay+x ∧ x≥0}
  - b:= x
  - {x=ay+b ∧ b≥0}
  - while  b≥y do
    - {x=ay+b ∧ b≥0 ∧ b≥y} => {x=(a+1)y+b-y ∧ b-y≥0}
    - a:= a+1
    - {x=ay+b ∧ b-y≥0}
    - b:= b - y
    - {x=ay+b ∧ b≥0}
  - {x=ay+b ∧ b ≥ 0 ∧ ~(b ≥ y)} => {x=ax+b ∧ 0≤b<y}

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.