Preuve d'algorithmes

Preuve d'algorithmes

Qu'est-ce qu'une preuve d'algorithme ?

La preuve d'algorithme est une démonstration mathématique qu'un algorithme produit le résultat attendu pour toutes les entrées valides et qu'il se termine effectivement.

Structure générale d'une preuve d'algorithme

Pour prouver qu'un algorithme itératif est correct, on suit généralement ces étapes :

1. Spécification : Définir clairement ce que l'algorithme doit faire (préconditions et postconditions).
2. Choix de l'invariant : Identifier une propriété qui reste vraie tout au long de la boucle.
3. Preuve de l'invariant:
   • Initialisation : L'invariant est vrai avant la première itération.
   • Conservation : Si l'invariant est vrai avant une itération, il reste vrai après.
4. Choix de la variante : Identifier une expression positive qui décroît à chaque itération.
5. Preuve de la terminaison : Montrer que la variante décroît strictement et atteint sa borne.
6. Conclusion : À la sortie, l'invariant + condition d'arrêt impliquent la postcondition.

Exemple complet 1 : Somme des n premiers entiers

Considérons l'algorithme classique de calcul de la somme \(S = 1 + 2 + \ldots + n\).

int somme(int n) {
    int s = 0;
    int i = 1;
    while (i <= n) {
        s = s + i;
        i = i + 1;
    }
    return s;
}

def somme(n):
    s = 0
    i = 1
    while i <= n:
        s = s + i
        i = i + 1
    return s

Spécification

• Précondition : \(n \ge 1\)
• Postcondition : \(s = 1 + 2 + \ldots + n\)

1. Preuve de correction partielle (invariant)

Invariant choisi : \(s = 1 + 2 + \ldots + (i-1)\)

• Initialisation : Avant la boucle, \(i = 1\) et \(s = 0\). La somme de 1 à 0 est vide, donc \(s = 0\). L'invariant est vrai.
• Conservation : Supposons l'invariant vrai avant une itération. On a \(s = 1 + \ldots + (i-1)\). Pendant l'itération, on ajoute \(i\) à \(s\), donc après l'ajout, \(s = 1 + \ldots + i\). Puis on incrémente \(i\) (nouvel \(i = i_{ancien} + 1\)). Après l'itération, l'invariant \(s = 1 + \ldots + (i-1)\) est rétabli.

2. Preuve de terminaison (variante)

Variante choisie : \(v = n - i + 1\)

• Positivité : Tant que \(i \le n\), \(v \ge 1\).
• Décroissance stricte : À chaque itération, \(i\) augmente de 1, donc \(v\) diminue exactement de 1.
• Borne inférieure : Lorsque \(i = n+1\), \(v = 0\) et la condition de boucle devient fausse.

3. Conclusion

À la sortie de la boucle, \(i = n+1\) et l'invariant donne \(s = 1 + \ldots + n\). L'algorithme est donc correct et se termine pour tout \(n \ge 1\).

Exemple complet 2 : Recherche du maximum dans un tableau

int maximum(int tab[], int n) {
    int max = tab[0];
    int i = 1;
    while (i < n) {
        if (tab[i] > max)
            max = tab[i];
        i++;
    }
    return max;
}

def maximum(tab):
    max_val = tab[0]
    i = 1
    while i < len(tab):
        if tab[i] > max_val:
            max_val = tab[i]
        i += 1
    return max_val

Spécification

• Précondition : Tableau non vide (\(n \ge 1\))
• Postcondition : \(\text{max\_val} = \max(tab[0], tab[1], \ldots, tab[n-1])\)

1. Preuve de correction partielle (invariant)

Invariant choisi : \(\text{max\_val} = \max(tab[0], tab[1], \ldots, tab[i-1])\)

• Initialisation : Avant la boucle, \(i = 1\) et \(\text{max\_val} = tab[0]\). Le maximum du premier élément est bien \(tab[0]\). L'invariant est vrai.
• Conservation: Supposons l'invariant vrai avant une itération. On compare \(tab[i]\) avec \(\text{max\_val}\) :
  • Si \(tab[i] > \text{max\_val}\), on met à jour \(\text{max\_val}\) avec \(tab[i]\).
  • Sinon, \(\text{max\_val}\) reste inchangé.
  Dans les deux cas, après l'itération, \(\text{max\_val} = \max(tab[0], \ldots, tab[i])\). Après incrémentation de \(i\), l'invariant est rétabli.

2. Preuve de terminaison (variante)

Variante choisie : \(v = n - i\)

• Positivité : Tant que \(i < n\), \(v \ge 1\).
• Décroissance stricte : À chaque itération, \(i\) augmente de 1, donc \(v\) diminue de 1.
• Borne inférieure : Lorsque \(i = n\), \(v = 0\) et la condition de boucle devient fausse.

3. Conclusion

À la sortie, \(i = n\) et l'invariant donne \(\text{max\_val} = \max(tab[0], \ldots, tab[n-1])\). L'algorithme est correct et se termine.

Exemple complet 3 : Recherche dichotomique

int recherche_dichotomique(int tab[], int n, int x) {
    int debut = 0;
    int fin = n - 1;
    
    while (debut <= fin) {
        int milieu = (debut + fin) / 2;
        if (tab[milieu] == x)
            return milieu;
        else if (tab[milieu] < x)
            debut = milieu + 1;
        else
            fin = milieu - 1;
    }
    return -1;
}

def recherche_dichotomique(tab, x):
    debut, fin = 0, len(tab) - 1
    
    while debut <= fin:
        milieu = (debut + fin) // 2
        if tab[milieu] == x:
            return milieu
        elif tab[milieu] < x:
            debut = milieu + 1
        else:
            fin = milieu - 1
    return -1

Spécification

• Précondition : Tableau trié en ordre croissant.
• Postcondition : Retourne un indice \(i\) tel que \(tab[i] = x\) s'il existe, sinon \(-1\).

1. Preuve de correction partielle (invariant)

Invariant choisi : Si \(x\) est présent dans le tableau, alors \(x \in tab[\text{debut} \ldots \text{fin}]\).

• Initialisation : \(\text{debut} = 0\), \(\text{fin} = n-1\). L'intervalle couvre tout le tableau. L'invariant est vrai.
• Conservation: Supposons l'invariant vrai avant une itération. On compare \(x\) avec \(tab[\text{milieu}]\) :
  • Si \(x = tab[\text{milieu}]\), on retourne l'indice (fin anticipée).
  • Si \(x > tab[\text{milieu}]\), alors \(x\) ne peut être que dans la moitié droite (tableau trié). On pose \(\text{debut} = \text{milieu} + 1\).
  • Si \(x < tab[\text{milieu}]\), alors \(x\) ne peut être que dans la moitié gauche. On pose \(\text{fin} = \text{milieu} - 1\).
  Dans tous les cas, si \(x\) est présent, il reste dans le nouvel intervalle. L'invariant est conservé.

2. Preuve de terminaison (variante)

Variante choisie : \(v = \text{fin} - \text{debut} + 1\) (taille de l'intervalle)

• Positivité : Tant que \(\text{debut} \le \text{fin}\), \(v \ge 1\).
• Décroissance stricte : À chaque itération, on réduit l'intervalle à sa moitié gauche ou droite. Dans les deux cas, la taille du nouvel intervalle est strictement inférieure à l'ancienne (au moins divisée par 2).
• Borne inférieure : Lorsque \(\text{debut} > \text{fin}\), \(v = 0\) et la boucle se termine.

3. Conclusion

• Cas trouvé : L'algorithme retourne l'indice correct.
• Cas non trouvé : La boucle se termine avec \(\text{debut} > \text{fin}\). L'invariant implique que \(x\) n'est pas dans le tableau, donc le retour \(-1\) est correct.

Récapitulatif des preuves

Extension aux algorithmes récursifs

Pour les algorithmes récursifs, la preuve d'exactitude utilise le principe de récurrence (ou induction) plutôt que des invariants de boucle.

Exemple : Factorielle récursive

int factorielle(int n) {
    if (n <= 1)
        return 1;
    else
        return n * factorielle(n - 1);
}

def factorielle(n):
    if n <= 1:
        return 1
    else:
        return n * factorielle(n - 1)

Preuve par induction

• Cas de base (\(n = 0\) ou \(n = 1\)) : La fonction retourne 1, ce qui est correct par définition (\(0! = 1! = 1\)).
• Hypothèse de récurrence : Supposons que \(factorielle(k)\) est correct pour tout \(k < n\).
• Pas de récurrence : Pour \(n > 1\), \(factorielle(n) = n \times factorielle(n-1)\). Par hypothèse, \(factorielle(n-1) = (n-1)!\). Donc \(factorielle(n) = n \times (n-1)! = n!\).

L'algorithme est donc correct pour tout \(n \ge 0\).