La importancia de la enseñanza del invariante en la estructura

Abstract

La característica más importante de la programación imperativa es la estructura iterativa (while, until, for). Apuntar a mostrar y enseñar una técnica formal que permita construir dicha estructura asegurando su correctitud y aportando la forma de documentarla y verificarla es el objetivo de este trabajo. Es conveniente expresar un problema en términos de un modelo formal, basado en reglas comprobables. Casi cualquier campo de la matemática, u otra ciencia, puede ser utilizado como ayuda para modelar el dominio de un problema. Una vez hallado un modelo adecuado, se trata de establecer una solución para el problema, ajustada a ese modelo.

El objetivo de este trabajo es presentar una manera formal para calcular y desarrollar una iteración cuidando hasta el último detalle, brindando una profunda comprensión de los programas y siendo una tarea mucho más fácil y rápida de verificación y corrección de la estructura mencionada.

La técnica consiste en imaginar congelar la computación en un punto crucial y dar una descripción estática del estado interno. De esta manera la técnica se completa especificando la situación de alguna forma lógica para obtener un Invariante de bucle. La importancia del mismo radica en que, con práctica, los alumnos podrán reconocer, diseñar e implementar bucles perfectamente documentados y verificados.