Programación basada en invariantes

La programación basada en invariantes ^{[ 1 ]} es una metodología de programación donde las especificaciones y los invariantes se escriben antes de las instrucciones del programa. Escribir los invariantes durante el proceso de programación tiene varias ventajas: requiere que el programador explicite sus intenciones sobre el comportamiento del programa antes de implementarlo, y los invariantes se pueden evaluar dinámicamente durante la ejecución para detectar errores de programación comunes. Además, si son suficientemente robustos, los invariantes se pueden usar para demostrar la corrección del programa basándose en la semántica formal de las instrucciones. Generalmente, se requiere un lenguaje combinado de programación y especificación, conectado a un potente sistema de prueba formal, para la verificación completa de programas no triviales. En este caso, también es posible un alto grado de automatización de las pruebas.

En la mayoría de los lenguajes de programación existentes , las principales estructuras organizativas son los bloques de control de flujo , como forbucles y sentencias . Estos lenguajes pueden no ser ideales para la programación basada en invariantes, ya que obligan al programador a tomar decisiones sobre el flujo de control antes de escribir los invariantes. Además, la mayoría de los lenguajes de programación no ofrecen un buen soporte para escribir especificaciones e invariantes, puesto que carecen de operadores cuantificadores y, por lo general, no permiten expresar propiedades de orden superior.whileif

La idea de desarrollar el programa junto con su demostración se originó con EW Dijkstra . De hecho, escribir invariantes antes de las instrucciones del programa ha sido considerado de diversas formas por MH van Emden, JC Reynolds y RJ Back .

• Eiffel (lenguaje de programación)