En informática , un invariante de bucle es una propiedad de un bucle de programa que es verdadera antes (y después) de cada iteración. Es una afirmación lógica , a veces comprobada con una afirmación de código . Conocer su(s) invariante(s) es esencial para comprender el efecto de un bucle.
En la verificación formal de programas , en particular el enfoque Floyd-Hoare , los invariantes de bucle se expresan mediante la lógica de predicados formales y se utilizan para demostrar propiedades de bucles y, por extensión, algoritmos que emplean bucles (normalmente propiedades de corrección ). Los invariantes de bucle serán verdaderos al entrar en un bucle y después de cada iteración, de modo que al salir del bucle se puedan garantizar tanto los invariantes de bucle como la condición de terminación del bucle.
Desde el punto de vista de la metodología de programación, el invariante de bucle puede considerarse como una especificación más abstracta del bucle, que caracteriza el propósito más profundo del bucle más allá de los detalles de su implementación. Un artículo de investigación [1] cubre algoritmos fundamentales de muchas áreas de la informática (búsqueda, ordenación, optimización, aritmética, etc.), caracterizando cada uno de ellos desde el punto de vista de su invariante.
Debido a la similitud entre los bucles y los programas recursivos , demostrar la corrección parcial de los bucles con invariantes es muy similar a demostrar la corrección de los programas recursivos por inducción . De hecho, el invariante del bucle suele ser el mismo que la hipótesis inductiva que se debe demostrar para un programa recursivo equivalente a un bucle dado.
La siguiente subrutina C devuelve el valor máximo en su matriz de argumentos , siempre que su longitud sea al menos 1. Se proporcionan comentarios en las líneas 3, 6, 9, 11 y 13. Cada comentario hace una afirmación sobre los valores de una o más variables en esa etapa de la función. Las afirmaciones resaltadas dentro del cuerpo del bucle, al principio y al final del bucle (líneas 6 y 11), son exactamente las mismas. Por lo tanto, describen una propiedad invariante del bucle. Cuando se llega a la línea 13, esta invariante aún se cumple y se sabe que la condición del bucle de la línea 5 se ha vuelto falsa. Ambas propiedades juntas implican que es igual al valor máximo en , es decir, que se devuelve el valor correcto de la línea 14. max()a[]ni!=nma[0...n-1]
int máx ( int n , constante int a []) { int m = a [ 0 ]; // m es igual al valor máximo en a[0...0] int i = 1 ; mientras ( i != n ) { // m es igual al valor máximo en a[0...i-1] si ( m < a [ i ]) m = a [ i ]; // m es igual al valor máximo en a[0...i] ++ yo ; // m es igual al valor máximo en a[0...i-1] } // m es igual al valor máximo en a[0...i-1], e i==n devuelve m ; }Siguiendo un paradigma de programación defensiva , la condición de bucle i!=nen la línea 5 debería modificarse mejor a i<n, para evitar bucles infinitos para valores negativos ilegítimos de n. Si bien este cambio en el código intuitivamente no debería hacer ninguna diferencia, el razonamiento que lleva a su corrección se vuelve algo más complicado, ya que entonces solo i>=nse conoce en la línea 13. Para obtener que también i<=nse cumple, esa condición debe incluirse en el invariante del bucle. Es fácil ver que i<=n, también, es un invariante del bucle, ya que i<nen la línea 6 se puede obtener a partir de la condición de bucle (modificada) en la línea 5, y por lo tanto i<=nse cumple en la línea 11 después de que ise ha incrementado en la línea 10. Sin embargo, cuando los invariantes de bucle deben proporcionarse manualmente para la verificación formal del programa, i<=na menudo se pasan por alto propiedades intuitivamente demasiado obvias como .
En la lógica Floyd-Hoare , [2] [3] la corrección parcial de un bucle while está gobernada por la siguiente regla de inferencia:
Esto significa:
En otras palabras: la regla anterior es un paso deductivo que tiene como premisa el triple de Hoare . Este triple es en realidad una relación sobre los estados de la máquina. Se cumple siempre que, partiendo de un estado en el que la expresión booleana es verdadera y ejecutando con éxito algún código llamado , la máquina termina en un estado en el que I es verdadero. Si se puede demostrar esta relación, la regla nos permite concluir que la ejecución exitosa del programa conducirá desde un estado en el que I es verdadero a un estado en el que se cumple. La fórmula booleana I en esta regla se llama invariante de bucle.
Con algunas variaciones en la notación utilizada, y con la premisa de que el bucle se detiene, esta regla también se conoce como el Teorema de Relación Invariante . [4] [5] Como lo presenta un libro de texto de la década de 1970 de una manera que estaba destinada a ser accesible para los programadores estudiantes: [4]
Supongamos que la notación P { seq } Qsignifica que si Pes verdadero antes de que se ejecute la secuencia de enunciados seq, entonces Qes verdadero después de ella. Entonces, el teorema de la relación invariante se cumple:
P & c { seq } PP { DO WHILE (c); seq END; } P & ¬cEl siguiente ejemplo ilustra cómo funciona esta regla. Considere el programa
mientras (x < 10) x := x+1;
Se puede entonces demostrar el siguiente triple de Hoare:
La condición C del whilebucle es . Hay que adivinar un invariante de bucle I útil ; se comprobará que es apropiado. Con estas suposiciones es posible demostrar el siguiente triple de Hoare:
Si bien esta tripleta se puede derivar formalmente de las reglas de la lógica Floyd-Hoare que rigen la asignación, también se justifica intuitivamente: el cálculo comienza en un estado donde es verdadero, lo que significa simplemente que es verdadero. El cálculo suma 1 a x , lo que significa que sigue siendo verdadero (para el entero x).
Bajo esta premisa, la regla de whilelos bucles permite la siguiente conclusión:
Sin embargo, la postcondición ( x es menor o igual a 10, pero no es menor que 10) es lógicamente equivalente a , que es lo que queríamos mostrar.
La propiedad es otra invariante del bucle de ejemplo, y la propiedad trivial es otra. Al aplicar la regla de inferencia anterior a la invariante anterior, se obtiene . Al aplicarla a la invariante , se obtiene , que es ligeramente más expresivo.
El lenguaje de programación Eiffel ofrece compatibilidad nativa con invariantes de bucle. [6] Un invariante de bucle se expresa con la misma sintaxis que se utiliza para un invariante de clase . En el ejemplo siguiente, la expresión de invariante de bucle x <= 10debe ser verdadera después de la inicialización del bucle y después de cada ejecución del cuerpo del bucle; esto se verifica en tiempo de ejecución.
desde x := 0 invariante x <= 10 hasta x > 10 bucle x := x + 1 fin El lenguaje de programación Whiley también proporciona soporte de primera clase para invariantes de bucle. [7] Los invariantes de bucle se expresan utilizando una o más wherecláusulas, como se ilustra a continuación:
function max ( int [] items ) -> ( int r ) // Requiere al menos un elemento para calcular max requiere | items | > 0 // (1) El resultado no es menor que ningún elemento asegura all { i en 0 .. | items | | items [ i ] <= r } // (2) El resultado coincide con al menos un elemento asegura some { i en 0 .. | items | | items [ i ] == r } : // nat i = 1 int m = items [ 0 ] // while i < | items | // (1) Ningún elemento visto hasta ahora es mayor que m donde all { k en 0 .. i | items [ k ] <= m } // (2) Uno o más elementos vistos hasta ahora coinciden con m donde some { k en 0 .. i | items [ k ] == m } : if items [ i ] > m : m = items [ i ] i = i + 1 // devuelve mLa max()función determina el elemento más grande en una matriz de enteros. Para que esto se defina, la matriz debe contener al menos un elemento. Las poscondiciones de max()requieren que el valor devuelto sea: (1) no menor que ningún elemento; y, (2) que coincida con al menos un elemento. El invariante de bucle se define inductivamente a través de dos wherecláusulas, cada una de las cuales corresponde a una cláusula en la poscondición. La diferencia fundamental es que cada cláusula del invariante de bucle identifica el resultado como correcto hasta el elemento actual i, mientras que las poscondiciones identifican el resultado como correcto para todos los elementos.
Un invariante de bucle puede cumplir uno de los siguientes propósitos:
Para 1., un comentario en lenguaje natural (como // m equals the maximum value in a[0...i-1]en el ejemplo anterior) es suficiente.
Para el caso 2, se requiere compatibilidad con lenguajes de programación, como la biblioteca C assert.h o la invariantcláusula de Eiffel que se muestra arriba. A menudo, la verificación en tiempo de ejecución se puede activar (para ejecuciones de depuración) y desactivar (para ejecuciones de producción) mediante un compilador o una opción de tiempo de ejecución. [ cita requerida ]
Para 3., existen algunas herramientas para apoyar pruebas matemáticas, generalmente basadas en la regla de Floyd-Hoare mostrada anteriormente, de que un código de bucle dado, de hecho, satisface un conjunto de invariantes de bucle dados.
La técnica de interpretación abstracta se puede utilizar para detectar automáticamente invariantes de bucle de un código determinado. Sin embargo, este enfoque está limitado a invariantes muy simples (como 0<=i && i<=n && i%2==0).
El código invariante de bucles consiste en instrucciones o expresiones que se pueden mover fuera del cuerpo de un bucle sin afectar la semántica del programa. Algunos compiladores realizan dichas transformaciones, llamadas movimiento de código invariante de bucles , para optimizar los programas. Un ejemplo de código invariante de bucles (en el lenguaje de programación C ) es
para ( int i = 0 ; i < n ; ++ i ) { x = y + z ; a [ i ] = 6 * i + x * x ; } donde los cálculos x = y+zy x*xse pueden mover antes del bucle, lo que da como resultado un programa equivalente, pero más rápido:
x = y + z ; t1 = x * x ; para ( int i = 0 ; i < n ; ++ i ) { a [ i ] = 6 * i + t1 ; } Por el contrario, por ejemplo, la propiedad 0<=i && i<=nes invariante del bucle tanto para el programa original como para el optimizado, pero no es parte del código, por lo tanto no tiene sentido hablar de "sacarla del bucle".
El código invariante al bucle puede inducir una propiedad invariante al bucle correspondiente. [ aclaración necesaria ] Para el ejemplo anterior, la forma más fácil de verlo es considerar un programa donde el código invariante al bucle se calcula antes y dentro del bucle:
x1 = y + z ; t1 = x1 * x1 ; para ( int i = 0 ; i < n ; ++ i ) { x2 = y + z ; a [ i ] = 6 * i + t1 ; } Una propiedad invariante del bucle de este código es (x1==x2 && t1==x2*x2) || i==0, que indica que los valores calculados antes del bucle coinciden con los calculados dentro del bucle (excepto antes de la primera iteración).