III. Correction d'un algorithme

Cours

Nous avons étudié le coût de deux algorithmes de tri, mais... font-ils bien ce qu'ils sont sensés faire, c'est-à-dire trier ? A tous les coups ?

L'étude des algorithmes passe parce qu'on appelle la preuve de leur correction : qu'ils font le travail voulu (preuve de correction) et montrer qu'ils se terminent (preuve de terminaison) - sinon... aucune chance qu'ils fassent ce que l'on veut qu'ils fassent ! -.

A. Correction

Définition

Pour montrer qu'un algorithme est correct, on montre qu'une propriété :
- est vraie avant de rentrer dans la boucle,
- reste vraie à chaque itération de boucle.
Si elle est vraie à chaque fois, elle sera vraie... à la fin.
On parle d'invariant de boucle.

La preuve de ces invariants se fait par récurrence qui est une notion mathématique que vous n'avez pas encore vue (nous n'allons donc pas faire les démonstrations).

A.I. Algorithme de calcul de moyenne

On considère la fonction suivante, qui doit calculer la moyenne des éléments de liste :

def moyenne(liste) :
    t = 0
    for i in range(len(liste)):
        t = t + liste[i]
        # assertion vraie à cet endroit
    return t/len(liste)

Que contient t après chaque passage de boucle ?

t contient les i+1 premiers éléments de liste.

Que peut-on en conclure sur ce que contient t à la fin de l'exécution de la boucle ?

On peut en conclure qu'à la fin de l'exécution de la boucle, t contient la somme des len(liste)-1+1 premiers éléments : donc tous les éléments de liste.

t contient bien la valeur attendue, et on sait ce que renvoie len(liste). Le résultat renvoyé par la fonction est donc correct.

L'invariant est qu'après chaque itération de boucle i, t contient la somme des i+1 premiers éléments de liste.

A.II. Les algorithmes de tri

Exemple 1 : Le tri par sélection

On donne le code suivant, devant trier t avec l'algorithme du tri par sélection :

def tri_selection(t):
    n = len(t)
    for i in range(n):
        ind = i
        for j in range(i+1, n):
            if t[j]<t[ind]:
                ind = j
        if i != ind:
            tmp = t[ind]
            t[ind]=t[i]
            t[i]=tmp
    return t

Les propriétés suivantes sont-elles vraies ou fausse ?

A la fin de l'étape i, le sous-tableau des éléments d'indice 0 à j est trié.

C'est faux, j sert à trouver le minimum sur le sous-tableau i+1:n.

A la fin de l'étape i, le sous-tableau des éléments d'indice 0 à i est trié.

C'est vrai, à la fin de l'étape i, on aura placé le minimum du sous-tableau i+1:n en position i, et les éléments d'avant seront triés.

A la fin de l'étape i, le sous-tableau des éléments d'indice i+1 à n est trié.

C'est faux, ces indices sont parcourus dans la boucle en j, mais seul un élément est sélectionné : le minimum.

Dans le cas particulier où i vaut n-1, le sous-tableau des éléments d'indice 0 à n-1 est trié, donc tout le tableau est trié.

Exemple 2 : Le tri par insertion

On donne le code suivant, devant trier t avec l'algorithme du tri par insertion :

def tri_insertion(t):
    n = len(t)
    for i in range(1,n):
        ref = t[i]
        j = i
        while j>0 and ref<t[j-1]:
            t[j] = t[j-1]
            j=j-1
        t[j] = ref
    return t

Les propriétés suivantes sont-elles vraies ou fausse ?

A la fin de l'étape i, le sous-tableau des éléments d'indice 0 à i-1 est trié.

C'est vrai, les éléments d'indice inférieur à i ont été triés dans les étapes précédentes.

A la fin de l'étape i, le sous-tableau des éléments d'indice 0 à i est trié.

C'est vrai, l'étape i sert à placer l'éléments d'indice i.

A la fin de l'étape i, le sous-tableau des éléments d'indice 0 à n-1 est trié.

C'est faux, ce n'est pas valable pour chaque valeur de i mais uniquement lorsque i vaut n-1.

Dans le cas particulier où i vaut n-1, le sous-tableau des éléments d'indice 0 à n-1 est trié, donc tout le tableau est trié.

Conclusion

Pour les deux algorithmes de tri, l'invariant est : à la fin de chaque étape i, le tableau est trié des indices 0 à i.

B. Terminaison

Un algorithme ne peut pas être correct, si on n'a pas l'assurance qu'il se termine.

Pourquoi est-ce qu'on est sûr qu'un algorithme se termine lorsqu'il contient une boucle bornée ?

Avec une boucle bornée, on exécute forcément la boucle un nombre fini de fois, connu à l'avance. On sait que l'on va sortir de la boucle.

Dans quel cas est-ce qu'on peut ne pas être sûr de si un algorithme va se terminer ou non ?

Lorsque l'on a une boucle non-bornée, on peut créer une boucle infinie.

Que faut-il faire alors pour montrer que l'algorithme se termine bien ?

Il faut montrer que l'on va sortir de la boucle non-bornée car, à un moment donné, sa condition ou une de ses conditions deviendra fausse.

B.I. Tri par sélection

Nous avons vu que le tri par sélection contenait 2 boucles bornées, donc il a toujours une complexité qui est du même ordre de grandeur. Il se termine donc.

B.II. Tri par insertion

Le tri par insertion contient une boucle non-bornée, montrons qu'il se termine tout de même.

Extrait de son implémentation :

ref = t[i]
j = i
while j > 0 and ref < t[j-1]:
    t[j] = t[j-1]
    j=j-1

Quand est-ce que la condition j > 0 devient fausse ?

Elle devient fausse lorsqu'on a parcouru tous les éléments de t jusqu'au premier : on arrive au bout du tableau. La valeur de j est décrémentée à chaque itération de boucle, cette situation se produira donc si l'autre condition ne devient pas fausse avant.

Quand est-ce que la condition ref < t[j-1] devient fausse ?

Elle devient fausse lorsque l'on a trouvé un élément de t de valeur inférieure à la référence t[i]. La valeur de t[j-1] est actualisée à chaque itération de boucle, car j est actualisée.

Définition

j est une valeur entière qui varie strictement à chaque itération, c'est ce qu'on appelle un variant de boucle, qui permet de prouver la terminaison de l'algorithme.

Ici, la première condition deviendra forcément fausse si la deuxième condition n'est pas fausse avant : l'algorithme se termine.

Synthèse

Faire la preuve complète de la correction d'un algorithme sert à prouver qu'il fait bien ce qu'on attend de lui dans tous les cas.

Pour prouver :
- sa correction, on cherche un invariant de boucle,
- sa terminaison, on cherche un variant de boucle.

---

TD

1. La fonction suivante prend en arguments deux entiers positifs et renvoie leur produit.

   def produit(a,b):
       c = 0
       i = 0
       while i < b:
           #
           i = i + 1
           c = c + a
       return c
   

   Quelle propriété reste vraie à chaque passage par la ligne marquée d'un # ?

   A 𝑐 = 𝑎 × (𝑖 + 1)
   B 𝑐 = 𝑎 × (𝑖 − 1)
   C 𝑐 = 𝑎 × 𝑖
   D 𝑐 = 𝑎 × 𝑏

2. On suppose qu'au début de l'exécution la variable K contient un entier positif non nul.
   Lequel des scripts suivants va boucler indéfiniment ?

   A

   i = K+1
   while i < K:
       i = i + 1
   

   B

   i = K-1
   while i < K:
       i = i - 1
   

   C

   i = K-1
   while i < K:
       i = i + 1
   

   D

   i = K+1
   while i >= K:
       i = i - 1
   

3. 𝑎 et 𝑚 étant deux entiers supérieurs à 1, la fonction suivante renvoie \(a^m\).

   def puissance(a,m):
       p = 1
       n = m
       q = a
       while n > 0:
           #
           if n%2 == 0:
               q = q * q
               n = n // 2
           else:
               p = q * p
               n = n - 1
       return p
   

   Quelle est l'égalité qui est vérifiée à chaque passage par la ligne marquée # ?

   A \(𝑝 × 𝑞^𝑛−1 = 𝑎^𝑚\)
   B \(𝑝 × 𝑞^𝑛 = 𝑎^𝑚\)
   C \(𝑝 × 𝑞^{𝑛+1} = 𝑎^𝑚\)
   D \(𝑝 × 𝑞^𝑚 = 𝑎^𝑛\)

4. Un algorithme de tri d’une liste d’entiers est implémenté de la façon suivante :

   def trier(L) :
       for i in range(len(L)):
           indice_min = i
           for j in range(i+1, len(L)):
               if L[j] < L[indice_min] :
                   indice_min = j
       L[i], L[indice_min] = L[indice_min], L[i]
       # assertion vraie à cet endroit
       return L
   

   Parmi les assertions suivantes laquelle reste vraie à chaque itération de la boucle, à l'endroit indiqué ci-dessus ?

   A la sous-liste L[0:i+1] contient les i plus grandes valeurs de L triées par ordre décroissant
   B la sous-liste L[0:i+1] contient les i plus grandes valeurs de L triées par ordre croissant
   C la sous-liste L[0:i+1] contient les i plus petites valeurs de L triées par ordre décroissant
   D la sous-liste L[0:i+1] contient les i plus petites valeurs de L triées par ordre croissant