El análisis de complejidad responde cuánto crece el costo de un algoritmo. La correctitud responde otra pregunta: si el algoritmo realmente produce el resultado que promete. Los invariantes ayudan a estudiar esa segunda dimensión, especialmente en algoritmos iterativos.

Después de analizar un algoritmo como Bubble Sort, AALIE puede mostrar una sección de loop invariant. Un invariante de ciclo es una propiedad que se mantiene verdadera antes de iniciar el ciclo y después de cada iteración relevante. Esa propiedad permite razonar sobre por qué el algoritmo progresa correctamente.

La lectura formal se organiza normalmente en tres partes: inicialización, mantenimiento y finalización. La inicialización verifica que la propiedad sea verdadera antes de comenzar. El mantenimiento comprueba que siga siendo verdadera después de una iteración. La finalización conecta el estado al terminar con el objetivo del algoritmo.

• Inicialización: el invariante debe cumplirse antes de ejecutar el ciclo.
• Mantenimiento: si el invariante era cierto antes de una iteración, debe seguir siéndolo después.
• Finalización: cuando el ciclo termina, el invariante debe permitir concluir que el resultado es correcto.

En algoritmos recursivos no se habla de loop invariant en sentido tradicional. En su lugar, se usa una lectura basada en hipótesis inductiva, caso base, pasos recursivos y terminación. Esta idea permite razonar sobre por qué una función recursiva produce resultados correctos para entradas cada vez mayores.

Para Fibonacci, la correctitud inductiva revisa que el caso base esté definido, que las llamadas recursivas avancen hacia valores menores y que la combinación de resultados respete la definición matemática de la sucesión. Si alguna de estas partes falla, el algoritmo puede terminar mal o no terminar.