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.

• Expliquez ce qui est calculé par l'algorithme.
• En utilisant votre réponse à la partie I comme post-condition pour l'algorithme, établissez un invariant de boucle et montrez que l'algorithme se termine et est correct.

En classe, la post-condition s'est avérée être et l'invariant est . Je ne comprends pas vraiment comment la post-condition et les invariants ont été obtenus. Je suppose que la condition de poste était ... ce qui n'est clairement pas le cas. Je me demande donc comment la post-condition et l'invariant ont été obtenus. Je me demande également comment obtenir la précondition en utilisant la post-condition.$0 \leq u^2 \leq n < (u + 1)^2$$0 \leq u^2 \leq n < v^2, u + 1 \leq v$$u + 1 = v$

Gilles a raison de dire que la technique générale est d'aller à la pêche pour des observations intéressantes.

Dans ce cas, vous pouvez observer que le programme est une instance de recherche binaire, car il a la forme suivante:

while i + 1 != k
  j := strictly_between(i, k)
  if f(j) <= X then i := j
  if f(j) > X then k := j

Ensuite , vous suffit de brancher votre particulier f, X... dans l'invariant général pour la recherche binaire. Dijkstra a une belle discussion sur la recherche binaire .

$u+1=v$ est en effet une post-condition de la boucle while (pourquoi pensez-vous que ce n'est "clairement" pas le cas?). C'est toujours le cas avec une boucle while qui ne contient pas a break: lorsque la boucle se termine, cela ne peut être que parce que la condition de la boucle (ici, ) est fausse. Ce n'est pas la seule chose qui sera vraie lorsque la boucle se terminera ici (cet algorithme calcule en fait quelque chose d'intéressant, comme vous l'avez vu dans votre classe, donc et sont aussi des post-conditions), mais c'est le plus évident.$u+1 \neq v$$u = \text{[this interesting thing]}$$v = \text{[this interesting thing]}$

Maintenant, pour trouver d'autres propriétés intéressantes, il n'y a pas de recette générale. En fait, il existe un certain sens formel dans lequel il n'y a pas de recette générale pour trouver des invariants de boucle. Le mieux que vous puissiez faire est d'appliquer certaines techniques qui ne fonctionnent que dans certains cas, ou généralement d'aller à la pêche pour des observations intéressantes (qui fonctionnent de mieux en mieux à mesure que vous vous familiarisez).

Si vous exécutez la boucle pour quelques itérations avec une valeur de , vous verrez qu'à chaque itération:$n$

• soit saute jusqu'à ;$u$$(u+v)/2$
• ou passe à .$v$$(u+v)/2$

En particulier, commence moins que et ne le dépassera jamais. De plus, commence positif et augmente, tandis que commence à et diminue. Donc est un invariant tout au long de ce programme.$u$$v$$u$$v$$n+1$$0 \le u \le v \le n+1$

Une chose qui n'est pas si évidente est de savoir si peut jamais être égal à . C'est important: si et deviennent égaux, nous aurons et la boucle continuera indéfiniment. Vous devez donc prouver que et ne deviennent jamais égaux afin de prouver que l'algorithme est correct (c'est-à-dire qu'il ne boucle pas indéfiniment). Une fois ce besoin identifié, il est facile de prouver (je laisse cela comme un exercice) que est un invariant de boucle (gardez à l'esprit que et sont des entiers, donc cela équivaut à ).$u$$v$$u$$v$$x = u = v$$u$$v$$u < v$$u$$v$$u+1 \le v$

Puisque à la fin du programme, la post-condition qui vous a été donnée peut également s'écrire (la partie est triviale). La raison pour laquelle nous voulons une post-condition comme celle-ci, impliquant , est que nous voulons lier le résultat du programme avec l'entrée . Pourquoi cette condition précise? Nous recherchons quelque chose d'aussi précis que possible, et nous regardons où apparaît à l'intérieur de la boucle:$v = u+1$$u^2 \le n < v^2$$0 \le u^2$$n$$n$$n$

• nous avons ;$u \le x \le v$
• lorsque , nous choisissons le suivant pour être , de sorte que (et ne change pas);$x^2 \le n$$u$$x$$u^2 \le n$$v$
• lorsque , nous choisissons le suivant comme , de sorte que (et ne change pas).$x^2 > n$$v$$x$$n < v^2$$u$

Cette dichotomie laisse entendre que peut-être tout le temps. En d'autres termes, nous soupçonnons qu'il s'agit d'un invariant de boucle. La vérification est laissée au lecteur comme exercice (n'oubliez pas de vérifier que la propriété est vraie au départ).$u^2 \le n < v^2$

Et maintenant que nous avons fait tout cela, nous voyons que et : est la racine carrée de arrondie à l'entier le plus proche.( u + 1 ) 2 > n u $u^2 \le n$$(u+1)^2 > n$$u$$n$