Prouver et analyser : la boîte à outils formalisée

x + 1 : expression, pure. x = x + 1 : instruction (l'affectation), effet sur l'état local. t.append(3) : techniquement une expression (un appel, qui vaut None) utilisée comme instruction — effet de bord sur la liste $t$. len(t) == 0 : expression, pure. print("ok") : appel valant None, effet de bord (écriture à l'écran). return x : instruction (contrôle du flot). (La frontière subtile : un appel de fonction est toujours une expression, mais sa valeur peut être inintéressante — None — et son intérêt tout entier dans l'effet de bord. D'où le bogue classique t = t.append(3), qui affecte None à t : la liste est perdue.)

Précondition : $n\ge 0$ (entier). Invariant $\mathcal{I}$ : $s=k^2$ (la somme des $k$ premiers impairs $1+3+\cdots +(2k-1)$ vaut $k^2$). Initialisation : $s=0=0^2$. ✓ Conservation : si $s=k^2$, alors $s+2k+1=k^2+2k+1=(k+1{)}^2$, et $k$ devient $k+1$ : l'invariant suit. ✓ Sortie : $\mathcal{I}\wedge \neg (k<n)$ donne $k=n$ (car $k$ croît de $1$ depuis $0$ : il atteint $n$ exactement) et $s=n^2$. Postcondition : la fonction renvoie $n^2$. Variant : $v=n-k$, entier, positif pendant la boucle, décroît de $1$ par tour. ✓ La fonction calcule le carré par additions — totalement correcte. (L'invariant $s=k^2$ ne se devine pas en relisant le code ligne à ligne : on le trouve en exécutant à la main — $s=1,4,9$ — puis en conjecturant ; la preuve transforme ensuite la conjecture en certitude. Démarche expérimentale, conclusion mathématique.)

Classes issues de la spécification : élément présent / absent. Classes issues de la structure : présent trouvé au premier milieu / après descente à gauche / après descente à droite ; absent plus petit que tout / plus grand que tout / entre deux éléments. Classes de taille : tableau vide (zéro tour), singleton (un tour), taille générale. Limites : présent en première position, en dernière position, au milieu exact ; doublons (toutes occurrences identiques).

Le jeu de tests : un représentant par case — c'est, à l'ordre près, exactement le « jeu canonique » du chapitre 5 : présent(milieu, première, dernière), absent(avant, après, entre), vide, singleton $\times$ (présent, absent), tous égaux. (Ce qui était au chapitre 5 une liste apprise devient une méthode : le canonique n'était pas un catalogue arbitraire, c'était le partitionnement — désormais, on sait le reconstruire pour n'importe quelle fonction.)

Affichage : [0.5, 0.75, 1.0] — les notes brutes ont disparu. normalise écrit dans la liste reçue (effet de bord) tout en renvoyant cette même liste : l'hybride non documenté du cours. L'appelant, voyant un return, croit légitimement la source préservée.

Correction pure : construire une liste neuve — return [x / m for x in notes] ; brutes reste intacte, le return dit vrai. Correction « effet assumé » : garder la mutation, supprimer le return (renvoyer None) et documenter « modifie notes en place » — la convention de list.sort. (Le choix entre les deux est un choix de conception à expliciter — troisième compétence du programme ; le crime n'est ni la pureté ni la mutation, c'est l'ambiguïté.)

(a) Correction partielle : l'unique sortie est le return i, gardé par le test all(t[i] >= x ...) — si la fonction s'arrête, l'indice renvoyé majore tous les éléments : postcondition garantie par construction. Non-terminaison possible : rien n'oblige le tirage à atteindre un indice de maximum — la suite de tirages $0,0,0,\dots$ (improbable mais possible) boucle sans fin sur un tableau dont le maximum est ailleurs. Aucun variant n'existe : aucune quantité ne décroît à coup sûr. (On dit que l'algorithme termine presque sûrement — notion du cours de probabilités, hors de notre définition de terminaison, qui exige l'arrêt pour toute exécution.)

(b) L'exemple minimal : def maximum(t): return t[0] avec la postcondition « renvoie le maximum ». Termine toujours (aucune boucle), faux dès que le maximum n'est pas en tête : terminaison sans correction partielle. (Les deux moitiés de la correction totale sont bien indépendantes — chacune peut exister sans l'autre, et chacune a son outil.)

Classes structurelles : effectif impair (un élément central) / pair (moyenne de deux). Limites de taille : $n=1$ ($\to t[0]$) ; $n=2$ ($\to$ moyenne des deux). Classes de valeurs : éléments tous égaux ($\to$ cette valeur) ; doublons autour du centre ($[1,2,2,3]\to 2.0$) ; valeurs non triées en entrée (vérifier que la fonction trie bien : $[3,1,2]\to 2$) ; et la classe oubliée : la médiane d'un effectif pair peut ne pas appartenir au tableau — $[1,2]\to 1,5$, de type flottant alors que les entrées sont entières. Jeu de tests :

assert mediane([5]) == 5
assert mediane([1, 2]) == 1.5            # la classe oubliée : résultat HORS tableau
assert mediane([3, 1, 2]) == 2           # entrée non triée
assert mediane([1, 2, 2, 3]) == 2.0
assert mediane([4, 4, 4, 4]) == 4.0
assert mediane([2, 1]) == 1.5            # pair, non trié

(Le test $[1,2]\to 1,5$ attrape deux familles de bogues réels : la division entière // utilisée par erreur — qui rendrait $1$ — et la confusion « la médiane est un élément du tableau ». Les classes oubliées sont presque toujours celles où le type ou la provenance du résultat change.)

Trois sources d'espace à inventorier systématiquement : les structures auxiliaires (les listes du tri fusion), la pile de récursion (un contexte par appel en attente — chapitre 6), et le résultat lui-même quand il est volumineux (les $2^n$ sous-listes : aucune implémentation ne fera mieux, l'espace est dans la spécification). (Pour le tri fusion, une subtilité honnête : les tranches t[:m] créent elles aussi des copies — l'implémentation du chapitre 9 est $O(n)$ d'espace au total grâce à la libération au fil des fusions, mais $O(n\log n)$ si l'on retenait tout ; les analyses d'espace exigent de savoir quand la mémoire se libère, ce qui les rend plus délicates que celles de temps.)

Invariant $\mathcal{I}$ — le tableau est partagé en quatre zones :

$$\underset{\text{que des }0}{\underbrace{t[\mathrm{0..}g-1]}}\left|\underset{\text{que des }1}{\underbrace{t[g..i-1]}}\right|\underset{\text{inconnu}}{\underbrace{t[i..d]}}|\underset{\text{que des }2}{\underbrace{t[d+\mathrm{1..}n-1]}}$$

Initialisation : $g=i=0$, $d=n-1$ — les trois zones connues sont vides, tout est inconnu. ✓

Conservation, cas par cas. Si $t[i]=0$ : l'échange avec $t[g]$ ramène ce $0$ en bout de zone-0 ; la case $t[g]$ échangée était soit un $1$ (zone-1 non vide : son premier élément), soit la case $i$ elle-même ($g=i$) — dans les deux cas, après g += 1; i += 1, les zones 0 et 1 sont correctes. Si $t[i]=2$ : l'échange l'envoie en bout de zone-2 et $d$ recule ; mais la valeur reçue de $t[d]$ est inconnue — c'est pourquoi i ne bouge pas : la case $i$ doit être réexaminée au tour suivant (l'incrémenter laisserait passer un $0$ ou un $2$ non classé : le bogue classique de cet algorithme, que l'invariant interdit noir sur blanc). Si $t[i]=1$ : il prolonge la zone-1, $i$ avance. ✓

Sortie : $i>d$ — la zone inconnue est vide ; les quatre zones se réduisent à $0\dots 01\dots 12\dots 2$ : trié, et seules des transpositions ont eu lieu : permutation. ✓

Variant : $v=d-i+1$ (la taille de la zone inconnue) — positif pendant la boucle, et chaque branche le fait décroître strictement ($i$ avance ou $d$ recule). ✓ Correction totale, temps $O(n)$, espace $O(1)$. (L'invariant à zones est le schéma des algorithmes de partition — on l'a entrevu avec le drapeau à deux couleurs du chapitre 1 et la partition du tri rapide ; sa force : chaque ligne de code se justifie par « quelle zone cette case rejoint-elle ? », et l'anomalie du cas 2 — ne pas avancer — cesse d'être une astuce pour devenir une nécessité démontrée.)

${\mathcal{I}}^{\prime }$ est un invariant irréprochable : $m=t[0]$ initialement (élément du préfixe), et chaque tour laisse $m$ inchangé ou l'affecte à $t[i]$ — toujours un élément du préfixe étendu. ✓ Mais à la sortie, ${\mathcal{I}}^{\prime }$ donne seulement : « $m$ appartient à $t$ » — ce que vérifie aussi return t[0] ! La postcondition « $m\ge x$ pour tout $x$ de $t$ » n'est pas impliquée : l'invariant est vrai mais trop faible. Celui qui convient (chapitre 1, exercice 6) : « $m$ est le maximum de $t[\mathrm{0..}i-1]$ » — appartenance et domination.

Méthode générale : l'invariant se construit à rebours depuis la postcondition — on écrit ce qu'on veut à la sortie ($m=\max t[\mathrm{0..}n-1]$), on remplace la borne finale par la variable de boucle ($m=\max t[\mathrm{0..}i-1]$), et l'on vérifie ensuite initialisation et conservation. Partir du code donne des invariants vrais ; partir de la postcondition donne des invariants utiles. (C'est le point 3 de la méthode du cours, vu en creux : la conclusion $\mathcal{I}\wedge \neg C\Rightarrow Q$ est une obligation de preuve à part entière, et c'est elle qui calibre la force de l'invariant.)

(a) Supposons disposer d'une fonction termine(f, x) qui répondrait, pour tout programme f et toute entrée x, si f(x) s'arrête. On construit alors le programme paradoxal :

def paradoxe(f):
    if termine(f, f):           # si f(f) s'arrête...
        while True:              # ... boucler sans fin
            pass
    return 0                     # sinon, s'arrêter

Que fait paradoxe(paradoxe) ? S'il s'arrête, c'est que termine a répondu « ne s'arrête pas » — contradiction ; s'il boucle, c'est que termine a répondu « s'arrête » — contradiction encore. Donc termine ne peut pas exister : c'est l'indécidabilité de l'arrêt (Turing, 1936). La terminaison se prouve au cas par cas, par l'intelligence d'un variant — jamais par un vérificateur universel ; et l'on a rencontré au chapitre 1 une boucle de quatre lignes (Syracuse) dont la terminaison résiste depuis un siècle.

(b) Le domaine de division(a, b) est infini ; un jeu de tests en visite un nombre fini. Pour tout jeu de tests fini, il existe un programme faux qui le passe : celui qui code en dur les bonnes réponses des tests et répond $0$ partout ailleurs. Le test établit la présence de conformité sur les cas essayés, jamais la correction universelle — chapitre 1, désormais argumenté.

(c) La preuve garantit l'algorithme sur tout le domaine, mais porte sur le texte idéal qu'on a raisonné — pas sur le fichier réellement exécuté, ses fautes de frappe, ses bornes décalées, sa bibliothèque surprenante (round(2.5) !). Le test exécute le vrai programme sur de vraies entrées, mais en nombre fini. L'un couvre l'infini des entrées, l'autre la réalité de la machine : aucun ne contient l'autre, et le programme officiel demande les deux — un algorithme doit se prouver, sa programmation doit se tester. (Les outils professionnels — preuve assistée, génération de tests — industrialisent chacun des deux pôles sans jamais abolir l'autre ; le grand théorème de (a) garantit même qu'aucune automatisation complète n'existera jamais : il restera toujours du métier.)