En informática , un ciclo invariante es una propiedad de un ciclo de programa que es verdadera antes (y después) de cada iteración. Es una aserción lógica , a veces verificada dentro del código mediante una llamada de aserción . Conocer sus invariantes es esencial para comprender el efecto de un bucle.
En la verificación formal de programas , particularmente el enfoque de Floyd-Hoare , los invariantes de bucle se expresan mediante la lógica de predicado formal y se utilizan para probar las propiedades de los bucles y mediante algoritmos de extensión que emplean bucles (generalmente 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 las 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 verse 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 esta implementación. Un artículo de encuesta [1] cubre algoritmos fundamentales de muchas áreas de la informática (búsqueda, clasificación, optimización, aritmética, etc.), caracterizando cada uno de ellos desde el punto de vista de su invariante.
Debido a la similitud de los bucles y los programas recursivos , probar la corrección parcial de los bucles con invariantes es muy similar a probar la corrección de los programas recursivos mediante inducción . De hecho, el invariante de bucle es a menudo el mismo que la hipótesis inductiva que se va a probar para un programa recursivo equivalente a un bucle dado.
Ejemplo informal
La siguiente subrutina C devuelve el valor máximo en su matriz de argumentos , siempre que su longitud sea al menos 1. Los comentarios se proporcionan 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 tanto, describen una propiedad invariante del bucle. Cuando se alcanza la línea 13, este invariante aún se mantiene y se sabe que la condición de 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[]
n
i!=n
m
a[0...n-1]
int max ( int n , const int a []) { int m = a [ 0 ]; // m es igual al valor máximo en un [0 ... 0] int i = 1 ; mientras que ( i ! = n ) { // m es igual al valor máximo en un [0 ... i-1] si ( m < a [ i ]) m = a [ i ]; // m es igual al valor máximo en un [0 ... i] ++ i ; // m es igual al valor máximo en un [0 ... i-1] } // m es igual al valor máximo en a [0 ... i-1], e i == n return m ;}
Siguiendo un paradigma de programación defensiva , la condición de bucle i!=n
en la línea 5 debería modificarse mejor a i
n
. Si bien este cambio en el código intuitivamente no debería hacer una diferencia, el razonamiento que conduce a su corrección se vuelve algo más complicado, ya que solo i>=n
se conoce en la línea 13. Para obtener que también se i<=n
cumpla, esa condición debe incluirse en el ciclo. invariante. Es fácil ver que i<=n
también es un invariante del bucle, ya que i
i<=n
mantiene en la línea 11 después de que i
se haya incrementado en la línea 10. Sin embargo, cuando los invariantes de bucle deben proporcionarse manualmente para la verificación formal del programa, a i<=n
menudo se pasan por alto propiedades tan obvias intuitivamente como .
Lógica de Floyd-Hoare
En la lógica de Floyd-Hoare , [2] [3] la corrección parcial de un bucle while se rige por la siguiente regla de inferencia:
Esto significa:
- Si alguna propiedad es preservado por el código —Más precisamente, si tiene después de la ejecución de siempre que ambos y sostenido de antemano— (línea superior) luego
- y se garantiza que son falsos y verdaderos, respectivamente, después de la ejecución de todo el ciclo , previsto era cierto antes del bucle (línea inferior) .
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 con los estados de la máquina. Se mantiene siempre que se parte de un estado en el que la expresión booleana es cierto y ejecuta con éxito un código llamado , la máquina termina en un estado en el que es verdad. Si se puede probar esta relación, la regla nos permite concluir que la ejecución exitosa del programa saldrá de un estado en el que es fiel a un estado en el que sostiene. La fórmula booleana en esta regla se denomina invariante de bucle.
Ejemplo
El siguiente ejemplo ilustra cómo funciona esta regla. Considere el programa
mientras (x <10) x: = x + 1;
Entonces se puede probar el siguiente triple de Hoare:
La condición C del while
bucle es. Un invariante de bucle útiltiene que adivinarse; resultará quees apropiado. Bajo estos supuestos es posible probar el siguiente triple de Hoare:
Si bien este triple se puede derivar formalmente de las reglas de la asignación lógica de Floyd-Hoare, también se justifica intuitivamente: el cálculo comienza en un estado en el que es cierto, lo que significa simplemente que es verdad. El cálculo suma 1 a, Lo que significa que sigue siendo cierto (para el entero x).
Bajo esta premisa, la regla para while
bucles permite la siguiente conclusión:
Sin embargo, la poscondición (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 otro invariante del ciclo de ejemplo, y la propiedad trivial es otro. Aplicando la regla de inferencia anterior a los rendimientos invariantes anteriores. Aplicarlo a invariante rendimientos , que es un poco más expresivo.
Soporte de lenguaje de programación
Eiffel
El lenguaje de programación Eiffel proporciona soporte nativo para invariantes de bucle. [4] Un invariante de bucle se expresa con la misma sintaxis utilizada para un invariante de clase . En el ejemplo siguiente, la expresión invariante de bucle x <= 10
debe ser verdadera después de la inicialización del bucle y después de cada ejecución del cuerpo del bucle; esto se comprueba en tiempo de ejecución.
desde x : = 0 invariante x <= 10 hasta x > 10 bucle x : = x + 1 final
Mientras
El lenguaje de programación Whiley también proporciona soporte de primera clase para invariantes de bucle. [5] Los invariantes de bucle se expresan mediante una o más where
cláusulas, como se ilustra a continuación:
function max ( int [] items ) -> ( int r ) // Requiere al menos un elemento para calcular max requiere | artículos | > 0 // (1) El resultado no es más pequeño que cualquier elemento asegura todo { i en 0 .. | artículos | | items [ i ] <= r } // (2) El resultado coincide con al menos un elemento asegura que algún { i en 0 .. | artículos | | items [ i ] == r } : // nat i = 1 int m = items [ 0 ] // while i < | artículos | // (1) Ningún elemento visto hasta ahora es más grande que m donde todos { k en 0 .. i | items [ k ] <= m } // (2) Uno o más elementos vistos hasta ahora coincide con m donde algunos { k en 0 .. i | items [ k ] == m } : si items [ i ] > m : m = items [ i ] i = i + 1 // devuelve m
La 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 condiciones posteriores de max()
requerir que el valor devuelto es: (1) no es menor que cualquier elemento; y, (2) que coincide con al menos un elemento. El invariante de bucle se define inductivamente a través de dos where
cláusulas, cada una de las cuales corresponde a una cláusula en la condición posterior. La diferencia fundamental es que cada cláusula del ciclo invariante identifica el resultado como correcto hasta el elemento actual i
, mientras que las poscondiciones identifican el resultado como correcto para todos los elementos.
Uso de invariantes de bucle
Un ciclo invariante puede servir para uno de los siguientes propósitos:
- puramente documental
- para ser verificado dentro del código mediante una llamada de aserción
- para ser verificado en base al enfoque de Floyd-Hoare
Para 1., un comentario en lenguaje natural (como // m equals the maximum value in a[0...i-1]
en el ejemplo anterior ) es suficiente.
2. Para, la programación de soporte de idioma se requiere, como la C biblioteca assert.h , o el anterior -mostrado invariant
cláusula en Eiffel. A menudo, la verificación en tiempo de ejecución puede activarse (para depurar ejecuciones) y desactivarse (para ejecuciones de producción) mediante un compilador o una opción de ejecución. [ cita requerida ]
Para 3., existen algunas herramientas para respaldar demostraciones matemáticas, generalmente basadas en la regla de Floyd-Hoare mostrada anteriormente , de que un código de ciclo dado satisface de hecho un (conjunto de) invariantes de ciclo determinados.
La técnica de interpretación abstracta se puede utilizar para detectar automáticamente un bucle invariante de un código dado. Sin embargo, este enfoque se limita a invariantes muy simples (como 0<=i && i<=n && i%2==0
).
Distinción del código invariante de bucle
Un bucle invariante ( propiedad de bucle invariante ) debe distinguirse del código invariante de bucle ; observe "invariante de bucle" (sustantivo) versus "invariante de bucle" (adjetivo). El código invariante de bucle consta de declaraciones o expresiones que se pueden mover fuera del cuerpo de un bucle sin afectar la semántica de un programa; tales transformaciones, llamadas movimiento de código invariante en bucle , son realizadas por algunos compiladores para optimizar programas. Un ejemplo de código invariante en bucle (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+z
y x*x
se pueden mover antes del ciclo, lo que resulta en 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 ; }
En contraste, por ejemplo, la propiedad 0<=i && i<=n
es un ciclo invariante tanto para el programa original como para el optimizado, pero no es parte del código, por lo que no tiene sentido hablar de "sacarlo del ciclo".
El código invariante de bucle puede inducir una propiedad invariante de 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 del ciclo se calcula tanto antes como dentro del ciclo:
x1 = y + z ; t1 = x1 * x1 ; para ( int i = 0 ; i < n ; ++ i ) { x2 = y + z ; a [ i ] = 6 * i + t1 ; }
Una propiedad invariante de ciclo de este código es (x1==x2 && t1==x2*x2) || i==0
, lo que indica que los valores calculados antes del ciclo coinciden con los calculados dentro (excepto antes de la primera iteración). [ cita requerida ]
Ver también
Referencias
- ^ Carlo A. Furia, [Bertrand Meyer] y Sergey Velder. "Invariantes de bucle: análisis, clasificación y ejemplos". Encuestas de computación de ACM. vol. 46, no. 3 de febrero de 2014 ( [1]
- ^ Robert W. Floyd (1967). "Asignación de significados a los programas" (PDF) . En JT Schwartz (ed.). Actas de simposios en matemáticas aplicadas . Aspectos matemáticos de la informática. 19 . Providence, RI: Sociedad Matemática Estadounidense. págs. 19–32.
- ^ Hoare, CAR (octubre de 1969). "Una base axiomática para la programación informática" (PDF) . Comunicaciones de la ACM . 12 (10): 576–580. doi : 10.1145 / 363235.363259 . Archivado desde el original (PDF) el 4 de marzo de 2016.
- ↑ Meyer, Bertrand , Eiffel: The Language, Prentice Hall , 1991, págs. 129-131.
- ^ Pearce, David J .; Groves, Lindsay (2015). "Diseño de un compilador de verificación: lecciones aprendidas del desarrollo de Whiley" . Ciencia de la Programación de Computadores . 113 : 191–220. doi : 10.1016 / j.scico.2015.09.006 .
Otras lecturas
- Thomas H. Cormen , Charles E. Leiserson , Ronald L. Rivest y Clifford Stein . Introducción a los algoritmos , segunda edición. MIT Press y McGraw-Hill, 2001. ISBN 0-262-03293-7 . Páginas 17-19, sección 2.1: Ordenación por inserción.
- David Gries . " Una nota sobre una estrategia estándar para desarrollar bucles invariantes y bucles ". Science of Computer Programming , vol 2, págs. 207–214. 1984.
- Michael D. Ernst, Jake Cockrell, William G. Griswold, David Notkin. " Descubrir dinámicamente invariantes probables del programa para respaldar la evolución del programa ". Conferencia internacional sobre ingeniería de software , págs. 213–224. 1999.
- Robert Paige. " Programación con invariantes ". Software IEEE , 3 (1): 56–69. Enero de 1986.
- Yanhong A. Liu, Scott D. Stoller y Tim Teitelbaum . Fortalecimiento de invariantes para una computación eficiente . Science of Computer Programming , 41 (2): 139-172. Octubre de 2001.
- Michael Huth, Mark Ryan. " Lógica en Ciencias de la Computación ", Segunda Edición.