Algorithmes élémentaires et preuve de programmes

Spécifier une fonction, c'est dire ce qu'elle fait sans dire comment : on nomme ses arguments, on écrit sa précondition, propriété que les arguments doivent vérifier pour que l'appel ait un sens, et sa postcondition, propriété qui relie la valeur renvoyée aux arguments. La spécification s'écrit dans la docstring, juste sous la ligne def (voir le thème Python : structures de contrôle et fonctions). C'est elle, et elle seule, que l'on démontre : une fonction est correcte relativement à une spécification, jamais dans l'absolu.

def recherche_sequentielle(valeurs, cible):
    """Renvoie le plus petit indice i tel que valeurs[i] == cible,
    et -1 si cible ne figure pas dans valeurs."""

Une précondition se contrôle à l'exécution par une assertion : assert len(valeurs) > 0 arrête le programme sur un appel interdit, au lieu de le laisser renvoyer n'importe quoi.

Un programme est partiellement correct si, pour toute donnée vérifiant la précondition, s'il s'arrête, alors le résultat vérifie la postcondition. Il termine si, pour toute donnée vérifiant la précondition, son exécution s'arrête après un nombre fini d'opérations. Il est totalement correct s'il est partiellement correct et qu'il termine. Une boucle infinie est donc partiellement correcte pour n'importe quelle postcondition, ce qui montre que la correction partielle seule ne garantit rien. Prouver un programme, c'est démontrer ces deux points séparément, avec deux outils distincts : l'invariant pour la correction partielle, le variant pour la terminaison.

Un invariant de la boucle while condition: est une propriété $P$ de l'état des variables telle que $P$ est vraie avant le premier test de la condition, et telle que, si $P$ est vraie au début d'un tour dont la condition est vraie, alors $P$ est encore vraie à la fin de ce tour. On dit que $P$ est vraie à chaque passage par le test. Un invariant n'est pas une propriété vraie partout dans le corps de la boucle : il peut être momentanément faux au milieu d'un tour, pourvu qu'il soit rétabli avant le test suivant. Pour une boucle for, l'invariant s'écrit au moyen de l'indice de parcours, par exemple « avant le tour d'indice $i$, la variable plus_grand vaut le maximum des $i$ premiers éléments ».

Théorème : soit une boucle while condition: et une propriété $P$ de l'état des variables. On suppose les deux hypothèses suivantes.
1) Initialisation : $P$ est vraie juste avant le premier test de la condition.
2) Conservation : pour tout état où $P$ est vraie et où la condition est vraie, l'exécution du corps de la boucle laisse $P$ vraie.
Alors $P$ est vraie à chaque passage par le test de la condition ; et si de plus la boucle termine, alors, à la sortie, $P$ est vraie et la condition est fausse.
La démonstration est une récurrence sur le nombre de tours déjà effectués (voir le thème Récurrence simple, bloc Fondamental) : l'initialisation donne le rang $0$, la conservation l'hérédité.
La conclusion s'arrête là : le théorème ne dit rien de la terminaison, qui demande un variant, et il ne donne la postcondition $Q$ que si $P$ et la négation de la condition entraînent $Q$. Un invariant qui n'entraîne pas la postcondition est vrai mais inutile.

Un variant de la boucle while condition: est une expression $V$ des variables du programme, à valeurs entières, telle que $V \geq 0$ à chaque passage par le test tant que la condition est vraie, et telle que chaque exécution du corps fasse strictement décroître $V$. Le variant mesure ce qu'il reste à faire : nombre de candidats non encore éliminés, nombre d'éléments non encore placés, valeur d'un entier que l'on divise. Les trois exigences se vérifient une par une : à valeurs entières, minoré, strictement décroissant.

Théorème : soit une boucle while condition:. On suppose qu'il existe une expression $V$ des variables du programme vérifiant les trois hypothèses suivantes.
1) $V$ prend ses valeurs dans $\mathbb{Z}$.
2) Au début de chaque tour, $V \geq 0$.
3) Chaque exécution du corps fait passer $V$ d'une valeur $V_k$ à une valeur $V_{k+1} < V_k$.
Alors la boucle termine, et elle effectue au plus $V_0 + 1$ tours, où $V_0$ est la valeur initiale de $V$.
Démonstration : si la boucle ne terminait pas, la suite $(V_k)_{k \in \mathbb{N}}$ des valeurs prises par $V$ au début des tours successifs serait une suite d'entiers naturels strictement décroissante, ce qui est impossible. Pour le décompte, $V$ étant entier et décroissant d'au moins $1$ par tour, la valeur au début du tour d'indice $k$ vérifie $V_k \leq V_0 - k$ ; comme l'hypothèse 2 donne $V_k \geq 0$, un tour d'indice $k$ n'a lieu que si $k \leq V_0$, d'où au plus $V_0 + 1$ tours.
L'hypothèse 1 est indispensable : la suite de terme général $2^{-k}$ est strictement décroissante et reste strictement positive, et la boucle while x > 0: x = x / 2 ne termine pas mathématiquement.

L'état d'un programme est la liste des valeurs de ses variables à un instant donné ; un tour de boucle va d'un test de la condition au suivant. La trace est la suite des états, que l'on écrit au brouillon sur un petit exemple pour deviner l'invariant. Précondition et postcondition forment la spécification, invariant et variant forment la preuve. Un algorithme est correct relativement à une spécification, il termine, et il est totalement correct quand il fait les deux. Un cas limite est une donnée extrême admise par la précondition : liste vide, liste à un élément, cible absente, motif vide.

Quand l'utiliser : à chaque fonction que l'on devra prouver, avant d'écrire la moindre ligne de code. L'écriture d'une docstring et la syntaxe des assertions relèvent du thème Python : structures de contrôle et fonctions ; ce qui se joue ici est la précision de l'énoncé, car une postcondition vague ne se démontre pas.
1) Nommer les arguments avec des noms parlants, et dire de quel type et de quelle forme ils sont : « valeurs est une liste de nombres », « valeurs est triée par ordre croissant ».
2) Écrire la précondition : ce que l'on suppose sans le vérifier. Elle autorise à ne pas traiter certains cas, à condition de le dire.
3) Écrire la postcondition en une phrase qui commence par « Renvoie… » et qui caractérise le résultat sans ambiguïté. « Renvoie l'indice de cible » est incomplet : quel indice si la cible apparaît deux fois, que renvoyer si elle est absente ? Écrire plutôt « Renvoie le plus petit indice i tel que valeurs[i] == cible, et $-1$ si cible ne figure pas dans valeurs ».
4) Dire si la fonction modifie ses arguments. « Trie la liste valeurs en place » et « Renvoie une nouvelle liste triée » sont deux spécifications différentes ; une fonction qui trie en place ne renvoie rien.
5) Recopier la spécification dans la docstring, puis placer les assertions de précondition. La précondition devient alors une hypothèse utilisable dans la preuve : c'est elle qui autorisera à écrire « par précondition, $n \geq 1$ ».
6) Écrire enfin un jeu de tests : un cas usuel, un cas où la réponse cherchée est absente, et un cas limite par clause de la précondition. Ces tests cherchent les fautes ; ils ne démontrent rien, et c'est l'invariant qui démontrera.

Écrire une fonction qui renvoie le plus grand élément d'une liste de nombres. Spécifier la fonction, puis donner un jeu de tests.

La liste vide n'a pas de plus grand élément : je le mets en précondition, plutôt que de renvoyer une valeur arbitraire.

Spécification. Argument : valeurs, liste de nombres. Précondition : valeurs est non vide. Postcondition : la valeur renvoyée est un élément de valeurs supérieur ou égal à tous les éléments de valeurs. La liste n'est pas modifiée.

def maximum(valeurs):
    """Renvoie le plus grand élément de valeurs.
    Précondition : valeurs est une liste non vide de nombres."""
    assert len(valeurs) > 0
    plus_grand = valeurs[0]
    for i in range(1, len(valeurs)):
        if valeurs[i] > plus_grand:
            plus_grand = valeurs[i]
    return plus_grand

Jeu de tests, dont la construction méthodique relève du thème Python : modules, fichiers et tests ; il sert ici à éprouver la spécification, non à la remplacer. Cas usuel : maximum([4, 7, 2, 7, 9]) renvoie 9. Maximum atteint deux fois : la postcondition n'exige qu'une valeur, pas un indice, donc le doublon $7$ ne pose aucune question. Cas limite d'un seul élément : maximum([3]) renvoie 3, et la boucle ne fait aucun tour. Cas des nombres tous négatifs : maximum([-4, -7, -2]) renvoie -2, test qui détecte l'initialisation fautive à $0$. Cas interdit : maximum([]) déclenche l'assertion, ce qui est le comportement voulu.

À retenir : la spécification tranche les cas douteux avant le code, et le jeu de tests contient au moins un cas limite par clause de la précondition.

Quand l'utiliser : devant toute boucle while, et devant toute question « montrer que l'algorithme termine ». Une boucle for sur un range ou sur une liste que l'on ne modifie pas termine toujours : on le dit en une ligne, sans variant.
1) Repérer ce qui rapproche de la sortie : la quantité dont la condition dit qu'elle doit devenir nulle ou négative. C'est presque toujours elle, le variant : droite - gauche + 1 pour une dichotomie, reste pour une division répétée, j + 1 pour une descente d'indice.
2) Écrire « Posons $V = \ldots$ », avec une formule explicite en fonction des variables, pas une phrase.
3) Vérifier que $V$ est entier : différence d'indices, longueur, quotient de deux entiers par //. Si $V$ est un flottant, le théorème ne s'applique pas.
4) Vérifier que $V \geq 0$ tant que la condition est vraie, en se servant de la condition elle-même : « tant que gauche <= droite, on a $d - g + 1 \geq 1 > 0$ ».
5) Vérifier la décroissance stricte en examinant toutes les branches du corps : chacune doit faire diminuer $V$ d'au moins $1$. Une branche oubliée, et la preuve tombe.
6) Conclure : « $V$ est un entier naturel qui décroît strictement à chaque tour, donc la boucle termine », puis, si l'énoncé le demande, « et le nombre de tours est au plus $V_0 + 1$, avec $V_0 = \ldots$ », ce qui fournit du même coup une majoration de la complexité. Cette majoration brute est souvent très large : quand le variant est divisé par deux au lieu d'être diminué de $1$, on lui préfère le décompte fin, en majorant $V$ après $k$ tours, comme dans la rédaction modèle qui suit.

Montrer que la boucle de la fonction en_base ci-dessous termine, et majorer son nombre de tours.

def en_base(n, b):
    """Renvoie la liste des chiffres de n en base b,
    du plus significatif au moins significatif.
    Précondition : n entier positif ou nul, b entier supérieur ou égal à 2."""
    assert n >= 0 and b >= 2
    if n == 0:
        return [0]
    chiffres = []
    reste = n
    while reste > 0:
        chiffres.append(reste % b)
        reste = reste // b
    chiffres.reverse()
    return chiffres

Posons pour variant $V$ la valeur de la variable reste au début d'un tour.

$V$ est un entier : reste vaut $n$ au départ, qui est entier par précondition, et l'opérateur // appliqué à deux entiers renvoie un entier.

$V \geq 0$ tant que la condition est vraie : la condition reste > 0 donne directement $V \geq 1 > 0$.

Décroissance stricte : soit $r \geq 1$ la valeur de reste au début d'un tour. Le corps remplace reste par $\lfloor r / b \rfloor$. Comme $b \geq 2$, on a $\lfloor r/b \rfloor \leq r/b \leq r/2 < r$, la dernière inégalité étant stricte car $r \geq 1$. Le variant décroît donc, et comme il est entier, il décroît d'au moins $1$.

Les trois hypothèses du théorème du variant sont vérifiées, donc la boucle termine.

Majoration du nombre de tours : notons $r_k$ la valeur de reste au début du tour d'indice $k$, avec $r_0 = n$. L'inégalité $r_{k+1} \leq r_k / b$ donne par récurrence $r_k \leq n / b^k$. Or le tour d'indice $k$ n'a lieu que si $r_k \geq 1$, donc que si $b^k \leq n$, c'est-à-dire $k \leq \log_b n$. Le nombre de tours est donc au plus $\lfloor \log_b n \rfloor + 1$, et il vaut exactement ce nombre : c'est le nombre de chiffres de $n$ en base $b$.

À retenir : le variant se lit dans la condition d'arrêt, et la majoration qui prouve la terminaison donne le nombre de tours, donc la complexité.

Ligne fautive : « La quantité $x$ est positive et décroît strictement à chaque tour, donc la boucle while x > 0: x = x / 2 termine. »

C'est faux, et le théorème du variant ne s'applique pas, car il exige un variant entier. La suite de terme général $x_k = 2^{-k}$ est strictement décroissante et reste strictement positive : mathématiquement, la boucle ne s'arrête jamais. L'argument « une suite strictement décroissante et minorée finit par s'arrêter » n'est valable que dans $\mathbb{N}$, où une suite strictement décroissante d'entiers positifs est nécessairement finie ; dans $\mathbb{R}$, il est faux. Exécutée en Python en partant de x = 1.0, cette boucle s'achève pourtant après $1075$ tours, nombre qui dépend de la valeur initiale, parce qu'au-dessous d'un certain seuil la machine ne représente plus que $0$ : un arrêt obtenu pour une raison étrangère à la preuve, et qui ne démontre rien.

Version correcte : prendre un variant entier. Pour while x > 0: x = x // 2 avec x entier, le variant est x lui-même, entier naturel qui vérifie $\lfloor x/2 \rfloor < x$ dès que $x \geq 1$ ; la boucle termine.

Quand l'utiliser : dès qu'un énoncé demande de montrer qu'une fonction « renvoie bien » ce qu'annonce sa spécification, et systématiquement pour les algorithmes de recherche et de tri.
1) Écrire la postcondition visée. C'est le but, et l'invariant en sera la forme partielle.
2) Dérouler la trace de la boucle sur un exemple de quatre ou cinq éléments, en notant l'état des variables avant chaque test. L'invariant se lit dans cette colonne.
3) Énoncer l'invariant comme une propriété indexée par le compteur de tours : « Notons $P(i)$ la propriété : avant le tour d'indice $i$, … ». Y faire figurer tout ce qui servira à conclure, y compris ce qui paraît évident, par exemple « et valeurs est une permutation de la liste initiale » pour un tri.
4) Initialisation : vérifier $P$ avant le premier test, avec les valeurs d'initialisation. C'est souvent le cas d'un préfixe vide ou d'un intervalle plein.
5) Conservation : supposer $P(i)$ et la condition vraies, exécuter le corps ligne par ligne, et rétablir $P(i+1)$. Toutes les branches du if sont à traiter, sans en sauter une.
6) Sortie : écrire la valeur du compteur, ou la négation de la condition, à la sortie ; l'injecter dans l'invariant ; en déduire la postcondition. Si l'invariant ne suffit pas à conclure, c'est qu'il est trop faible : y ajouter ce qui manque, et refaire l'étape 5.
7) Traiter à part les sorties par return placées à l'intérieur de la boucle : à cet endroit précis, écrire pourquoi la valeur renvoyée vérifie la postcondition.

Montrer que la fonction maximum renvoie un élément de valeurs supérieur ou égal à tous les éléments de valeurs, pour toute liste non vide.

def maximum(valeurs):
    """Renvoie le plus grand élément de valeurs.
    Précondition : valeurs est une liste non vide de nombres."""
    assert len(valeurs) > 0
    plus_grand = valeurs[0]
    for i in range(1, len(valeurs)):
        if valeurs[i] > plus_grand:
            plus_grand = valeurs[i]
    return plus_grand

Notons $n$ la longueur de valeurs et $v_0, \dots, v_{n-1}$ ses éléments, que la fonction ne modifie pas. Par précondition, $n \geq 1$.

Terminaison : la boucle est un for sur range(1, n), qui effectue exactement $n - 1$ tours ; elle termine.

Invariant. Pour $i \in \{1, \dots, n\}$, notons $P(i)$ la propriété : avant le tour d'indice $i$, la variable plus_grand vaut $\max(v_0, \dots, v_{i-1})$.

Initialisation : avant le tour d'indice $1$, plus_grand vaut $v_0$, qui est bien le maximum de la famille réduite à $v_0$. Donc $P(1)$ est vraie.

Conservation : soit $i \in \{1, \dots, n-1\}$ tel que $P(i)$ soit vraie ; exécutons le tour d'indice $i$. Notons $m = \max(v_0, \dots, v_{i-1})$ la valeur de plus_grand au début de ce tour. Si $v_i > m$, le corps affecte $v_i$ à plus_grand, et $\max(v_0, \dots, v_i) = \max(m, v_i) = v_i$ : la nouvelle valeur est bien $\max(v_0, \dots, v_i)$. Sinon $v_i \leq m$, la variable n'est pas modifiée et vaut encore $m = \max(m, v_i) = \max(v_0, \dots, v_i)$. Dans les deux cas, $P(i+1)$ est vraie.

Sortie : la boucle s'arrête après le tour d'indice $n-1$, donc $P(n)$ est vraie, c'est-à-dire que plus_grand vaut $\max(v_0, \dots, v_{n-1})$.

Conclusion : la valeur renvoyée est le maximum de l'ensemble des éléments de valeurs ; c'est donc l'un d'eux, et il est supérieur ou égal à tous les autres. La fonction est totalement correcte relativement à sa spécification.

À retenir : l'invariant d'un parcours de liste dit ce que vaut l'accumulateur pour le préfixe déjà lu, et la sortie s'obtient en prenant pour préfixe la liste entière.

Énoncé : montrer que le tri par sélection trie la liste.

Invariant fautif proposé : « avant le tour d'indice $i$, la tranche valeurs[0:i] est triée par ordre croissant ».

Cet invariant est vrai et il se conserve, mais il ne permet pas de conclure. Il est en effet satisfait par l'état final [1, 2, 7] obtenu à partir de [7, 1, 2] comme par l'état final [1, 1, 1] : la tranche entière est triée dans les deux cas, et dans le second les valeurs ne sont plus celles du départ. Il manque deux choses : que la liste reste une permutation de la liste initiale, et que chaque élément placé le soit définitivement, c'est-à-dire soit inférieur ou égal à tous ceux qui restent. Un invariant se juge à ce qu'il entraîne à la sortie, non à sa vraisemblance.

Version correcte : « avant le tour d'indice $i$, la liste valeurs est une permutation de la liste initiale, la tranche valeurs[0:i] est triée par ordre croissant, et tout élément de valeurs[0:i] est inférieur ou égal à tout élément de valeurs[i:n] ». À la sortie, cet invariant donne une liste triée contenant exactement les éléments de départ.

Ligne fautive : « L'invariant de la recherche dichotomique est $d - g + 1$, qui décroît strictement, donc l'algorithme est correct. »

Deux confusions en une seule phrase. D'abord, un invariant est une propriété, quelque chose qui est vrai ou faux, tandis que $d - g + 1$ est un nombre : un nombre ne peut pas être vrai. Ensuite, ce nombre est le variant, et ce qu'il démontre n'est pas la correction mais la terminaison. Les deux outils ne répondent pas à la même question : le variant dit que l'algorithme s'arrête, l'invariant dit que ce qu'il renvoie alors est juste. Un algorithme peut parfaitement s'arrêter très vite en renvoyant une réponse fausse, comme la dichotomie appliquée à une liste non triée, qui termine toujours et se trompe.

Version correcte : nommer les deux, séparément et dans les mots qui conviennent. « Variant : $V = d - g + 1$, entier positif strictement décroissant, donc la boucle termine. Invariant : tout indice $i$ tel que $v_i = c$ vérifie $g \leq i \leq d$ ; à la sortie l'intervalle est vide, donc la cible est absente. » Deux paragraphes, deux conclusions différentes.

Propriété : soit $n \in \mathbb{N}$ et $b$ un entier supérieur ou égal à $2$. La fonction en_base renvoie la liste $[c_{m-1}, \dots, c_1, c_0]$ des chiffres de $n$ en base $b$, c'est-à-dire l'unique famille d'entiers vérifiant
$n = \sum_{t=0}^{m-1} c_t \, b^t, \qquad 0 \leq c_t \leq b-1, \qquad c_{m-1} \neq 0,$
à laquelle on ajoute la convention $[0]$ pour $n = 0$. Le nombre de tours de boucle, donc le nombre de chiffres, vaut $m = \lfloor \log_b n \rfloor + 1$ pour $n \geq 1$, et le coût est $\Theta(\log n)$ si l'on compte chaque opération arithmétique pour une opération élémentaire.

L'algorithme repose sur la division euclidienne répétée : le reste reste % b donne le chiffre des unités, le quotient reste // b est le nombre dont il reste à écrire les chiffres. Les chiffres sortent donc du moins significatif au plus significatif, ce que l'appel final à reverse corrige. L'invariant est l'égalité qui relie ce qui est déjà écrit à ce qui reste à traiter.

Montrer que la fonction en_base renvoie bien les chiffres de $n$ en base $b$.

Soient $n \geq 1$ et $b \geq 2$ (le cas $n = 0$ est traité à part par le if, qui renvoie [0]).

Notons, au début d'un tour de la boucle, $m$ la longueur de la liste chiffres, $c_0, \dots, c_{m-1}$ ses éléments dans leur ordre d'ajout, et $r$ la valeur de reste. Notons $P$ la propriété :
$n = \sum_{t=0}^{m-1} c_t \, b^t + r \, b^m \qquad \text{et} \qquad \forall t, \ 0 \leq c_t \leq b-1.$

Initialisation : avant le premier test, chiffres est vide et reste vaut $n$, donc $m = 0$, la somme est vide et l'égalité s'écrit $n = 0 + n \times b^0 = n$. La seconde clause porte sur une famille vide. Donc $P$ est vraie.

Conservation : supposons $P$ vraie au début d'un tour dont la condition reste > 0 est vraie, et notons $r \geq 1$ la valeur de reste. Le corps ajoute $c_m = r \bmod b$ à la liste, puis remplace reste par $r' = \lfloor r/b \rfloor$. On a $0 \leq c_m \leq b-1$ par définition du reste d'une division euclidienne par $b$, donc la seconde clause est conservée. Pour la première, la division euclidienne de $r$ par $b$ s'écrit $r = b \, r' + c_m$, donc
$\sum_{t=0}^{m} c_t \, b^t + r' \, b^{m+1} = \sum_{t=0}^{m-1} c_t \, b^t + c_m \, b^m + r' \, b^{m+1} = \sum_{t=0}^{m-1} c_t \, b^t + b^m \, (c_m + b \, r') = \sum_{t=0}^{m-1} c_t \, b^t + r \, b^m,$
qui vaut $n$ par hypothèse. Donc $P$ est vraie au début du tour suivant.

Sortie : la boucle a été prouvée terminante, et elle s'arrête avec reste $= 0$. L'invariant donne alors $n = \sum_{t=0}^{m-1} c_t b^t$ avec $0 \leq c_t \leq b-1$.

Chiffre de tête non nul : au dernier tour exécuté, la valeur $r$ de reste vérifiait $r \geq 1$ et $\lfloor r/b \rfloor = 0$, donc $1 \leq r \leq b-1$ et le chiffre ajouté valait $c_{m-1} = r \bmod b = r \geq 1$. Le premier chiffre écrit est donc non nul.

L'appel chiffres.reverse() retourne la liste : elle contient $c_{m-1}, \dots, c_0$, du plus significatif au moins significatif, ce qu'annonce la spécification. Sur en_base(2026, 16), la fonction renvoie [7, 14, 10], et l'on vérifie que $7 \times 256 + 14 \times 16 + 10 = 2026$.

À retenir : l'invariant d'un algorithme qui construit un résultat morceau par morceau est une égalité entre la donnée de départ d'une part, et la partie déjà construite plus la partie restante d'autre part.

Propriété : pour toute liste valeurs de longueur $n$ et toute valeur cible, la fonction ci-dessous renvoie le plus petit indice $i$ tel que $v_i =$ cible, et $-1$ si cible ne figure pas dans valeurs. Elle effectue au plus $n$ comparaisons, exactement $i + 1$ si la première occurrence est à l'indice $i$, et exactement $n$ si la cible est absente : son coût est $O(n)$ dans tous les cas, $\Theta(n)$ dans le pire des cas et $\Theta(1)$ dans le meilleur.

def recherche_sequentielle(valeurs, cible):
    """Renvoie le plus petit indice i tel que valeurs[i] == cible,
    et -1 si cible ne figure pas dans valeurs."""
    for i in range(len(valeurs)):
        if valeurs[i] == cible:
            return i
    return -1

Aucune hypothèse n'est faite sur valeurs : c'est le prix du coût linéaire, et c'est exactement ce que fait l'opérateur in sur une liste. Rappel hors ligne : $f = O(g)$ signifie qu'il existe $C > 0$ et un rang au-delà duquel $|f| \leq C |g|$, et $f = \Theta(g)$ que l'on a $f = O(g)$ et $g = O(f)$ (voir le thème Négligeabilité, domination et équivalents, bloc Analyse 2) ; le décompte des opérations élémentaires est traité dans le thème Complexité des algorithmes.

Quand l'utiliser : dès qu'une quantité se calcule en lisant la liste une fois et une seule, somme, produit, maximum, minimum, compteur, indice du meilleur élément, présence d'un élément.
1) Nommer l'accumulateur et dire ce qu'il représente : « somme contient la somme des éléments déjà lus », « plus_grand contient le maximum des éléments déjà lus ». Cette phrase est déjà l'invariant.
2) L'initialiser avec la valeur correspondant au préfixe vide ou au premier élément : $0$ pour une somme, $1$ pour un produit, $0$ pour un compteur, valeurs[0] pour un maximum. Ne jamais initialiser un maximum à $0$ : $0$ n'est pas une valeur du préfixe vide.
3) Choisir la forme du parcours. for v in valeurs si seule la valeur sert, for i in range(len(valeurs)) si l'indice sert, for i, v in enumerate(valeurs) si les deux servent (voir le thème Python : listes, tuples, chaînes et dictionnaires).
4) Écrire la mise à jour, une seule ligne par tour, de sorte que l'invariant soit rétabli pour le préfixe augmenté d'un élément.
5) Renvoyer l'accumulateur après la boucle, sans oublier return : une fonction qui affiche n'a rien renvoyé.
6) Traiter le cas limite de la liste vide : soit la précondition l'exclut avec une assertion, soit la valeur renvoyée est décidée et écrite dans la spécification.
7) Donner le coût : un parcours sans boucle imbriquée dont chaque tour coûte un nombre borné d'opérations est en $\Theta(n)$.

Écrire une fonction qui renvoie la moyenne d'une liste non vide de nombres, et une fonction qui renvoie le nombre d'éléments strictement supérieurs à cette moyenne. Prouver la première et donner le coût des deux.

def moyenne(valeurs):
    """Renvoie la moyenne arithmétique de valeurs.
    Précondition : valeurs est une liste non vide de nombres."""
    assert len(valeurs) > 0
    somme = 0
    for v in valeurs:
        somme = somme + v
    return somme / len(valeurs)


def au_dessus_de_la_moyenne(valeurs):
    """Renvoie le nombre d'éléments de valeurs strictement supérieurs
    à la moyenne de valeurs.
    Précondition : valeurs est une liste non vide de nombres."""
    assert len(valeurs) > 0
    m = moyenne(valeurs)
    compteur = 0
    for v in valeurs:
        if v > m:
            compteur = compteur + 1
    return compteur

Notons $n \geq 1$ la longueur de valeurs et $v_0, \dots, v_{n-1}$ ses éléments.

Terminaison de moyenne : la boucle for parcourt une liste qui n'est pas modifiée, donc elle effectue exactement $n$ tours et termine.

Invariant. Pour $i \in \{0, \dots, n\}$, notons $P(i)$ la propriété : avant le tour d'indice $i$, la variable somme vaut $\sum_{k=0}^{i-1} v_k$, somme vide et donc nulle pour $i = 0$.

Initialisation : avant le premier tour, somme vaut $0$, qui est la somme vide ; $P(0)$ est vraie.

Conservation : soit $i \in \{0, \dots, n-1\}$ tel que $P(i)$ soit vraie. Le tour d'indice $i$ lit $v = v_i$ et remplace somme par $\sum_{k=0}^{i-1} v_k + v_i = \sum_{k=0}^{i} v_k$. Donc $P(i+1)$ est vraie.

Sortie : après le dernier tour, $P(n)$ est vraie, donc somme vaut $\sum_{k=0}^{n-1} v_k$. La division par len(valeurs) $= n \geq 1$ est licite et la valeur renvoyée est $\frac{1}{n}\sum_{k=0}^{n-1} v_k$, qui est bien la moyenne arithmétique.

Coût : chaque tour effectue une addition et une affectation, en nombre borné d'opérations élémentaires, donc moyenne est en $\Theta(n)$. La fonction au_dessus_de_la_moyenne appelle moyenne une fois, puis effectue un second parcours de $n$ tours à coût borné : elle est en $\Theta(n) + \Theta(n) = \Theta(n)$.

À retenir : deux parcours successifs restent linéaires, et il faut appeler moyenne avant la boucle, une fois pour toutes : la rappeler dans le test la ferait recalculer à chaque tour et donnerait un coût $\Theta(n^2)$.

Ligne fautive : plus_grand = 0 avant une boucle qui cherche le maximum d'une liste.

Contre-exemple chiffré : sur [-4, -7, -2], aucune valeur n'est supérieure à $0$, la variable n'est jamais mise à jour, et la fonction renvoie 0, qui n'est même pas un élément de la liste. La postcondition « la valeur renvoyée est un élément de valeurs » est violée. La valeur $0$ est neutre pour la somme, pas pour le maximum : le maximum d'une famille vide est $-\infty$, qui ne s'écrit pas avec un entier. Même faute symétrique pour un minimum initialisé à $0$, ou à $100$ pour des notes.

Version correcte : initialiser avec le premier élément, plus_grand = valeurs[0], et faire partir la boucle de l'indice $1$ ; la liste vide est alors exclue par une précondition, assert len(valeurs) > 0, puisqu'elle n'a pas de plus grand élément.

Ligne fautive : return valeurs[i] à la place de return i, dans une recherche séquentielle spécifiée « renvoie le plus petit indice i tel que valeurs[i] == cible, et $-1$ si cible ne figure pas dans valeurs ».

La fonction ne répond plus à sa spécification, et le défaut n'est pas seulement formel : elle devient inexploitable. Contre-exemple exécuté sur [4, -1, 7], avec trois cibles : la cible $7$, qui figure dans la liste, donne 7 ; la cible $-1$, qui y figure aussi, donne -1 ; et la cible $5$, qui n'y figure pas, donne encore -1. Impossible de distinguer une réussite d'un échec sur les deux derniers appels. Renvoyer la valeur trouvée n'apprend d'ailleurs rien, puisque c'est la cible que l'on a fournie. La version correcte renvoie 2, 1 et -1 sur ces trois mêmes appels, dans cet ordre.

Version correcte : return i, et, pour rendre la sortie $-1$ légitime, dire dans la postcondition qu'elle signale l'absence, puisque $-1$ n'est jamais un indice valide de parcours. La même vigilance vaut dans l'autre sens : une fonction spécifiée « renvoie le plus grand élément » renvoie une valeur, pas indice_max, et deux spécifications voisines, « le maximum » et « l'indice du maximum », donnent deux fonctions différentes.

Propriété : si valeurs est une liste de longueur $n$ triée par ordre croissant, la fonction ci-dessous renvoie un indice $i$ tel que $v_i =$ cible, et $-1$ si cible ne figure pas dans valeurs. L'hypothèse « triée » est indispensable, et elle est en précondition : sur une liste quelconque, la fonction termine encore mais peut renvoyer $-1$ alors que la cible est présente.

def recherche_dichotomique(valeurs, cible):
    """Renvoie un indice i tel que valeurs[i] == cible,
    et -1 si cible ne figure pas dans valeurs.
    Précondition : valeurs est triée par ordre croissant."""
    gauche = 0
    droite = len(valeurs) - 1
    while gauche <= droite:
        milieu = (gauche + droite) // 2
        if valeurs[milieu] == cible:
            return milieu
        if valeurs[milieu] < cible:
            gauche = milieu + 1
        else:
            droite = milieu - 1
    return -1

L'invariant est l'intervalle des candidats : tout indice $i$ tel que $v_i =$ cible vérifie $g \leq i \leq d$. En cas de doublons, l'indice renvoyé n'est pas nécessairement le plus petit : la postcondition dit « un indice », pas « le premier ».

Propriété : sur une liste triée de longueur $n \geq 1$, la recherche dichotomique effectue au plus $\lfloor \log_2 n \rfloor + 1$ tours de boucle, et chaque tour n'examine qu'un seul élément de la liste, au prix d'une ou deux comparaisons avec cible ; son coût est $\Theta(\log n)$ dans le pire des cas et $\Theta(1)$ dans le meilleur, pour une complexité spatiale supplémentaire $\Theta(1)$. Le nombre de candidats $V = d - g + 1$ vaut $n$ au départ et est au moins divisé par deux à chaque tour. Pour $n = 10^6$, cela fait au plus $20$ tours, contre $10^6$ pour la recherche séquentielle : c'est le gain qui justifie de trier au préalable dès que l'on fait de nombreuses recherches dans la même liste.

Quand l'utiliser : le signal dans l'énoncé est « liste triée », « coût logarithmique », « en $O(\log n)$ », ou une recherche répétée dans une même liste. Plus largement, dès que l'on cherche un seuil dans une suite monotone : plus petit $i$ tel que $u_i \geq x$, racine d'une fonction croissante par dichotomie sur les indices.
1) Poser deux bornes qui délimitent les candidats restants, gauche = 0 et droite = len(valeurs) - 1, et écrire la convention : les candidats sont les indices de $g$ à $d$ inclus.
2) Écrire la condition de boucle cohérente avec cette convention : while gauche <= droite, car l'intervalle est vide si et seulement si $g > d$.
3) Calculer le milieu par milieu = (gauche + droite) // 2 : la division entière garantit $g \leq m \leq d$ dès que $g \leq d$.
4) Distinguer les trois cas, sans en fusionner deux : égalité, on renvoie ; élément trop petit, les candidats sont à droite, gauche = milieu + 1 ; élément trop grand, droite = milieu - 1. Les décalages de $1$ sont ce qui fait décroître le variant, ils ne sont pas facultatifs.
5) Écrire l'invariant : tout indice $i$ tel que $v_i =$ cible vérifie $g \leq i \leq d$. La conservation se démontre en utilisant l'hypothèse de tri, qui est le seul endroit où elle sert.
6) Écrire le variant $V = d - g + 1$, entier, positif tant que la condition est vraie, strictement décroissant dans les deux branches.
7) Conclure sur les trois points : terminaison par le variant, correction par l'invariant à la sortie et au return, coût en comptant les tours grâce à $V_{k+1} \leq V_k / 2$.
8) Tester sur les cas limites : liste vide, cible en première et en dernière position, cible absente plus petite que tout, plus grande que tout.

Soit valeurs une liste de $n$ nombres triée par ordre croissant. Montrer que recherche_dichotomique termine, qu'elle est correcte, et qu'elle effectue au plus $\lfloor \log_2 n \rfloor + 1$ tours de boucle.

Notons $v_0 \leq v_1 \leq \dots \leq v_{n-1}$ les éléments de valeurs, $c$ la valeur de cible, et $g_k$, $d_k$ les valeurs de gauche et droite au début du tour d'indice $k$. On a $g_0 = 0$ et $d_0 = n-1$.

Terminaison. Posons $V = d - g + 1$. C'est un entier, comme différence d'entiers. Tant que la condition gauche <= droite est vraie, $V \geq 1 > 0$. Dans ce cas, $m = \lfloor (g+d)/2 \rfloor$ vérifie $g \leq m \leq d$. Si le corps exécute gauche = milieu + 1, le nouveau variant vaut $d - m \leq d - g = V - 1$ ; s'il exécute droite = milieu - 1, il vaut $m - g \leq d - g = V - 1$. Dans les deux cas $V$ décroît d'au moins $1$. Le théorème du variant s'applique : la boucle termine.

Correction. Notons $P$ la propriété : tout indice $i \in \{0, \dots, n-1\}$ tel que $v_i = c$ vérifie $g \leq i \leq d$.

Initialisation : avant le premier test, $g = 0$ et $d = n-1$, donc tout indice de la liste convient ; $P$ est vraie.

Conservation : supposons $P$ vraie au début d'un tour dont la condition est vraie, et supposons que le corps n'exécute pas le return. Premier cas, $v_m < c$. Soit $i$ tel que $v_i = c$. Si l'on avait $i \leq m$, la croissance de la liste donnerait $v_i \leq v_m < c$, donc $v_i \neq c$, ce qui est exclu ; donc $i \geq m+1$. Comme $P$ donne déjà $i \leq d$, l'indice $i$ est bien dans le nouvel intervalle $\{m+1, \dots, d\}$. Second cas, $v_m > c$ : le même raisonnement avec $i \geq m$ donnerait $v_i \geq v_m > c$, donc $i \leq m-1$, et $i$ reste dans $\{g, \dots, m-1\}$. Dans les deux cas $P$ est conservée. C'est le seul endroit où sert l'hypothèse de tri.

Sortie par le return : la ligne return milieu n'est exécutée que si valeurs[milieu] == cible, et la valeur renvoyée est alors un indice $i$ tel que $v_i = c$ : la postcondition est vérifiée.

Sortie par la condition : la boucle s'arrête avec $g > d$, donc l'ensemble $\{g, \dots, d\}$ est vide. D'après $P$, aucun indice $i$ ne vérifie $v_i = c$, donc $c$ ne figure pas dans valeurs, et la fonction renvoie $-1$ : la postcondition est encore vérifiée.

La fonction est donc totalement correcte relativement à sa spécification.

Coût. Notons $V_k = d_k - g_k + 1$ et posons $V_0 = n$. En écrivant $d = g + V - 1$, on obtient $m - g = \lfloor (V-1)/2 \rfloor$ et $d - m = \lceil (V-1)/2 \rceil$, donc dans les deux branches $V_{k+1} \leq \lceil (V_k - 1)/2 \rceil \leq V_k / 2$. Par récurrence, $V_k \leq n / 2^k$. Or le tour d'indice $k$ n'a lieu que si $V_k \geq 1$, c'est-à-dire si $2^k \leq n$, soit $k \leq \log_2 n$. Le nombre de tours est donc au plus $\lfloor \log_2 n \rfloor + 1$. Chaque tour effectue un nombre borné d'opérations élémentaires, donc le coût est $O(\log n)$, atteint lorsque la cible est absente.

À retenir : les trois questions se traitent avec les trois mêmes objets, le variant pour la terminaison, l'invariant pour la correction, et la décroissance géométrique du variant pour le coût.

Ligne fautive : droite = milieu à la place de droite = milieu - 1, dans la branche où valeurs[milieu] > cible.

Contre-exemple exécuté : sur [2, 3, 5, 7] avec cible = 1, on a $g = 0$, $d = 3$, puis $m = 1$ et $v_1 = 3 > 1$, donc $d$ devient $1$ ; puis $m = 0$ et $v_0 = 2 > 1$, donc $d$ devient $0$ ; puis $m = 0$ de nouveau, et rien ne change : la boucle tourne indéfiniment. La raison se lit sur le variant : lorsque $g = d$, le milieu vaut $m = g = d$, et l'affectation droite = milieu laisse $V = d - g + 1$ égal à $1$. La décroissance stricte, troisième hypothèse du théorème du variant, est en défaut.

Version correcte : droite = milieu - 1, qui exclut l'indice milieu déjà testé et donne $V_{k+1} \leq V_k - 1$. La même faute symétrique, gauche = milieu, produit la même boucle infinie. Règle : avec la convention while gauche <= droite, les deux bornes se déplacent au-delà du milieu, jamais dessus.

Ligne fautive : appeler recherche_dichotomique(valeurs, cible) sur une liste dont rien ne garantit qu'elle est triée.

Contre-exemple exécuté : recherche_dichotomique([5, 1, 9], 5) renvoie $-1$, alors que $5$ figure bien dans la liste, à l'indice $0$. Le déroulement le montre : $m = 1$, $v_1 = 1 < 5$, donc on ne cherche plus qu'à droite et l'indice $0$ est perdu. La conservation de l'invariant utilise la croissance de la liste, et rien d'autre ; sans elle, l'élimination d'une moitié n'est pas justifiée. La fonction termine toujours, car le variant ne dépend pas du tri : c'est la correction qui tombe, pas la terminaison, et le résultat est faux en silence.

Version correcte : écrire l'hypothèse en précondition et s'y tenir, ou trier avant de chercher. Attention au coût : trier pour une seule recherche coûte $\Theta(n \log n)$, bien plus que la recherche séquentielle en $\Theta(n)$. Trier d'abord n'est rentable que si l'on effectue ensuite de nombreuses recherches dans la même liste.

Ligne fautive : « On vérifie sur [2, 3, 5, 7] que la fonction renvoie bien 2 pour la cible 5 : l'algorithme est donc correct. »

Un jeu de tests explore un nombre fini de données, alors que la postcondition est quantifiée sur toutes les listes et toutes les cibles : aucun nombre fini de tests réussis ne démontre un énoncé universel. Contre-exemple exécuté, sur la version fautive du piège précédent, celle qui écrit droite = milieu : pour la liste [2, 3, 5, 7], elle renvoie 2 pour la cible $5$, 0 pour $2$, 3 pour $7$ et 1 pour $3$. Quatre tests, quatre succès, et un lecteur pressé conclut. Avec la cible $1$, absente, la même fonction boucle indéfiniment. Le test qui aurait tout révélé est précisément celui auquel on n'a pas pensé.

Version correcte : démontrer, par un invariant pour la correction et un variant pour la terminaison, ce qui couvre toutes les données d'un coup. Les tests gardent leur rôle, mais l'autre : un seul test qui échoue réfute définitivement, alors que mille tests qui réussissent ne prouvent rien. On teste donc pour chercher les fautes, et l'on rédige ensuite la preuve pour établir qu'il n'y en a plus. Sur une copie, « on vérifie que » suivi d'un exemple ne vaut aucun point de correction.

Trier une liste $v_0, \dots, v_{n-1}$, c'est produire une permutation de ses éléments rangée par ordre croissant : la liste obtenue contient exactement les mêmes éléments, avec les mêmes multiplicités, et vérifie $v_0 \leq v_1 \leq \dots \leq v_{n-1}$. Les deux moitiés de cette postcondition comptent autant l'une que l'autre. Un tri est en place s'il modifie la liste reçue en n'utilisant qu'un nombre borné de variables auxiliaires, indépendant de $n$ : sa complexité spatiale supplémentaire est $\Theta(1)$. Un tri est stable si deux éléments de même clé restent dans leur ordre de départ, ce qui permet de trier par une clé après avoir trié par une autre. Un tri par comparaison n'accède aux éléments que par des tests du type $v_i \leq v_j$, sans rien supposer de leur nature.

Propriété : la fonction ci-dessous trie valeurs en place, par ordre croissant. Elle effectue exactement $\frac{n(n-1)}{2}$ comparaisons entre éléments et, pour $n \geq 1$, $n-1$ échanges, quelle que soit la liste de départ : son coût est $\Theta(n^2)$ dans le meilleur comme dans le pire des cas, pour une complexité spatiale supplémentaire $\Theta(1)$. Elle est en place, mais elle n'est pas stable.

def tri_selection(valeurs):
    """Trie la liste valeurs en place, par ordre croissant."""
    n = len(valeurs)
    for i in range(n - 1):
        indice_min = i
        for j in range(i + 1, n):
            if valeurs[j] < valeurs[indice_min]:
                indice_min = j
        valeurs[i], valeurs[indice_min] = valeurs[indice_min], valeurs[i]

Le principe tient en une phrase : chercher le plus petit élément de la partie non triée, et l'échanger avec le premier de cette partie. L'invariant porte sur le préfixe déjà construit : il est trié, et il ne bougera plus.

Quand l'utiliser : pour tout tri itératif, tri par sélection, tri par insertion, tri à bulles, et pour tout algorithme qui construit son résultat position par position.
1) Rappeler la postcondition en deux morceaux : la liste finale est croissante, et c'est une permutation de la liste initiale. Une preuve qui oublie le second morceau ne prouve rien, puisque la liste constante $0$ est croissante.
2) Poser l'invariant en trois clauses : valeurs est une permutation de la liste initiale ; la tranche valeurs[0:i] est triée ; et, pour un tri par sélection, tout élément de valeurs[0:i] est inférieur ou égal à tout élément de valeurs[i:n].
3) Initialisation : à $i = 0$ le préfixe est vide, donc trié, et rien n'a été échangé, donc la permutation est l'identité. Le dire, même si c'est bref.
4) Conservation : identifier la valeur placée au tour $i$, dire pourquoi elle est à sa place, et pourquoi les trois clauses sont rétablies. La clause de permutation se conserve parce que le corps ne fait que des échanges, ou des décalages suivis d'une réécriture de la valeur mise de côté.
5) Traiter la boucle interne à part, avec son propre invariant : pour le tri par sélection, « indice_min est l'indice d'un plus petit élément de valeurs[i:j] ».
6) Sortie : dire la valeur finale de $i$ et vérifier que l'invariant devient la postcondition. Pour le tri par sélection, $i = n-1$, et le dernier élément est bien à sa place grâce à la troisième clause.
7) Compter le coût en sommant le nombre de tours de la boucle interne, et donner le résultat en $\Theta$, pire et meilleur cas séparés si les deux diffèrent.

Montrer que tri_selection trie valeurs en place, et compter exactement le nombre de comparaisons qu'elle effectue.

Notons $n$ la longueur de valeurs et $L$ la liste initiale. Si $n \leq 1$, la boucle externe ne fait aucun tour et la liste, de longueur au plus $1$, est déjà triée. Supposons désormais $n \geq 2$.

Boucle interne. Fixons $i$ et notons $R(j)$, pour $j \in \{i+1, \dots, n\}$, la propriété : avant le tour d'indice $j$, indice_min est l'indice d'un plus petit élément de la tranche valeurs[i:j]. Initialisation : pour $j = i+1$, indice_min vaut $i$ et la tranche valeurs[i:i+1] se réduit à $v_i$. Conservation : si valeurs[j] < valeurs[indice_min], le nouvel indice_min est $j$ et $v_j$ est strictement plus petit que tous les éléments de valeurs[i:j] ; sinon indice_min ne change pas et son élément reste minimal, car $v_j$ ne lui est pas strictement inférieur. Dans les deux cas $R(j+1)$ est vraie. À la sortie, $R(n)$ donne : indice_min est l'indice d'un plus petit élément de valeurs[i:n].

Boucle externe. Notons $P(i)$, pour $i \in \{0, \dots, n-1\}$, la conjonction des trois propriétés suivantes, considérées avant le tour d'indice $i$ : (a) valeurs est une permutation de $L$ ; (b) la tranche valeurs[0:i] est triée par ordre croissant ; (c) tout élément de valeurs[0:i] est inférieur ou égal à tout élément de valeurs[i:n].

Initialisation : avant le tour d'indice $0$, la liste n'a pas été modifiée, donc (a) est vraie ; la tranche vide est triée, donc (b) est vraie ; (c) porte sur une famille vide, donc est vraie. Ainsi $P(0)$ est vraie.

Conservation : soit $i \in \{0, \dots, n-2\}$ tel que $P(i)$ soit vraie. D'après l'étude de la boucle interne, indice_min est l'indice d'un plus petit élément $m$ de valeurs[i:n]. Le corps échange valeurs[i] et valeurs[indice_min]. Un échange ne fait que permuter deux cases, donc (a) est conservée. Après l'échange, valeurs[i] vaut $m$. Comme $m$ minore valeurs[i:n] avant l'échange, et que l'échange ne fait que déplacer des éléments à l'intérieur de cette tranche, $m$ minore encore valeurs[i+1:n] : la clause (c) au rang $i+1$ est vraie pour l'élément $m$, et elle l'est pour les éléments de valeurs[0:i] car ils minoraient déjà valeurs[i:n] par (c) au rang $i$. Enfin valeurs[0:i+1] est triée : valeurs[0:i] l'est par (b), et son dernier élément est inférieur ou égal à $m$ par (c). Donc $P(i+1)$ est vraie.

Sortie : la boucle externe s'arrête après le tour d'indice $n-2$, donc $P(n-1)$ est vraie. La tranche valeurs[0:n-1] est triée et chacun de ses éléments est inférieur ou égal au dernier élément valeurs[n-1], donc la liste entière est triée ; et c'est une permutation de $L$. La fonction est correcte, et elle termine puisque ses deux boucles sont des for sur des range.

Coût. Pour chaque $i \in \{0, \dots, n-2\}$, la boucle interne effectue $n - 1 - i$ comparaisons, une par tour. Le total vaut
$\sum_{i=0}^{n-2} (n-1-i) = \sum_{k=1}^{n-1} k = \frac{n(n-1)}{2}.$
Ce nombre ne dépend pas du contenu de la liste : le tri par sélection coûte $\Theta(n^2)$ dans tous les cas, même sur une liste déjà triée. Il effectue en revanche seulement $n-1$ échanges, et n'utilise aucune mémoire auxiliaire dépendant de $n$.

À retenir : l'invariant d'un tri a toujours une clause de permutation, et la clause (c) est celle qui permet de conclure que le préfixe ne bougera plus.

Propriété : la fonction ci-dessous trie valeurs en place, par ordre croissant. Elle est stable, sa complexité spatiale supplémentaire est $\Theta(1)$, et, pour $n \geq 1$, son nombre de comparaisons vaut $n-1$ dans le meilleur des cas, atteint lorsque la liste est déjà triée, et $\frac{n(n-1)}{2}$ dans le pire des cas, atteint lorsque la liste est strictement décroissante : le coût est $\Theta(n)$ dans le meilleur des cas et $\Theta(n^2)$ dans le pire.

def tri_insertion(valeurs):
    """Trie la liste valeurs en place, par ordre croissant."""
    for i in range(1, len(valeurs)):
        x = valeurs[i]
        j = i - 1
        while j >= 0 and valeurs[j] > x:
            valeurs[j + 1] = valeurs[j]
            j = j - 1
        valeurs[j + 1] = x

C'est le tri du joueur de cartes : chaque nouvel élément est inséré à sa place dans la main déjà triée, les plus grands se décalant d'un cran. Contrairement au tri par sélection, il est adaptatif : son coût s'effondre sur une liste presque triée, ce qui en fait le tri quadratique à retenir.

Montrer que tri_insertion trie valeurs en place, puis déterminer son nombre de comparaisons dans le meilleur et dans le pire des cas.

Notons $n$ la longueur de valeurs et $L$ la liste initiale.

Terminaison. La boucle externe est un for sur range(1, n). La boucle interne admet pour variant $V = j + 1$ : c'est un entier ; tant que la condition est vraie on a $j \geq 0$, donc $V \geq 1 > 0$ ; et le corps remplace $j$ par $j - 1$, donc $V$ décroît de $1$ exactement. Les deux boucles terminent.

Invariant externe. Notons $P(i)$, pour $i \in \{1, \dots, n\}$, la propriété : avant le tour d'indice $i$, valeurs est une permutation de $L$ et la tranche valeurs[0:i] est triée par ordre croissant.

Initialisation : avant le tour d'indice $1$, rien n'a été modifié et la tranche valeurs[0:1], d'un seul élément, est triée. Donc $P(1)$ est vraie.

Conservation. Soit $i \in \{1, \dots, n-1\}$ tel que $P(i)$ soit vraie. Notons $w_0 \leq w_1 \leq \dots \leq w_{i-1}$ le contenu de valeurs[0:i] au début du tour et $x =$ valeurs[i]. Pour la boucle interne, notons $Q(j)$ la propriété : valeurs[0:j+1] contient $w_0, \dots, w_j$, la tranche valeurs[j+2:i+1] contient $w_{j+1}, \dots, w_{i-1}$ dans cet ordre, et tous ces éléments sont strictement supérieurs à $x$.

$Q(i-1)$ est vraie au premier test : valeurs[0:i] contient $w_0, \dots, w_{i-1}$ et la tranche valeurs[i+1:i+1] est vide, donc la dernière clause porte sur une famille vide.

Conservation de $Q$ : si $j \geq 0$ et $w_j > x$, le corps recopie $w_j$ dans la case $j+1$ et décrémente $j$ ; la tranche valeurs[j+1:i+1] contient alors $w_j, w_{j+1}, \dots, w_{i-1}$, tous strictement supérieurs à $x$ puisque $w_j > x$ est précisément la condition. Donc $Q(j-1)$ est vraie.

Sortie de la boucle interne : elle a lieu pour une valeur $j_0$ telle que $j_0 = -1$, ou $j_0 \geq 0$ et $w_{j_0} \leq x$. L'affectation valeurs[j + 1] = x donne alors pour valeurs[0:i+1] la suite
$w_0, \dots, w_{j_0}, \ x, \ w_{j_0+1}, \dots, w_{i-1}.$
C'est une permutation du contenu précédent de valeurs[0:i+1], donc valeurs reste une permutation de $L$. Elle est croissante : les $w_k$ pour $k \leq j_0$ sont croissants et majorés par $w_{j_0} \leq x$ lorsque $j_0 \geq 0$ ; et $x$ est strictement inférieur à $w_{j_0+1}, \dots, w_{i-1}$ d'après $Q(j_0)$, ces derniers étant eux-mêmes croissants. Donc $P(i+1)$ est vraie.

Sortie : $P(n)$ donne une liste triée qui est une permutation de $L$. La fonction est totalement correcte.

Stabilité. La condition d'arrêt est valeurs[j] > x, avec une inégalité stricte : la descente s'arrête dès qu'elle rencontre un élément égal à $x$, et $x$ est déposé juste après lui. Deux éléments de même clé conservent donc leur ordre de départ.

Coût. Au tour d'indice $i$, la boucle interne effectue au moins une comparaison et au plus $i$. Si la liste est déjà triée, la première comparaison échoue à chaque tour, d'où $\sum_{i=1}^{n-1} 1 = n-1$ comparaisons. Si la liste est strictement décroissante, la descente va jusqu'à $j = -1$ à chaque tour, d'où $\sum_{i=1}^{n-1} i = \frac{n(n-1)}{2}$ comparaisons. Le coût est donc $\Theta(n)$ dans le meilleur des cas et $\Theta(n^2)$ dans le pire.

À retenir : la boucle interne d'un tri par insertion se prouve avec son propre invariant, qui décrit le trou laissé par la valeur mise de côté, et l'inégalité stricte du test est exactement ce qui rend le tri stable.

Propriété : si tous les éléments de valeurs sont des entiers de l'intervalle $\{0, \dots, k\}$, la fonction ci-dessous renvoie la liste triée de ces éléments, en $\Theta(n + k)$ opérations et avec $\Theta(n + k)$ cases de mémoire supplémentaire : $k+1$ cases pour les effectifs, et $n$ cases pour la liste renvoyée, qui n'est pas la liste reçue. L'hypothèse sur les valeurs est essentielle : hors de $\{0, \dots, k\}$, l'accès effectifs[v] est hors bornes ou compte au mauvais endroit.

def tri_comptage(valeurs, k):
    """Renvoie la liste triée des éléments de valeurs.
    Précondition : tout élément de valeurs est un entier
    de l'intervalle [0, k]."""
    effectifs = [0] * (k + 1)
    for v in valeurs:
        effectifs[v] = effectifs[v] + 1
    triee = []
    for v in range(k + 1):
        for _ in range(effectifs[v]):
            triee.append(v)
    return triee

Ce tri n'effectue aucune comparaison entre éléments : il se sert des valeurs comme d'indices. Il n'est pas en place, et il n'est intéressant que si $k$ est du même ordre que $n$ : pour $n = 10$ et $k = 10^9$, il est ruineux.

Montrer que tri_comptage renvoie la liste triée des éléments de valeurs, et donner son coût.

Notons $n$ la longueur de valeurs et $v_0, \dots, v_{n-1}$ ses éléments, tous entiers dans $\{0, \dots, k\}$ par précondition.

Première boucle. Notons $P(i)$ la propriété : avant le tour d'indice $i$, pour tout $u \in \{0, \dots, k\}$, effectifs[u] vaut le nombre d'indices $t < i$ tels que $v_t = u$. Initialisation : avant le premier tour, la liste effectifs ne contient que des zéros, et aucun indice $t < 0$ n'existe. Conservation : le tour d'indice $i$ lit $v_i$, qui appartient à $\{0, \dots, k\}$ par précondition, donc l'accès est licite ; il ajoute $1$ à la seule case d'indice $v_i$, ce qui met à jour le compte pour $u = v_i$ et ne change rien pour les autres. À la sortie, $P(n)$ donne : pour tout $u$, effectifs[u] est le nombre d'occurrences de $u$ dans valeurs.

Seconde boucle. Elle ajoute à triee la valeur $u$ exactement effectifs[u] fois, pour $u$ parcourant $0, 1, \dots, k$ dans cet ordre croissant. La liste obtenue contient donc, pour chaque $u$, autant d'occurrences de $u$ que valeurs : c'est une permutation de valeurs. Et elle est croissante, puisque les valeurs y sont ajoutées par ordre croissant de $u$, chaque paquet étant constitué de valeurs égales. La postcondition est donc vérifiée.

Coût. La création de effectifs coûte $\Theta(k)$. La première boucle effectue $n$ tours à coût borné, soit $\Theta(n)$. La seconde boucle exécute $k+1$ tours externes, et le nombre total de tours internes est $\sum_{u=0}^{k} \texttt{effectifs}[u] = n$ ; son coût est donc $\Theta(k + n)$. Au total, $\Theta(n + k)$ en temps, et $\Theta(n + k)$ en espace supplémentaire : $k+1$ cases pour la liste des effectifs, et $n$ cases pour la liste renvoyée.

À retenir : le coût d'une boucle doublement imbriquée ne se majore pas toujours par le produit des deux bornes ; ici, la somme des tours internes est connue et vaut $n$, ce qui fait tomber le coût à une somme au lieu d'un produit.

Théorème : soit $A$ un algorithme de tri qui n'accède aux éléments que par des comparaisons deux à deux. Alors, sur des entrées de $n$ éléments deux à deux distincts, $A$ effectue dans le pire des cas au moins $\log_2(n!)$ comparaisons, et l'on a $\log_2(n!) \geq \frac{n}{2}\log_2\frac{n}{2}$ pour $n \geq 2$ : le coût de $A$ est donc $\Omega(n \log n)$. Aucune ruse d'écriture ne fera descendre un tri par comparaison sous cette barre. Le tri fusion, en $\Theta(n \log n)$ (voir le thème Récursivité et diviser pour régner), l'atteint donc à une constante multiplicative près : il est optimal. Les tris par sélection et par insertion, en $\Theta(n^2)$ dans le pire des cas, en sont loin. La borne ne s'applique qu'aux tris par comparaison : le tri par comptage, qui utilise les valeurs comme indices, la contourne sans la contredire.