Bucle invariante

Bucle invariable  - en programación  - una expresión lógica que es verdadera después de cada paso del cuerpo del bucle (después de la ejecución del operador fijo ) y antes del inicio del bucle, dependiendo de las variables que cambian en el cuerpo del bucle. [1] Los invariantes se utilizan en la teoría de la verificación de programas para probar la corrección del resultado obtenido por un algoritmo cíclico.

Definición

Una invariante de bucle es una expresión matemática (normalmente una igualdad) que inevitablemente incluye al menos algunas variables cuyos valores cambian de una iteración del bucle a la siguiente. El invariante se construye de tal manera que sea verdadero inmediatamente antes del inicio de la ejecución del bucle (antes de entrar en la primera iteración) y después de cada una de sus iteraciones. Además, si el invariante incluye variables definidas solo dentro del ciclo (por ejemplo, el contador de ciclos foren Pascal o Ada ), entonces para ingresar al ciclo se toman en cuenta con los valores que recibirán en el momento de la inicialización.

Prueba de la corrección del ciclo usando el invariante

El procedimiento para probar la operatividad del ciclo con la ayuda de un invariante es el siguiente:

  1. Se prueba que la expresión del invariante es verdadera antes del comienzo del ciclo.
  2. Se prueba que la expresión de la invariante se mantiene verdadera después de la ejecución del cuerpo del ciclo; así, por inducción, se prueba que al final de todo el ciclo, se satisfará el invariante.
  3. Se prueba que si la invariante es verdadera, después de completar el ciclo, las variables tomarán exactamente los valores que se requiere obtener (esto se determina elementalmente a partir de la expresión de la invariante y los valores finales conocidos de las variables, en las que se basa la condición para terminar el ciclo).
  4. Se prueba (quizás sin aplicar la invariante) que el ciclo terminará, es decir, la condición de terminación se cumplirá tarde o temprano.
  5. La verdad de las afirmaciones demostradas en las etapas anteriores indica sin ambigüedad que el bucle se ejecutará en un tiempo finito y dará el resultado deseado.

Los invariantes también se utilizan en el diseño y optimización de algoritmos cíclicos . Por ejemplo, para asegurarse de que el bucle optimizado sigue siendo correcto, basta con demostrar que no se viola la invariante del bucle y que se puede lograr la condición de terminación del bucle.

Notas

  1. ↑ VV Borisenko. Fundamentos de Programación (enlace no disponible) . CONOCE Intuit . Consultado el 18 de junio de 2013. Archivado desde el original el 20 de mayo de 2012.