informatique (MP2I/MPI) · Chapitre 15 · Exercice de TD
Dichotomiser sur la réponse : la racine carrée entière
Diviser pour régner · niveau 2
Énoncé
Écrire, avec spécification, terminaison et correction, une fonction rendant sans employer de flottants. Où se cache le débordement ?
Corrigé
La propriété « » est monotone en : vraie jusqu'à un seuil, fausse ensuite. On dichotomise sur ce seuil.
(* Renvoie le plus grand r tel que r*r <= n, c'est-à-dire floor(sqrt n).
Précondition : n >= 0. Aucun flottant, aucun débordement.
Complexité : Theta(log n). *)
let racine n =
let bas = ref 0 and haut = ref (n + 1) in
(* INVARIANT : bas*bas <= n < haut*haut, et bas < haut. *)
while !haut - !bas > 1 do
let m = !bas + (!haut - !bas) / 2 in
if m <= n / m then bas := m else haut := m (* PAS m * m <= n *)
done;
!bas
Terminaison. Variant : . Comme dès que l'écart dépasse , l'affectation réduit strictement l'écart. Il faut tours.
Correction. L'invariant tient à l'initialisation : et pour . Il est préservé par construction, puisqu'on remplace l'une des bornes par du bon côté du test. À la sortie, et : c'est la définition de .
Le débordement, et il est où l'on ne l'attend pas. La forme naturelle du test est m * m <= n. Or vaut environ au premier tour : le produit approche , qui déborde bien avant . Mesuré en OCaml, dont les entiers font bits (max_int ) :
test m * m <= n | test m <= n / m | |
|---|---|---|
La première divergence apparaît à , valeur trouvée en balayant les puissances de deux. Au-delà, la version naïve rend des résultats absurdes — un « » plus grand que — sans le moindre signalement.
Le remède. Écrire m <= n / m : la division entière ne déborde jamais, et le test est équivalent pour . C'est le même geste qu'au chapitre chap:langage-c — x <= INT8_MAX - y plutôt que x + y <= INT8_MAX : on réécrit le test pour que l'expression testée ne puisse pas déborder avant d'être testée.