Amusant... Au vu de la correction d'un examen, de discussions avec des collègues et de mon propre comportement, quand on demande de prouver qu'un algorithme de tri est bien un algorithme de tri, les gens pensent spontanément à prouver que la sortie est triée, mais pas que c'est une permutation de l'entrée !

PS J. Moore vient de plaisanter sur le même sujet : après avoir « prouvé correct » le tri par insertion, il fait remarquer qu'avec sa spécification « la sortie est triée », la fonction retournant la liste constante 1 2 3 4 convient...