Une spécification qui ment

/* Renvoie l'indice de la DERNIERE occurrence de v dans t[0..n-1], ou -1. */
int derniere(const int t[], int n, int v) {
    for (int i = 0; i < n; i = i + 1) {
        if (t[i] == v) { return i; }
    }
    return -1;
}

Le code rend la première occurrence, pas la dernière. Mesuré sur $t=[4,7,4,9,4]$ :

derniere(t, 5, 4) = 0     la specification annonce 4
derniere(t, 5, 7) = 1     une seule occurrence : indistinguable
derniere(t, 5, 8) = -1    absent : indistinguable

Le point de méthode. On ne sait pas, en toute rigueur, « laquelle des deux est fausse » : le commentaire et le code se contredisent, et rien dans le fragment ne dit lequel exprime l'intention. C'est précisément le problème. Une spécification écrite après le corps décrit ce que le code fait — elle ne peut donc pas le contredire, mais elle ne sert à rien non plus. Une spécification écrite avant décide, et une contradiction devient alors un défaut identifié, du côté du code.

Le test qui l'aurait montré. Il faut un tableau qui contienne au moins deux occurrences de la valeur cherchée. Les deux derniers cas mesurés ci-dessus, qui sont pourtant les premiers auxquels on pense — une occurrence, aucune occurrence —, ne séparent pas les deux fonctions. C'est un exemple direct du partitionnement des domaines d'entrée : la classe pertinente ici n'est pas « présent / absent » mais « zéro, une, plusieurs occurrences ».

La correction, selon l'intention retenue :

/* Renvoie l'indice de la derniere occurrence de v dans t[0..n-1], ou -1.
   Precondition : n >= 0. */
int derniere(const int t[], int n, int v) {
    assert(n >= 0);
    for (int i = n - 1; i >= 0; i = i - 1) {
        if (t[i] == v) { return i; }
    }
    return -1;
}

Parcourir à l'envers, plutôt que retenir le dernier indice vu, évite de continuer après avoir trouvé.