Probleme – La dichotomie, jusqu'au nombre exact de tours

1. Le code.

/* Renvoie un indice i tel que t[i] == v, ou -1 si v ne figure pas dans
   t[0..n-1].
   Precondition  : n >= 0 et t[0..n-1] est croissant (au sens large).
   Postcondition : soit le resultat vaut -1 et v est absent de t[0..n-1],
                   soit 0 <= resultat < n et t[resultat] == v. */
int cherche(const int t[], int n, int v) {
    assert(n >= 0);
    int g = 0, d = n - 1;
    /* INVARIANT : si v figure dans t[0..n-1], alors il figure dans
       t[g..d].            VARIANT : d - g + 1. */
    while (g <= d) {
        int m = g + (d - g) / 2;
        if (t[m] == v) { return m; }
        if (t[m] < v) { g = m + 1; } else { d = m - 1; }
    }
    return -1;
}

2. Les preuves.

Terminaison. Variant $V=d-g+1$, le nombre de cases encore candidates. Il est entier, et positif tant que $g\le d$. À chaque tour où l'on ne retourne pas, ou bien $g$ passe à $m+1>g$, ou bien $d$ passe à $m-1<d$ : dans les deux cas $V$ décroît d'au moins $1$. La boucle s'arrête.

Correction. Initialisation : $g=0$, $d=n-1$, donc $t[g..d]$ est tout le tableau : l'invariant est trivialement vrai. Conservation : supposons-le vrai et $t[m]\ne v$. Si $t[m]<v$, alors par croissance $t[k]\le t[m]<v$ pour tout $k\le m$ : $v$ ne peut figurer dans $t[g..m]$, donc s'il figure quelque part dans $t[g..d]$ c'est dans $t[m+\mathrm{1..}d]$ — ce qui est exactement le nouvel intervalle. Le cas $t[m]>v$ est symétrique. Utilisation : deux sorties possibles. Ou bien on retourne $m$ avec $t[m]=v$, et la postcondition est vérifiée. Ou bien on sort par $g>d$ : l'intervalle $t[g..d]$ est vide, et l'invariant dit alors que $v$ ne figure nulle part — on rend $-1$.

3. Le nombre exact de tours. Notons $V_k$ la valeur du variant après $k$ tours, avec $V_0=n$. Le tour retire la case $m$ et garde l'un des deux côtés, dont la taille est au plus $\lceil (V-1)/2\rceil \le \lfloor V/2\rfloor$. Donc $V_k\le \lfloor n/2^k\rfloor$, et la boucle s'arrête dès que $V_k=0$, c'est-à-dire au plus tard pour $2^k>n$, soit $k=\lfloor {\log }_{2}n\rfloor +1$.

Cette borne est atteinte : en cherchant une valeur absente, on ne retourne jamais par le return m, et le pire cas est réalisé. Vérification, en essayant toutes les valeurs présentes et absentes pour chaque $n$ :

   n |    1 |    2 |    3 |    4 |    7 |    8 |   15 |   16 |  100 | 1000 | 10^6
tours|    1 |    2 |    2 |    3 |    3 |    4 |    4 |    5 |    7 |   10 |   20
log2 |    1 |    2 |    2 |    3 |    3 |    4 |    4 |    5 |    7 |   10 |   20

Le maximum mesuré vaut $\lfloor {\log }_{2}n\rfloor +1$ pour les onze tailles. Noter le saut à chaque puissance de deux : de $n=7$ à $n=8$, un tour de plus ; de $n=8$ à $n=15$, aucun. Un million de cases se fouillent en vingt comparaisons.

4. La première occurrence. La postcondition dit « un indice $i$ tel que $t[i]=v$ », pas « le plus petit ». Sur $t=[2,2,2,2,2]$ et $v=2$, le premier milieu est $m=2$ et la fonction rend $2$ : ni la première occurrence, ni la dernière.

Ce n'est pas un défaut, c'est la spécification. La corriger a un coût qu'il faut connaître : pour obtenir la première occurrence, on ne s'arrête pas sur l'égalité, on continue de chercher à gauche.

/* Renvoie le plus petit i tel que t[i] >= v, ou n si v majore t.
   Precondition : t[0..n-1] croissant. */
int borne_inferieure(const int t[], int n, int v) {
    int g = 0, d = n;                   /* d est EXCLU : l'invariant change */
    /* INVARIANT : tous les t[k] pour k < g sont < v, et tous les t[k]
       pour k >= d sont >= v. */
    while (g < d) {
        int m = g + (d - g) / 2;
        if (t[m] < v) { g = m + 1; } else { d = m; }
    }
    return g;
}

Elle n'a aucune sortie anticipée : le nombre de tours ne dépend pas de la valeur cherchée, seulement du chemin suivi, et il vaut au plus $\lceil {\log }_2(n+1)\rceil$. Mesuré sur toutes les valeurs, présentes et absentes : entre $19$ et $20$ tours pour $n=10^6$, et borne_inferieure rend bien $0$ sur $[2,2,2,2,2]$, là où cherche rendait $2$.

Le changement de convention sur $d$ — exclu au lieu d'inclus — est ce qui rend l'invariant énonçable : avec $d$ inclus, il faudrait parler de $t[d+1]$, indice qui peut valoir $n$. Un intervalle mal choisi rend une preuve pénible ; c'est souvent le signe qu'il faut changer de convention, pas de code.