Cyclic Proofs in Hoare Logic and its Reverse

Aquí presento un resumen técnico detallado del artículo "Cyclic Proofs in Hoare Logic and its Reverse" (Pruebas Cíclicas en la Lógica de Hoare y su Dual), basado en el documento proporcionado.

1. Problema y Contexto

La lógica de Hoare es el marco formal estándar para especificar y razonar sobre la corrección de programas informáticos. Tradicionalmente, se formula como un sistema de prueba axiomático donde las reglas para bucles (while) requieren que el demostrador invente explícitamente:

• Invariantes de bucle: Para la corrección parcial (garantizar que si el programa termina, satisface la postcondición).
• Medidas de terminación bien fundadas: Para la corrección total (garantizar además que el programa termina).

La búsqueda de estas invariantes y medidas es un obstáculo significativo para la automatización de la verificación de programas.

Por otro lado, existe el Reverse Hoare Logic (Lógica de Hoare Inversa) o Incorrectness Logic, que se centra en demostrar la presencia de comportamientos específicos (reachability) o errores, en lugar de su ausencia.

El problema central abordado en este trabajo es la falta de un tratamiento unificado y sistemático de las versiones parcial y total tanto de la Lógica de Hoare estándar como de su dual (Lógica de Hoare Inversa) utilizando sistemas de prueba cíclica. Los sistemas cíclicos permiten representar pruebas como árboles de derivación infinitos pero regulares (con "backlinks" o enlaces hacia atrás), eliminando la necesidad de invariancias explícitas en favor de condiciones de sonido global sobre la estructura de la prueba.

2. Metodología

Los autores desarrollan y comparan cuatro sistemas lógicos:

1. PHL: Lógica de Hoare Parcial.
2. THL: Lógica de Hoare Total.
3. PRHL: Lógica de Hoare Inversa Parcial.
4. TRHL: Lógica de Hoare Inversa Total.

La metodología se basa en los siguientes pasos:

• Definición Semántica: Se define un lenguaje de programación simple tipo while y se establecen las semánticas operacionales (pequeños pasos) para definir la validez de las triples de Hoare y Reverse Hoare.
• Sistemas Axiomáticos: Se presentan los sistemas de prueba estándar para los cuatro casos, destacando las reglas de bucle que requieren invariantes y medidas de terminación.
• Sistemas de Prueba Cíclica: Se reformulan los sistemas anteriores en un estilo de "continuación" ({P} C; C' {Q}), donde los bucles se descomponen mediante una regla de desdoblamiento (unfolding) única.
  • Condición de Sonido Global (Parcial): Para PHL y PRHL, se requiere que cualquier camino infinito en la prueba contenga infinitas aplicaciones de reglas de ejecución simbólica. Esto asegura que un contraejemplo hipotético correspondería a una ejecución infinita, contradiciendo la naturaleza finita de un contraejemplo de corrección parcial.
  • Condición de Sonido Global (Total): Para THL y TRHL, se añade la condición de que debe existir una traza infinitamente progresiva (infinitely progressing trace) de medidas bien fundadas a lo largo de los caminos infinitos. Esto garantiza que cualquier contraejemplo hipotético implicaría una cadena descendente infinita de valores naturales, lo cual es imposible.
• Traducción y Complejidad: Se demuestra la completitud relativa mediante una transformación explícita de pruebas axiomáticas estándar a pruebas cíclicas, mostrando que cualquier prueba válida en el sistema axiomático puede convertirse en una prueba cíclica válida.

3. Contribuciones Clave

1. Unificación Simétrica: El trabajo revela una simetría profunda entre la Lógica de Hoare y su dual.
   • Las condiciones de sonido para las versiones parciales (PHL y PRHL) son esencialmente coinductivas (basadas en la existencia de ejecuciones infinitas).
   • Las condiciones de sonido para las versiones totales (THL y TRHL) son esencialmente inductivas (basadas en la disminución de medidas bien fundadas).
2. Formulación de PRHL: Los autores introducen y formalizan la Lógica de Hoare Inversa Parcial (PRHL), una variante que, aunque semánticamente dual a la corrección total, no estaba tan bien explorada en la literatura previa como sus contrapartes.
3. Sistemas Cíclicos para Lógica Inversa: Se presentan por primera vez sistemas de prueba cíclica completos para la Lógica de Hoare Inversa (tanto parcial como total), demostrando que las condiciones de sonido necesarias son análogos naturales de las de la lógica estándar.
4. Pruebas de Sonido y Completitud: Se proporcionan demostraciones directas de la sonoridad (soundness) de los sistemas cíclicos y de su completitud relativa mediante la traducción desde los sistemas axiomáticos.

4. Resultados Principales

• Teorema de Sonoridad (4.7 y 5.5): Se demuestra que si una triple tiene una prueba cíclica en cualquiera de los cuatro sistemas (PHL, THL, PRHL, TRHL), entonces es válida semánticamente. La prueba se basa en la construcción de un camino infinito en la prueba pre-cíclica que contradice las condiciones de sonido global (ya sea por la falta de ejecución infinita o por la existencia de una cadena descendente infinita).
• Teorema de Completitud Relativa (4.9 y 5.7): Se demuestra que si una triple es demostrable en el sistema axiomático estándar, entonces es demostrable en el sistema cíclico correspondiente. Esto se logra mediante un algoritmo de traducción que transforma el árbol de prueba finito (axiomático) en un árbol cíclico (con backlinks) preservando la validez.
• Relaciones de Dualidad: Se confirma que:
  • PRHL y THL son duales semánticos.
  • TRHL y PHL son duales semánticos.
  • Los sistemas de prueba cíclicos comparten reglas estructurales, diferenciándose únicamente en las condiciones de sonido global aplicadas a los caminos infinitos.

5. Significado e Impacto

Este trabajo es significativo por varias razones:

• Clarificación Teórica: Proporciona una visión unificada y clara de las relaciones entre corrección parcial/total y lógica directa/inversa, mostrando cómo los sistemas de prueba cíclica pueden manejar todas estas variantes con un conjunto de reglas casi idéntico.
• Potencial para Automatización: Al eliminar la necesidad de inventar invariantes y medidas de terminación explícitas (reemplazándolas por condiciones de estructura de prueba), los sistemas cíclicos abren nuevas vías para la búsqueda automática de pruebas y la detección de errores (bug detection) mediante herramientas como el demostrador de teoremas Cyclist.
• Fundamento para Incorrectness Logic: Al formalizar la lógica de Hoare Inversa en un marco cíclico, se fortalece la base teórica para la lógica de incorrectness, que es fundamental para la verificación de seguridad y la detección de vulnerabilidades.
• Novedad en PRHL: La formalización de la versión parcial de la lógica inversa llena un vacío en la taxonomía de lógicas tipo Hoare, ofreciendo una herramienta teórica para razonar sobre la posibilidad de divergencia o comportamientos parciales en contextos de "reachability".

En resumen, el artículo demuestra que la teoría de pruebas cíclicas es un marco robusto y flexible capaz de abarcar tanto la corrección tradicional como la lógica de incorrectness, unificando sus fundamentos bajo condiciones de sonido globales coherentes.