La dichotomie entière qui ne se termine pas

Voici la recherche d'un seuil sur les entiers, telle qu'on l'écrit spontanément — $p$ étant une propriété monotone, fausse puis vraie :

(* FAUX : ne termine pas. *)
while !bas < !haut do
  let m = (!bas + !haut) / 2 in
  if p m then haut := m else bas := m       (* <-- bas := m *)
done

Mesuré sur $p(n)=(n^2\ge 50)$ dans $[0,50]$ : la boucle atteint l'état $\mathtt{bas}=7$, $\mathtt{haut}=8$, et y reste. En effet $m=(7+8)/2=7$ par troncature, $p(7)$ est faux puisque $49<50$, donc $\mathtt{bas}:=7$ : rien n'a bougé, et le tour suivant est identique. L'exécution a été arrêtée à cent tours.

Le diagnostic. La division entière tronque vers le bas : quand $\mathtt{haut}=\mathtt{bas}+1$, le milieu vaut $\mathtt{bas}$. L'affectation bas := m ne change alors rien, et le variant $\mathtt{haut}-\mathtt{bas}$ cesse de décroître.

La correction — une unité :

(* Plus petit n de [bas, haut] tel que p n, en supposant p monotone et p haut vrai.
   Complexité : Theta(log (haut - bas)). *)
let cherche_seuil p bas0 haut0 =
  let bas = ref bas0 and haut = ref haut0 in
  (* INVARIANT : le seuil est dans [bas, haut]. *)
  while !bas < !haut do
    let m = !bas + (!haut - !bas) / 2 in
    if p m then haut := m else bas := m + 1        (* +1 : m est ÉLIMINÉ *)
  done;
  !bas

Elle rend $8$ en $6$ tours, et l'on vérifie $8^2=64\ge 50>49=7^2$.

Le raisonnement qui l'aurait évitée. Écrire le variant avant le code. Le variant est $\mathtt{haut}-\mathtt{bas}$ ; pour qu'il décroisse strictement, il faut que chaque branche élimine au moins une valeur. Si $p(m)$ est faux, alors $m$ n'est pas le seuil : on peut, et l'on doit, l'éliminer — d'où $\mathtt{bas}:=m+1$. Si $p(m)$ est vrai, $m$ est un candidat qu'il faut garder : $\mathtt{haut}:=m$, et c'est le choix de la troncature vers le bas qui rend cette branche sûre.

La règle générale, et elle se retient. Dans une dichotomie entière, la branche qui garde le candidat doit être celle vers laquelle la division tronque. Ici la troncature va vers le bas, donc c'est haut qui garde. Si l'on cherchait le plus grand $n$ tel que $p(n)$, il faudrait arrondir le milieu vers le haut, sans quoi la même boucle infinie reviendrait de l'autre côté.