¿Cómo se obtiene el bucle invariante en este algoritmo de búsqueda de límite de raíz cuadrada?

Originalmente en matemáticas . SE pero sin respuesta allí.

Considere el siguiente algoritmo.

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 

donde u, v y n son números enteros y la operación de división es división entera.

• Explica lo que calcula el algoritmo.
• Usando su respuesta a la parte I como la condición posterior para el algoritmo, establezca un bucle invariante y demuestre que el algoritmo termina y es correcto.

En clase, se encontró que la condición posterior era y la invariante es . Realmente no entiendo cómo se obtuvieron las condiciones posteriores y las invariantes. Me imagino que la condición de publicación fue ... que claramente no es el caso. Entonces me pregunto cómo se obtuvo la condición posterior e invariante. También me pregunto cómo se puede obtener la precondición usando la postcondición.$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 tiene razón en que la técnica general es ir a pescar en busca de observaciones interesantes.

En este caso, puede observar que el programa es una instancia de búsqueda binaria, porque tiene la siguiente forma:

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

A continuación, sólo tiene que enchufar en su concreto f, X... en el invariante general para la búsqueda binaria. Dijkstra tiene una buena discusión sobre la búsqueda binaria .

es de hecho una condición posterior del ciclo while (¿por qué crees que no es "claramente" el caso?). Este es siempre el caso con un ciclo while que no contiene un: cuando el ciclo sale, solo puede ser porque la condición del ciclo (aquí, u + 1 ≠ v ) es falsa. No es lo único que será cierto cuando el ciclo salga aquí (este algoritmo realmente calcula algo interesante, como viste en tu clase, por lo que u = [esta cosa interesante] y v = [esta cosa interesante] también son condiciones posteriores ), pero es lo más obvio.$u+1=v$break$u+1 \neq v$$u = \text{[this interesting thing]}$$v = \text{[this interesting thing]}$

Ahora, para encontrar otras propiedades interesantes, no hay una receta general. De hecho, hay un sentido formal en el que no hay una receta general para encontrar invariantes de bucle. Lo mejor que puede hacer es aplicar algunas técnicas que solo funcionan en algunos casos, o generalmente ir a pescar para observaciones interesantes (que funciona mejor y mejor a medida que adquiere más experiencia).

Si ejecuta el ciclo durante algunas iteraciones con algún valor de , verá eso en cada iteración:$n$

• u salta hasta ( u + v ) / 2 ;$u$$(u+v)/2$
• o salta a ( u + v ) / 2 .$v$$(u+v)/2$

En particular, comienza menos que v , y nunca lo superará. Además, u comienza positivo y aumenta, mientras que v comienza en n + 1 y disminuye. Entonces 0 ≤ u ≤ v ≤ n + 1 es una invariante en todo este programa.$u$$v$$u$$v$$n+1$$0 \le u \le v \le n+1$

Una cosa que no es tan obvio es si nunca puede ser igual a v . Eso es importante: si u y v alguna vez se vuelven iguales, tendremos x = u = v y el ciclo continuará para siempre. Por lo tanto, debe demostrar que u y v nunca se vuelven iguales para demostrar que el algoritmo es correcto (es decir, no se repite para siempre). Una vez que se ha identificado esta necesidad, es fácil demostrar (lo dejo como ejercicio) que u < v es un bucle invariante (tenga en cuenta que u y v son enteros, por lo que esto es equivalente a $u$$v$$u$$v$$x = u = v$$u$$v$$u < v$$u$$v$ ).$u+1 \le v$

Como al final del programa, la condición posterior que le dieron también se puede escribir u 2 ≤ n < v 2 (la parte 0 ≤ u 2 es trivial). La razón por la que queremos una condición posterior como esta, que involucre n , es que queremos vincular el resultado del programa con la entrada n . ¿Por qué esta condición precisa? Estamos buscando algo que sea lo más preciso posible, y observamos dónde aparece n dentro del bucle:$v = u+1$$u^2 \le n < v^2$$0 \le u^2$$n$$n$$n$

• tenemos ;$u \le x \le v$
• cuando , elegimos la siguiente u para que sea x , de modo que u 2 ≤ n (y v no cambie);$x^2 \le n$$u$$x$$u^2 \le n$$v$
• cuando , elegimos la siguiente v para que sea x , de modo que n < v 2 ( yu no cambie).$x^2 > n$$v$$x$$n < v^2$$u$

Esta dicotomía sugiere que quizás todo el tiempo. En otras palabras, sospechamos que es un bucle invariante. Verificar esto se deja como un ejercicio para el lector (recuerde verificar que la propiedad sea verdadera inicialmente).$u^2 \le n < v^2$

Y ahora que hemos hecho todo esto, vemos que y ( u + 1 ) 2 > n : u es la raíz cuadrada de n redondeado hacia abajo al entero más cercano.$u^2 \le n$$(u+1)^2 > n$$u$$n$