Démonstration du tri sélection

Invariant de boucle

Un invariant de boucle est une propriété logique qui est :

• Vraie avant le début de la boucle (initialisation),
• Conservée à chaque itération de la boucle (maintien),
• Encore vraie à la fin de la boucle (lorsque la condition de la boucle devient fausse).

L'invariant de boucle sert à raisonner sur le comportement d'un algorithme et à prouver sa correction. C'est un outil clé en informatique pour démontrer qu'une boucle atteint son objectif tout en restant dans un état cohérent.

Reprenons l'algorithme du tri sélection, en le prenant en ordre croissant avec le minimum (on range par la gauche)

def tri_selection(tab):
    n = len(tab)
    for i in range(n - 1):  # Boucle principale
        min_index = i
        for j in range(i + 1, n):  # Recherche du minimum
            if tab[j] < tab[min_index]:
                min_index = j
        tab[i], tab[min_index] = tab[min_index], tab[i]  # Échange
    return tab

Ici, voici l'invariant de boucle que nous allons utiliser :

À chaque itération i de la boucle externe, les i premiers éléments du tableau (tab[0] à tab[i-1]) sont triés et sont les i plus petits éléments du tableau.

Pour démontrer la terminaison, et la correction de l'algorithme du tri par sélection à l'aide d'un invariant de boucle, il faut suivre une méthode rigoureuse qui s'appuie sur trois étapes principales :

• Définir l'invariant de boucle (propriété vraie à chaque itération).
• Montrer que l'invariant est vérifié initialement.
• Montrer que l'invariant est maintenu à chaque itération et que la boucle termine.

Étapes de la démonstration

Initialisation

• Avant toute exécution de la boucle externe, aucun élément n’a été traité.
• La sous-partie du tableau correspondant aux indices 0 à i-1 (ici vide) est donc trivialement triée.
• L’invariant est donc vérifié avant la première itération.

Maintien : l'invariant est conservé à chaque itération

Supposons que l’invariant est vrai au début de l’itération i. Cela signifie que les i premiers éléments (tab[0] à tab[i-1]) sont triés et sont les i plus petits éléments du tableau.

• L’algorithme cherche dans la sous-partie restante (tab[i] à tab[n-1]) l’élément minimum.
• Il place cet élément à l’indice i en échangeant les valeurs.
• Après cette opération, les i+1 premiers éléments (tab[0] à tab[i]) sont triés et correspondent aux i+1 plus petits éléments du tableau. En effet, l'élément minimum trouvé est par définition plus grand que tous les précédents, et plus petit que tous les suivants.

Ainsi, l’invariant est maintenu à chaque itération.

Terminaison : l’algorithme s’arrête et donne le bon résultat

La boucle externe s’arrête lorsque i = n - 1. À ce moment, l’invariant garantit que :

• Les n-1 premiers éléments (tab[0] à tab[n-2]) sont triés.
• Le dernier élément (tab[n-1]) est déjà correctement placé, car il est le plus grand.

Donc, tout le tableau est trié lorsque la boucle se termine.

Conclusion

La combinaison de l’invariant et de la progression de la boucle (i augmente à chaque itération, et la boucle s'arrête lorsque i = n-1) garantit la terminaison de l’algorithme. L'invariant de boucle est donc un outil puissant pour démontrer la correction et la terminaison de l'algorithme du tri par sélection.