Probleme – La postcondition qu'on oublie : trier, c'est aussi permuter

void tri(int t[], int n) {
    if (n == 0) { return; }
    int mini = t[0];
    for (int i = 1; i < n; i = i + 1) { if (t[i] < mini) { mini = t[i]; } }
    for (int i = 0; i < n; i = i + 1) { t[i] = mini; }
}

1. La postcondition complète comporte deux clauses, et la seconde est celle qu'on omet :

• [(i)] $t[0]\le t[1]\le \cdots \le t[n-1]$ — le tableau est croissant ;
• [(ii)] le tableau final est une permutation du tableau initial — mêmes valeurs, mêmes multiplicités.

Sans (ii), la spécification est satisfaite par la fonction qui écrit $0$ partout.

2. Les deux vérificateurs.

/* Renvoie true ssi t[0..n-1] est croissant au sens large. */
bool est_trie(const int t[], int n) {
    for (int i = 1; i < n; i = i + 1) { if (t[i-1] > t[i]) { return false; } }
    return true;
}

/* Renvoie true ssi b[0..n-1] est une permutation de a[0..n-1].
   copie(t, n) duplique t dans un bloc neuf (NULL si l'allocation echoue),
   compare_int est la comparaison d'entiers attendue par qsort.
   Complexite : Theta(n log n), par tri des deux copies. */
bool est_permutation(const int a[], const int b[], int n) {
    int* u = copie(a, n); int* v = copie(b, n);
    if (u == NULL || v == NULL) { free(u); free(v); return false; }
    qsort(u, n, sizeof(int), compare_int);
    qsort(v, n, sizeof(int), compare_int);
    bool ok = (memcmp(u, v, (size_t) n * sizeof(int)) == 0);
    free(u); free(v);
    return ok;
}

3. Le verdict. La fonction proposée calcule le minimum et le recopie partout. Mesuré sur $[3,1,4,1,5]$ :

tri correct    : 1 1 3 4 5 | est_trie VRAI | est_permutation VRAI
fonction testee: 1 1 1 1 1 | est_trie VRAI | est_permutation FAUX

Et elle passe tous les tests d'un jeu qui ne vérifierait que le tri :

{1,2,3} -> {1,1,1} : est_trie VRAI
{3,2,1} -> {1,1,1} : est_trie VRAI
{2,2,2} -> {2,2,2} : est_trie VRAI
{5,5,5} -> {5,5,5} : est_trie VRAI

Quatre cas de test bien partitionnés — trié, inversé, constant — et tous verts sur une fonction qui détruit les données.

Une méthode de test qui découle de tout cela : le test par propriétés. Plutôt que d'écrire des couples (entrée, sortie attendue), on écrit les invariants de la fonction et on les vérifie sur des entrées tirées au hasard :

for (int essai = 0; essai < 10000; essai = essai + 1) {
    int n = alea(0, 50);
    int* a = tableau_aleatoire(n);
    int* b = copie(a, n);
    tri(b, n);
    assert(est_trie(b, n));
    assert(est_permutation(a, b, n));      /* la clause qu'on oublie */
    free(a); free(b);
}

Le programme officiel n'exige pas la génération automatique de jeux de tests, et ce fragment n'y prétend pas : les propriétés, elles, sont écrites à la main. C'est seulement l'énumération des cas qui est confiée à la machine.