La discipline de programmation

(a) Syntaxe : il manque le deux-points après def double(x) — l'interpréteur refuse le fichier avant toute exécution. Correction : def double(x):.

(b) Exécution : t[3] lève IndexError, car les indices valides d'une liste de longueur $3$ sont $0$, $1$, $2$. Correction : t[2] pour le dernier élément (ou t[-1]).

(c) Logique : n 2 calcule le double, pas le carré ; le programme s'exécute sans erreur et rend un résultat faux — seul un test comme assert carre(3) == 9 le révèle. Correction : n n (ou n ** 2). (La hiérarchie du danger est croissante : (a) est signalée immédiatement, (b) à l'exécution, (c) jamais.)

def occurrences(v, t: list) -> int:
    """Renvoie le nombre d'indices i tels que t[i] == v.

    Précondition : t est une liste (éventuellement vide).
    Postcondition : le résultat c vérifie 0 <= c <= len(t),
    et c est exactement le cardinal de {i : t[i] == v}.
    """

Trois points méritent attention : la liste vide est admise (et donnera $0$) ; la postcondition encadre le résultat ($0\le c\le n$), ce qui fournira plus tard un test de propriété gratuit ; et rien n'est dit du parcours — le contrat reste muet sur le comment. (Savoir s'arrêter là est tout l'exercice : la spécification est un livrable en soi.)

assert dernier_indice(3, [3, 1, 3, 2]) == 2    # présent plusieurs fois : le DERNIER
assert dernier_indice(2, [3, 1, 3, 2]) == 3    # présent en dernière position
assert dernier_indice(3, [3]) == 0             # liste à un élément
assert dernier_indice(7, [3, 1, 2]) is None    # absent
assert dernier_indice(7, []) is None           # liste vide
assert dernier_indice(5, [5, 5, 5]) == 2       # tous égaux

Le premier test est le plus discriminant : il sépare dernier_indice de indice (une implémentation qui renverrait le premier indice échouerait ici et seulement ici). Un bon jeu de tests contient toujours au moins un cas qui distingue la spécification visée de sa voisine la plus proche. (Les tests 2 et 3 traquent les erreurs de bornes, les tests 4 à 6 les cas limites du contrat.)

Personne n'a raison, ni tort : la spécification est ambiguë. Pour $x=2,5$, les deux entiers $2$ et $3$ sont à égale distance — « l'entier le plus proche » n'existe pas. Le contrat doit trancher la règle des demi-entiers. Par exemple :

def arrondi(x: float) -> int:
    """Renvoie l'entier n minimisant |x - n| ; en cas d'égalité
    (x demi-entier), renvoie le plus GRAND des deux candidats.

    Postcondition : |x - arrondi(x)| <= 0.5.
    """

assert arrondi(2.3) == 2 and arrondi(2.7) == 3   # cas nominaux
assert arrondi(2.5) == 3                          # demi-entier : la règle choisie
assert arrondi(-2.5) == -2                        # demi-entier négatif (le plus grand !)
assert arrondi(4.0) == 4                          # déjà entier

Le test arrondi(-2.5) == -2 est subtil : « le plus grand » de $-3$ et $-2$ est $-2$. Une moitié des bogues d'arrondi du monde réel vit dans les négatifs. (Leçon : un désaccord entre deux implémentations « correctes » signale presque toujours un trou dans la spécification — c'est elle qu'il faut corriger d'abord.)

Posons comme variant la valeur de $b$. Tant que la boucle s'exécute, $b>0$ (condition d'entrée) : le variant est positif. À chaque tour, le nouveau $b$ vaut $a\mathrm{mod}b$, qui appartient à $[[0,b-1]]$ par définition du reste : le variant décroît strictement. Une suite strictement décroissante d'entiers positifs étant finie, la boucle termine. (Noter que $a$, lui, ne décroît pas nécessairement au premier tour — si $a<b$, le tour initial échange les deux valeurs. C'est bien $b$ et lui seul qu'il faut choisir. La correction, elle, repose sur l'invariant $\mathrm{pgcd}(a,b)=\mathrm{pgcd}(a_0,b_0)$, conséquence de $\mathrm{pgcd}(a,b)=\mathrm{pgcd}(b,a\mathrm{mod}b)$ — l'identité d'Euclide vue en mathématiques.)

Invariant ${\mathcal{I}}_i$ : « au début du tour d'indice $i$, $m$ est le maximum de $t[\mathrm{0..}i-1]$ » (c'est-à-dire : $m\in \{t[0],\dots ,t[i-1]\}$ et $m\ge t[j]$ pour tout $j<i$).

Initialisation ($i=1$) : $m=t[0]$ est bien le maximum du préfixe $t[\mathrm{0..0}]$. ✓

Conservation : supposons ${\mathcal{I}}_i$ vraie. Deux cas. Si $t[i]>m$, alors $t[i]$ majore $m$, donc tous les $t[j]$, $j<i$ : après m = t[i], $m$ est le maximum de $t[\mathrm{0..}i]$. Sinon, $t[i]\le m$ et $m$ reste le maximum de $t[\mathrm{0..}i]$. Dans les deux cas, ${\mathcal{I}}_{i+1}$ est vraie. ✓

Conclusion : à la sortie ($i=n$), $m$ est le maximum de $t[\mathrm{0..}n-1]$ tout entier : la postcondition est prouvée — y compris l'appartenance $m\in t$, que le maximum_faux du cours violait. (L'invariant dit exactement « le travail déjà fait est juste » ; la preuve se réduit alors à vérifier le dernier geste.)

La postcondition a deux clauses — triée et mêmes éléments — qu'on vérifie séparément :

def verifie(t: list, r: list) -> bool:
    """r est-il un tri acceptable de t ?"""
    croissante = all(r[i] <= r[i + 1] for i in range(len(r) - 1))
    memes_elements = sorted(t) == sorted(r)
    return croissante and memes_elements

import random
for essai in range(1000):
    t = [random.randint(-50, 50) for _ in range(random.randint(0, 30))]
    assert verifie(t, tri(t)), f"echec sur {t}"

Le message d'échec affiche l'entrée fautive (forme exigible : assert nu ; message et f-string sont des commodités hors annexe). Mille entrées aléatoires exercent plus de situations qu'aucun jeu de tests manuel — et la clause memes_elements attrape le bogue classique du tri qui perd ou duplique des éléments, invisible si l'on ne vérifie que la croissance. (Oublier la seconde clause est l'erreur canonique : la liste [1, 1, 1] est parfaitement triée, quelle que soit l'entrée… Le test de propriété teste le contrat entier, pas sa moitié facile.)

Le piège : $n$ augmente aux tours impairs, ce n'est donc pas un variant. Mais regardons deux tours : si $n$ est impair (et $n\ne 1$, donc $n\ge 3$), le tour suivant donne $n+1$, pair, puis $(n+1)/2\le n-1<n$. Si $n$ est pair, un seul tour donne $n/2<n$. Ainsi la quantité $n$ décroît strictement au bout d'au plus deux tours : formellement, $v=2n+(n\mathrm{mod}2)$ est un variant qui décroît strictement à chaque tour (vérification : pour $n$ pair, $v$ passe de $2n$ à $\le n+1$ ; pour $n$ impair, de $2n+1$ à $2n+2$… non : à $2(n+1)=2n+2>2n+1$ — ce candidat échoue !). Reprenons : le bon variant est $v=3n+(n\mathrm{mod}2)$ : pour $n$ pair, $v=3n\to 3n/2+(n/2\mathrm{mod}2)\le 3n/2+1<3n$ dès $n\ge 1$ ; pour $n$ impair, $v=3n+1\to 3(n+1)=3n+3>3n+1$ — échec encore. La leçon est qu'un variant par tour n'existe pas toujours sous forme simple : on raisonne alors par paquets de tours. La mesure $n$ décroît strictement tous les deux tours au plus, et reste $\ge 1$ : la suite des valeurs de $n$ observées tous les deux tours est strictement décroissante dans ${\mathbb{N}}^{\ast }$, donc finie — la boucle termine, en au plus $2\lceil {\log }_{2}n\rceil +O(1)$ tours.

Avec n = 3 n + 1, on obtient la suite de Syracuse : la terminaison pour tout $n$ est une conjecture ouverte depuis près d'un siècle — personne ne sait exhiber de variant, et personne n'a trouvé de contre-exemple. (Double moralité : prouver la terminaison peut exiger de l'invention — paquets de tours, mesures composées — et il existe des boucles de quatre lignes dont la terminaison dépasse l'état actuel des mathématiques. Le variant n'est pas une formalité.)*

1. Spécification puis implémentation.

def renverse(t: list) -> list:
    """Renvoie une nouvelle liste r de même longueur que t,
    telle que r[i] == t[n - 1 - i] pour tout i (n = len(t)).
    La liste t n'est pas modifiée."""
    r = []
    for i in range(len(t)):
        # Invariant : r == [t[n-1], t[n-2], ..., t[n-i]]  (les i derniers, renversés)
        r.append(t[len(t) - 1 - i])
    return r

2. Jeu de tests.

assert renverse([1, 2, 3]) == [3, 2, 1]      # nominal
assert renverse([]) == []                     # vide
assert renverse([7]) == [7]                   # un élément
assert renverse([1, 2, 2]) == [2, 2, 1]       # doublons
t = [1, 2, 3]; renverse(t)
assert t == [1, 2, 3]                         # t non modifiée (clause du contrat !)

3. Preuve. Invariant ${\mathcal{I}}_i$ : « au début du tour $i$, $r=[t[n-1],\dots ,t[n-i]]$ » (liste vide pour $i=0$). Initialisation : $r=[]$. ✓ Conservation : si ${\mathcal{I}}_i$ tient, le tour ajoute $t[n-1-i]$ en queue, donnant $r=[t[n-1],\dots ,t[n-i],t[n-1-i]]$, soit ${\mathcal{I}}_{i+1}$. ✓ À la sortie ($i=n$) : $r=[t[n-1],\dots ,t[0]]$, c'est-à-dire $r[i]=t[n-1-i]$ pour tout $i$ — la postcondition. La clause « $t$ non modifiée » tient car le corps ne contient aucune écriture dans $t$. (Le déroulé complet — contrat, code, tests, preuve — est le geste professionnel que ce cours installera comme un réflexe ; l'avant-dernier test, souvent oublié, vérifie une clause du contrat qui ne se voit pas dans le résultat renvoyé.)

Les flottants sont des approximations binaires : ni $0,1$ ni $0,2$ ne sont représentables exactement en base $2$, et la machine calcule

>>> (0.1 + 0.2) / 2
0.15000000000000002

L'égalité stricte == entre flottants issus de calculs est donc un test trop fragile : il peut échouer sur du code juste (ici) comme réussir sur du code faux (compensation accidentelle d'erreurs). La bonne pratique est la comparaison à tolérance :

assert abs(moyenne([0.1, 0.2]) - 0.15) < 1e-12

Règle générale : dans un jeu de tests numérique, on réserve == aux entiers, aux booléens et aux résultats exacts par nature (longueurs, indices, comptages) ; toute comparaison de flottants calculés passe par un écart absolu abs(a - b) < eps (ou relatif pour les grandes valeurs). (Ce phénomène n'est pas un défaut de Python : c'est l'arithmétique IEEE 754, partagée par tous les langages — on le retrouvera chaque fois que l'informatique calcule sur le continu.)