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).

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.