¿Qué es un bucle invariante?
Estoy leyendo "Introducción al algoritmo" de CLRS. En el capítulo 2, los autores mencionan las "invariantes de bucle". ¿Qué es un bucle invariante?
En palabras simples, un invariante de bucle es algún predicado (condición) que se cumple para cada iteración del bucle. Por ejemplo, veamos un forbucle simple parecido a este:
int j = 9;
for(int i=0; i<10; i++)
j--;
En este ejemplo es cierto (para cada iteración) que i + j == 9. Una invariante más débil que también es cierta es esa
i >= 0 && i <= 10.
Me gusta esta definición muy simple: ( fuente )
Una invariante de bucle es una condición [entre variables de programa] que necesariamente es verdadera inmediatamente antes e inmediatamente después de cada iteración de un bucle. (Tenga en cuenta que esto no dice nada sobre su verdad o falsedad a mitad de una iteración).
Por sí solo, un invariante de bucle no hace mucho. Sin embargo, dada una invariante adecuada, se puede utilizar para ayudar a demostrar la corrección de un algoritmo. El ejemplo simple en CLRS probablemente tenga que ver con la clasificación. Por ejemplo, deje que su invariante de bucle sea algo así como, al comienzo del bucle, ise ordenan las primeras entradas de esta matriz. Si puede demostrar que se trata de un invariante de bucle (es decir, que se mantiene antes y después de cada iteración del bucle), puede utilizarlo para demostrar la exactitud de un algoritmo de clasificación: al finalizar el bucle, el invariante del bucle aún se cumple. y el contador ies la longitud de la matriz. Por lo tanto, las primeras ientradas están ordenadas, lo que significa que toda la matriz está ordenada.
Un ejemplo aún más simple: invariantes de bucles, corrección y derivación de programas .
La forma en que entiendo un invariante de bucle es como una herramienta formal y sistemática para razonar sobre programas. Hacemos una única afirmación en la que nos centramos en demostrar que es verdadera y la llamamos invariante de bucle. Esto organiza nuestra lógica. Si bien también podemos discutir informalmente sobre la corrección de algún algoritmo, el uso de un invariante de bucle nos obliga a pensar con mucho cuidado y garantiza que nuestro razonamiento sea hermético.
