Comment l'invariant de boucle est-il obtenu dans cet algorithme de recherche de racine carrée?
Initialement sur math.SE mais sans réponse là-bas. Considérez l'algorithme suivant. u := 0 v := n+1; while ( (u + 1) is not equal to v) do x := (u + v) / 2; if ( x * x <= n) u := x; else v := x; end_if end_while où u, v et n sont des entiers et l'opération de division est une division entière....