¿Qué es un invariante de bucle?

Me gusta esta definición muy simple: (fuente)

Un invariante de bucle es una condición [entre las variables del programa] que es necesariamente verdadera inmediatamente antes e inmediatamente después de cada iteración de un bucle. (Tenga en cuenta que esto no dice nada acerca de su verdad o falsedad en parte a través de una iteración.)

Por sí mismo, un invariante de bucle no hace mucho. Sin embargo, dado un invariante apropiado, se puede utilizar para ayudar a probar la corrección de un algoritmo. Simple ejemplo en CLRS probablemente tiene que ver con la ordenación. Por ejemplo, deje que su invariante de bucle sea algo así como, al comienzo del bucle, se ordenan las primeras entradas i de esta matriz. Si puede probar que esto es de hecho un invariante de bucle (es decir, que se mantiene antes y después de cada iteración de bucle), puede usar esto para probar la corrección de un algoritmo de ordenación: al final del bucle, el invariante de bucle sigue satisfecho, y el contador i es la longitud de la matriz. Por lo tanto, el las primeras entradas i son ordenadas significa que toda la matriz está ordenada.

Un ejemplo aún más simple: Loops Invariantes, Corrección y Derivación del Programa.

La forma en que entiendo un invariante de bucle es como una herramienta sistemática y formal para razonar sobre los programas. Hacemos una sola declaración que nos centramos en probar verdadero, y lo llamamos el invariante del lazo. Organiza nuestra lógica. Mientras que también podemos discutir informalmente sobre la corrección de algún algoritmo, usando un bucle invariante nos obliga a pensar con mucho cuidado y asegura que nuestro razonamiento es hermético.

Hay una cosa que muchas personas no se dan cuenta de inmediato cuando se trata de bucles e invariantes. Se confunden entre el invariante del bucle y el condicional del bucle (la condición que controla la terminación del bucle ).

Como la gente señala, el invariante de bucle debe ser verdadero

1. antes de que comience el bucle
2. antes de cada iteración del bucle
3. después de que el bucle termina

(aunque puede ser temporalmente falso durante el cuerpo del bucle ). Por otro lado, el bucle condicional debe ser false después de que el bucle termine, de lo contrario el bucle nunca terminaría.

Así, el invariante del bucle y el condicional del bucle deben ser condiciones diferentes.

Un buen ejemplo de invariante de bucle complejo es para la búsqueda binaria.

bsearch(type A[], type a) {
start = 1, end = length(A)

    while ( start <= end ) {
        mid = floor(start + end / 2)

        if ( A[mid] == a ) return mid
        if ( A[mid] > a ) end = mid - 1
        if ( A[mid] < a ) start = mid + 1

    }
    return -1

}

Así que el bucle condicional parece bastante sencillo - cuando start > end el bucle termina. Pero por qué ¿es el bucle correcto? ¿Cuál es el invariante de bucle que prueba su corrección?

El invariante es la declaración lógica:

if ( A[mid] == a ) then ( start <= mid <= end )

Esta afirmación es una tautología lógica - siempre es verdadera en el contexto del bucle / algoritmo específico que estamos tratando de probar. Y proporciona información útil sobre la corrección del bucle después de que termina.

Si regresamos porque encontramos el elemento en la matriz, entonces la instrucción es claramente verdadera, ya que si A[mid] == a entonces a está en la matriz y mid debe estar entre el inicio y el final. Y si el bucle termina porque start > end entonces no puede haber un número tal que start <= mid y mid <= end y por lo tanto sabemos que la declaración A[mid] == a debe ser falsa. Sin embargo, como resultado, la declaración lógica general sigue siendo verdadera en el sentido nulo. (En lógica la declaración if (false) then (something ) es siempre verdadera. )

Ahora qué pasa con lo que dije sobre el bucle condicional necesariamente siendo falso ¿cuándo termina el bucle? Parece que cuando el elemento se encuentra en la matriz, entonces el condicional de bucle es verdadero cuando el bucle termina!? En realidad no es, porque el condicional de bucle implícito es realmente while ( A[mid] != a && start <= end ) pero acortamos la prueba real ya que la primera parte está implícita. Este condicional es claramente falso después del bucle, independientemente de cómo termina el bucle.

Las respuestas anteriores han definido un Invariante de Bucle de una manera muy buena.

Ahora permítanme tratar de explicar cómo los autores de CLRS utilizaron Invariantes de Bucle para demostrar la corrección de la Clasificación de Inserción.

Algoritmo de ordenación de inserción (como se indica en el libro):

INSERTION-SORT(A)
    for j ← 2 to length[A]
        do key ← A[j]
        // Insert A[j] into the sorted sequence A[1..j-1].
        i ← j - 1
        while i > 0 and A[i] > key
            do A[i + 1] ← A[i]
            i ← i - 1
        A[i + 1] ← key

Invariante de bucle en este caso (Fuente: libro CLRS): Subarray[1 a j-1] siempre está ordenado.

Ahora vamos a comprobar esto y demostrar que el algoritmo es correcto.

Inicialización: Antes de la primera iteración j = 2. Así Subarray [1:1] es la matriz a ser tested.As solo tiene un elemento por lo que se ordena.Así Invariante es satisfecho.

Maintanence : Esto se puede verificar fácilmente comprobando el invariante después de cada iteration.In este caso está satisfecho.

Terminación: Este es el paso donde probaremos la corrección del algoritmo.

Cuando el bucle termina entonces el valor de j=n+1. De nuevo el invariante de bucle es satisfecho.Esto significa que El subarray[1 a n] debe ser ordenado.

Esto es lo que queremos hacer con nuestro Algoritmo.Por lo tanto, nuestro Algoritmo es correcto.

Además de todas las buenas respuestas, supongo que un gran ejemplo de Cómo pensar en Algoritmos, por Jeff Edmonds puede ilustrar el concepto muy bien:

EJEMPLO 1.2.1"El algoritmo de Dos dedos Find-Max"

1) Especificaciones: Una instancia de entrada consiste en una lista L(1..n) de elemento. La salida consiste en un índice i tal que L (i) tiene máximo valor. Si hay varias entradas con este mismo valor, entonces cualquier uno de ellos es devolver.

2) Pasos básicos: Usted decide sobre el método de dos dedos. Su dedo derecho corre por la lista.

3) Medida del progreso: La medida del progreso es qué tan lista de su dedo derecho es.

4) El Invariante del Bucle: El invariante del bucle indica que su dedo izquierdo apunta a una de las entradas más grandes encontradas hasta ahora por su dedo derecho.

5) Pasos principales: Cada iteración, mueve el dedo derecho hacia abajo uno entrada en la lista. Si su dedo derecho ahora está apuntando a una entrada que es más grande que la entrada del dedo izquierdo, luego mueva su izquierda dedo para estar con el dedo derecho.

6) Haz progreso: Haces progreso porque tu dedo derecho se mueve una entrada.

7) Mantener Invariante de Bucle: Usted sabe que el invariante de bucle se ha mantenido de la siguiente manera. Para cada paso, el nuevo elemento del dedo izquierdo es Max (elemento viejo dedo izquierdo, elemento nuevo). Por el invariante del lazo, esto es Max (Max (lista más corta), nuevo elemento). Matemáticamente, esto es Max (lista más larga).

8) Estableciendo el Invariante del Bucle: Usted establece inicialmente el invariante del bucle señalando ambos dedos al primer elemento.

9) Condición de salida: Ha terminado cuando su dedo derecho ha terminado recorriendo la lista.

10) Fin: Al final, sabemos que el problema se resuelve de la siguiente manera. Por la condición de salida, su dedo derecho ha encontrado todos el entrada. Por el invariante de bucle, su dedo izquierdo apunta al máximo de estos. Devuelve esta entrada.

11) Terminación y Tiempo de ejecución: El tiempo requerido es una constante veces la longitud de la lista.

12) Casos especiales: Compruebe lo que sucede cuando hay varias entradas con el mismo valor o cuando n = 0 o n = 1.

13) Detalles de Codificación e Implementación: ...

14) Prueba formal: La corrección del algoritmo se desprende de la por encima de los pasos.

Debe tenerse en cuenta que un Invariante de Bucle puede ayudar en el diseño de algoritmos iterativos cuando se considera una afirmación que expresa relaciones importantes entre las variables que deben ser verdaderas al comienzo de cada iteración y cuando el bucle termina. Si esto se mantiene, el cálculo está en el camino hacia la efectividad. Si es false, entonces el algoritmo ha fallado.

Invariante en este caso significa una condición que debe ser verdadera en un cierto punto en cada iteración de bucle.

En la programación por contrato, un invariante es una condición que debe ser verdadera (por contrato) antes y después de que se llame a cualquier método público.

El significado de invariante es nunca cambiar

Aquí el invariante del bucle significa "El cambio que sucede a la variable en el bucle (incremento o decremento) no está cambiando la condición del bucle, es decir, la condición es satisfactoria" de modo que el concepto invariante del bucle ha llegado

Es difícil hacer un seguimiento de lo que está sucediendo con los bucles. Los bucles que no terminan o terminan sin lograr su comportamiento objetivo es un problema común en la programación de computadoras. Los invariantes de bucle ayudan. Un invariante de bucle es una declaración formal sobre la relación entre variables en su programa que se mantiene verdadera justo antes de que el bucle se ejecute (estableciendo el invariante) y es verdadera de nuevo en la parte inferior del bucle, cada vez a través del bucle (manteniendo el invariante). Aquí está el patrón general del uso de Invariantes de Bucle en su código:

... // el Invariante del bucle debe ser verdadero aquí
while (TEST CONDITION) {
// parte superior del bucle
...
// parte inferior del bucle
// el Invariante del bucle debe ser verdadero aquí
}
// Terminación + Invariante de bucle = Meta
...
Entre la parte superior e inferior del bucle, presumiblemente se está avanzando hacia el objetivo del bucle. Esto podría perturbar (hacer false) el invariante. El punto de Invariantes de Bucle es la promesa de que el invariante será restaurado antes de repetir el cuerpo del bucle cada vez. Esto tiene dos ventajas:

El trabajo no se lleva a la siguiente pasada en formas complicadas y dependientes de los datos. Cada paso a través del bucle en independiente de todos los demás, con el invariante que sirve para unir los pasos juntos en un todo de trabajo. El razonamiento de que su bucle funciona se reduce al razonamiento de que el invariante del bucle se restaura con cada paso a través del bucle. Esto rompe el complicado comportamiento general del bucle en pequeños pasos simples, cada uno de los cuales se puede considerar por separado. La condición de prueba del bucle no es parte del invariante. Es lo que hace que el bucle termine. Consideras por separado dos cosas: por qué el bucle debe terminar alguna vez, y por qué el bucle logra su objetivo cuando termina. El bucle terminará si cada vez a través del bucle se mueve más cerca de satisfacer la condición de terminación. Es a menudo es fácil asegurar esto: por ejemplo, pisar una variable contraria por una hasta que alcance un límite superior fijo. A veces el razonamiento detrás de la terminación es más difícil.

El invariante de bucle debe ser creado de modo que cuando se alcanza la condición de terminación, y el invariante es verdadero, entonces se alcanza el objetivo:

Invariante + terminación = > meta
Se necesita práctica para crear invariantes que son simples y se relacionan que capturan todo el logro de la meta, excepto la terminación. Es mejor usar símbolos matemáticos para expresar invariantes de bucle, pero cuando esto conduce a situaciones demasiado complicadas, confiamos en una prosa clara y sentido común.

Lo siento, no tengo permiso para comentar.

@ Tomas Petricek como mencionaste

Un invariante más débil que también es cierto es que i > = 0 & & i

¿Cómo es un invariante de bucle?

Espero no estar equivocado, por lo que entiendo^[1], Loop invariant será true al principio del bucle (Inicialización), será true antes y después de cada iteración (Mantenimiento) y también será true después de la terminación del bucle (Termination). Pero después de la última iteración i se convierte en 10. Por lo tanto, la condición i >= 0 && i

[1] http://www.win.tue.nl / ~kbuchin/teaching/JBP030/notebooks/loop-invariants.html

La Propiedad Invariante de bucle es una condición que se mantiene para cada paso de una ejecución de bucle (ie. para los bucles, mientras que los bucles, etc.)

Esto es esencial para una Prueba de Invariante de Bucle, donde uno es capaz de demostrar que un algoritmo se ejecuta correctamente si en cada paso de su ejecución se mantiene esta propiedad invariante de bucle.

Para que un algoritmo sea correcto, el Invariante del bucle debe mantenerse en:

Inicialización (el principio)

Mantenimiento (cada paso después)

Terminación (cuando está terminado)

Esto se usa para evaluar un montón de cosas, pero el mejor ejemplo son los algoritmos codiciosos para el recorrido de grafos ponderados. Para que un algoritmo codicioso produzca una solución óptima (una ruta a través del gráfico), debe alcanzar conectar todos los nodos en la ruta de menor peso posible.

Por lo tanto, la propiedad invariante del bucle es que el camino tomado tiene el menor peso. En el que comienza no hemos añadido ninguna arista, por lo que esta propiedad es cierto (no es falso, en este caso). En cada paso, seguimos el borde de menor peso (el paso codicioso), por lo que nuevamente estamos tomando el camino de menor peso. En al final, hemos encontrado el camino más bajo, por lo que nuestra propiedad también es verdadera.

Si un algoritmo no hace esto, podemos probar que no es óptimo.

Invariante de bucle es una fórmula matemática como (x=y+1). En ese ejemplo, x y y representan dos variables en un bucle. Teniendo en cuenta el comportamiento cambiante de esas variables a lo largo de la ejecución del código, es casi imposible probar todos los valores posibles de x y y y ver si producen algún error. Digamos que x es un entero. Integer puede contener espacio de 32 bits en la memoria. Si ese número excede, se produce un desbordamiento del búfer. Así que tenemos que estar seguros de que a lo largo de la ejecución del código, nunca excede ese espacio. para eso, necesitamos entender una fórmula general que muestra la relación entre las variables. Después de todo, solo tratamos de entender el comportamiento del programa.

En palabras simples, es una condición de BUCLE que es verdadera en cada iteración de bucle:

for(int i=0; i<10; i++)
{ }

En esto podemos decir que el estado de i es i<10 and i>=0

Un invariante de bucle es una afirmación que es verdadera antes y después de la ejecución del bucle.

En la Búsqueda lineal (según el ejercicio dado en el libro), necesitamos encontrar el valor V en la matriz dada.

Es simple como escanear el array desde 0

Según mi entendimiento en el problema anterior -

Invariantes de bucle (Inicialización): V no se encuentra en la iteración k - 1. Muy primera iteración, esto sería -1 por lo tanto, podemos decir que V no se encuentra en la posición -1

Mantenimiento: En la siguiente iteración,V no encontrada en k-1 es verdadera

Termination: Si V se encuentra en k posición o k alcanza la longitud de la matriz, terminar el bucle.