{log}: From a Constraint Logic Programming Language to a Formal Verification Tool

Título: {log}: De un lenguaje de Programación Lógica con Restricciones a una Herramienta de Verificación Formal

1. Problema

El trabajo aborda la desconexión histórica entre la programación y la verificación formal. Tradicionalmente, los lenguajes de programación y las especificaciones formales son entes separados, lo que requiere traducciones costosas y propensas a errores, o el uso de anotaciones manuales complejas para verificar propiedades.
Aunque existen herramientas que integran programación y prueba (como Agda, Dafny, F* o Why3), muchas de ellas se basan en tipos dependientes o requieren solvers externos (SMT) y no siempre permiten que el mismo código actúe simultáneamente como programa ejecutable y especificación formal. Además, en el contexto de la Programación Lógica con Restricciones (CLP), escribir código que sea fácil de verificar automáticamente es difícil si el código se aleja de los fragmentos de teoría de conjuntos para los cuales existen procedimientos de decisión.

2. Metodología

Los autores proponen una evolución del lenguaje {log} (pronunciado 'setlog'), originalmente un lenguaje CLP basado en Prolog, transformándolo en un entorno de verificación formal integrado. La metodología se basa en los siguientes pilares:

• Dualidad Programa-Fórmula: En {log}, no existe distinción entre especificación e implementación. El mismo código actúa como programa ejecutable y como fórmula lógica. Esto se logra porque {log} es un solucionador de satisfacibilidad de restricciones que implementa procedimientos de decisión para fragmentos expresivos de la teoría de conjuntos y aritmética entera.
• Lenguaje de Máquinas de Estado: Se define un lenguaje de especificación de máquinas de estado sobre la base de {log}, inspirado en notaciones formales como B y Z. Este lenguaje utiliza lógica de primer orden (FOL), teoría de conjuntos y aritmética entera para definir:
  • Variables de estado.
  • Invariantes (propiedades que deben mantenerse).
  • Operaciones (transiciones de estado).
  • Axiomas y teoremas.
• Integración de Componentes: Se han desarrollado componentes adicionales (implementados en SWI-Prolog) que interactúan con el solucionador central:
  • Entorno Next: Para la ejecución interactiva de escenarios funcionales.
  • Generador de Condiciones de Verificación (VCG): Automatiza la creación de obligaciones de prueba (VC) para invariancia y consistencia.
  • Marco de Pruebas Basado en Modelos (TTF): Genera casos de prueba a partir de la especificación.

3. Contribuciones Clave

El artículo presenta cuatro contribuciones principales que integran {log} en un marco de verificación unificado:

1. Lenguaje Declarativo de Máquinas de Estado: Una sintaxis que permite especificar sistemas como colecciones de predicados lógicos. Las máquinas de estado se escriben en el mismo lenguaje que el programa, eliminando la necesidad de traducciones.
2. Entorno Next y Ejecución Simbólica:
   • Next: Facilita la ejecución de escenarios deterministas y totalmente instanciados, encadenando automáticamente los estados "antes" y "después" de las operaciones. Permite verificar invariantes en cada paso.
   • Ejecución Simbólica: Permite ejecutar especificaciones con variables en lugar de constantes, generando restricciones que describen el comportamiento general del sistema.
3. Generador de Condiciones de Verificación (VCG) y Prueba Automática:
   • Genera automáticamente condiciones de verificación estándar: satisfacción del estado inicial, satisfacibilidad de las operaciones y lemas de invariancia (que cada operación preserva los invariantes).
   • Utiliza el propio motor de {log} como demostrador de teoremas automático.
   • Ofrece mecanismos para analizar condiciones no demostradas (VC), proporcionando contraejemplos (abstractos o concretos) que ayudan al usuario a identificar si la especificación es incorrecta o si faltan hipótesis.
4. Generación de Casos de Prueba (TTF): Implementa el Test Template Framework (TTF) directamente en {log. Utiliza tácticas de prueba (como Forma Normal Disyuntiva y Particiones Estándar) para dividir el espacio de entrada y generar casos de prueba concretos, utilizando al solucionador de {log} para podar especificaciones insatisfacibles y encontrar soluciones.

4. Resultados

• Viabilidad de la Verificación Automática: El sistema ha demostrado ser capaz de verificar propiedades de seguridad y consistencia en varios estudios de caso (incluyendo un sistema de "Libro de Cumpleaños" como ejemplo principal, propiedades de seguridad de muros chinos y modelos de sistemas de tren de aterrizaje).
• Eficiencia en la Detección de Errores: El uso de contraejemplos generados automáticamente ha permitido identificar errores en especificaciones (como invariantes faltantes o precondiciones incorrectas) sin intervención manual extensa.
• Rendimiento: Aunque algunos problemas de teoría de conjuntos son NP-completos, los procedimientos de decisión implementados en {log} han demostrado ser eficaces en la práctica para problemas no triviales, resolviendo la mayoría de las condiciones de verificación en tiempo razonable.
• Integración Unificada: Se ha logrado un flujo de trabajo donde el mismo código se escribe, se ejecuta como prototipo, se verifica formalmente y se utiliza para generar pruebas, todo dentro de un solo entorno y con una sola notación.

5. Significado e Impacto

Este trabajo es significativo porque demuestra que las técnicas de Programación Lógica con Restricciones (CLP) son tan valiosas para la verificación formal como las técnicas provenientes del paradigma de programación funcional (usado en Agda o Dafny).

• Unificación de Abstracción: Al tratar conjuntos y relaciones binarias como ciudadanos de primera clase, {log} eleva el nivel de abstracción de las especificaciones, acercándose a la notación matemática formal.
• Eliminación de Traducciones: A diferencia de otras herramientas que requieren traducir especificaciones a lenguajes intermedios o solvers externos, {log} utiliza un único motor para la ejecución, la prueba y la generación de pruebas. Esto reduce la complejidad y el riesgo de errores de traducción.
• Prototipado y Verificación Simultáneos: La capacidad de ejecutar especificaciones formales como programas funcionales permite a los desarrolladores validar el comportamiento del sistema antes de intentar campañas de prueba formales complejas.
• Futuro: El trabajo sienta las bases para herramientas de verificación más accesibles, aunque los autores reconocen la necesidad de mejorar la automatización en la adición de hipótesis y el soporte para pruebas de refinamiento y lógica de primer orden más avanzada.

En resumen, el artículo presenta {log} no solo como un lenguaje de programación, sino como un sistema de verificación formal integrado que cierra la brecha entre la especificación abstracta y la implementación ejecutable mediante el uso de procedimientos de decisión para la teoría de conjuntos.