Logique de Hoare

Logique de Hoare

La logique de Hoare (Floyd-Hoare, 1969) est un systeme formel pour raisonner sur la correction des programmes.

Triplet de Hoare

{P} C {Q}

• P : precondition (vraie avant C)
• C : commande (le code)
• Q : postcondition (vraie apres C, si C termine)

Interpretation

Si P est vraie avant C, et si C termine, alors Q est vraie apres.

On parle de correction partielle (la terminaison est prouvee separement via un variant).

Regles d'inference de Hoare

1. Axiome d'affectation

{P[x := E]} x = E; {P}

2. Regle de composition

{P} S1 {R} && {R} S2 {Q} => {P} S1; S2 {Q}

3. Regle du conditionnel

{P && B} S1 {Q} && {P && !B} S2 {Q} => {P} if(B) S1 else S2 {Q}

4. Regle de la boucle while

{P && B} S {P} => {P} while(B) S {P && !B}

Ou P est l'invariant de boucle.

5. Regle de consequence

P' => P && {P} C {Q} && Q => Q' => {P'} C {Q'}

Application : premmin(x)

// @pre: aucune
// @post: j = premmin(x)
if (|x| == 0) { j = NEANT; }
else {
    j = 0; k = 1;
    // @invariant: 1 <= k <= |x| && j = premmin(x[0..k-1])
    // @variant: k
    while (k < |x|) {
        if (x[k] < x[j]) j = k;
        k = k + 1;
    }
}

Verification de l'invariant

1. Initialisation : k=1, j=0. x[0..0] a pour minimum x[0]=x[j]. OK.
2. Preservation : Si invariant tient et k < |x| :
   • Si x[k] < x[j] alors j=k (nouveau min du prefixe)
   • k incremente, prefixe s'etend
   • Invariant preserve.
3. Terminaison : Quand k >= |x|, j = premmin(x). OK.

Variant : |x|-k decroit strictement.

Methode de preuve d'une boucle

1. Trouver l'invariant P tel que :

   • P vrai avant d'entrer dans la boucle
   • P preserve par le corps de boucle
   • P && !B => Q (postcondition)

2. Trouver le variant V (entier naturel) :

   • V decroit strictement a chaque iteration
   • V >= 0 garantit la terminaison

Exemple : insertion croissante

• Invariant : x[k]=a et x = u[0..k-1].insc(u[k..|u|-1], a)
• Variant : k (decroit de 1 par echange)

Pourquoi c'est important

Sans invariant, impossible de prouver qu'une boucle fait ce qu'on attend.
Sans variant, impossible de garantir qu'elle termine.