La postcondition d'un tri a deux moitiés

La fonction fautive. Elle rend un tableau parfaitement croissant :

def tri_faux(t):
    """Rend un tableau croissant... en écrasant ce qui dépasse."""
    for i in range(1, len(t)):
        if t[i] < t[i - 1]:
            t[i] = t[i - 1]
    return t

tri_faux([5, 2, 8, 1])       # [5, 5, 8, 8]

Le résultat est croissant : la première moitié de la postcondition est satisfaite. Mais les effectifs sont passés de {5: 1, 2: 1, 8: 1, 1: 1} à {5: 2, 8: 2} : deux valeurs ont disparu, deux ont été dupliquées. Ce n'est pas un tri, c'est une destruction.

La vérification des vrais tris. Le contrôle se fait de deux façons, qui se valent :

a = list(t); tri_insertion(a)
b = list(t); tri_selection(b)
assert sorted(a) == sorted(t) == sorted(b)          # meme multiensemble
assert effectifs(a) == effectifs(t) == effectifs(b) # meme, par comptage

$3000$ tableaux tirés au hasard, avec beaucoup de doublons — $3000$ cas passent.

Pourquoi les vrais tris ne peuvent pas échouer là-dessus. C'est un argument de démonstration, pas de test. Le tri par sélection ne fait qu'échanger : un échange permute deux cases, il ne crée ni ne détruit rien. Le tri par insertion décale puis dépose : la valeur x est sauvegardée avant que sa case ne soit écrasée, et redéposée exactement une fois. Dans les deux cas, le multiensemble des valeurs est un invariant de tout le programme, pas seulement d'une boucle.

La leçon. Une postcondition partielle ne prouve rien. « Le tableau sort croissant » est vérifiable en un parcours et rassurant — et complètement insuffisant. tri_faux passerait ce test sur tous les tableaux du monde. La seconde moitié, « et il contient les mêmes éléments », n'est pas un détail de rédaction : c'est elle qui distingue un tri d'un écrasement.