104. Lógica de Hoare y lógica dinámica

Idea central

La lógica de Hoare nació para demostrar que un programa hace lo que debe. Floyd («Assigning meanings to programs», 1967) propuso anotar los diagramas de flujo con aserciones lógicas en cada punto. Hoare («An axiomatic basis for computer programming», 1969) convirtió esa idea en un sistema axiomático cuyas fórmulas son ternas \(\{P\}\ C\ \{Q\}\): si \(P\) vale antes de ejecutar \(C\) y \(C\) termina, entonces \(Q\) vale después. Pratt («Semantical considerations on Floyd–Hoare logic», 1976) vio que cada programa \(\alpha\) puede tratarse como una modalidad \([\alpha]\) («después de toda ejecución de \(\alpha\)»), con semántica de Kripke en la que los mundos son estados y las relaciones de accesibilidad son las ejecuciones. Fischer y Ladner (1979) definieron la lógica dinámica proposicional (PDL). El gesto común es tratar las acciones como objetos lógicos de primera clase, junto a las proposiciones.

Principios, axiomas y reglas de inferencia

Lógica de Hoare (corrección parcial, para un lenguaje de asignación, composición, condicional y bucle):

• Asignación: \(\{Q[e/x]\}\ x := e\ \{Q\}\). Para que \(Q\) valga tras asignar \(e\) a \(x\), antes debe valer \(Q\) con \(e\) en lugar de \(x\).
• Composición: de \(\{P\}\ C_1\ \{R\}\) y \(\{R\}\ C_2\ \{Q\}\), inferir \(\{P\}\ C_1; C_2\ \{Q\}\).
• Condicional: de \(\{P \land B\}\ C_1\ \{Q\}\) y \(\{P \land \neg B\}\ C_2\ \{Q\}\), inferir \(\{P\}\ \mathtt{if}\ B\ \mathtt{then}\ C_1\ \mathtt{else}\ C_2\ \{Q\}\).
• Bucle con invariante: de \(\{P \land B\}\ C\ \{P\}\), inferir \(\{P\}\ \mathtt{while}\ B\ \mathtt{do}\ C\ \{P \land \neg B\}\).
• Consecuencia: de \(P \to P'\), \(\{P'\}\ C\ \{Q'\}\) y \(Q' \to Q\), inferir \(\{P\}\ C\ \{Q\}\).

Las aserciones se escriben en un lenguaje de primer orden sobre los tipos de datos. El sistema es correcto. No puede ser completo en sentido absoluto, porque las implicaciones de la regla de consecuencia pueden ser verdades aritméticas no demostrables; Cook (1978) probó su completitud relativa: es completo si se dispone de todas las verdades del lenguaje de aserciones y este es expresivo. La corrección total (que además el programa termine) exige una variante del bucle con una función de cota decreciente.

Ejemplo. Para \(C \equiv x := x + 1\) y \(Q \equiv x > 0\), el axioma de asignación da \(\{x + 1 > 0\}\ C\ \{x > 0\}\), y por consecuencia \(\{x \geq 0\}\ C\ \{x > 0\}\).

Lógica dinámica proposicional (PDL). Programas construidos a partir de programas atómicos con:

• \(\alpha ; \beta\) (composición), \(\alpha \cup \beta\) (elección no determinista), \(\alpha^*\) (iteración un número finito de veces), \(A?\) (prueba: sigue si \(A\) es verdadera).

Semántica: cada programa \(\alpha\) denota una relación \(R_\alpha\) entre estados; \(w \models [\alpha]A\) si \(A\) vale en todo \(v\) con \(w R_\alpha v\), y \(\langle \alpha \rangle A := \neg[\alpha]\neg A\). La terna de Hoare equivale a \(P \to [\alpha]Q\), y \(\mathtt{while}\ B\ \mathtt{do}\ C\) se define como \((B?; C)^*; \neg B?\).

Axiomas (Segerberg, 1977; completitud de Parikh, 1978), con modus ponens y necesitación para cada \([\alpha]\):

• Tautologías clásicas y \([\alpha](A \to B) \to ([\alpha]A \to [\alpha]B)\).
• \([\alpha ; \beta]A \leftrightarrow [\alpha][\beta]A\).
• \([\alpha \cup \beta]A \leftrightarrow ([\alpha]A \land [\beta]A)\).
• \([B?]A \leftrightarrow (B \to A)\).
• \([\alpha^*]A \leftrightarrow (A \land [\alpha][\alpha^*]A)\).
• Inducción: \((A \land [\alpha^*](A \to [\alpha]A)) \to [\alpha^*]A\).

Metateoremas. PDL tiene la propiedad del modelo finito (vía la clausura de Fischer y Ladner), es decidible y su satisfacibilidad es EXPTIME-completa (cota inferior de Fischer y Ladner, superior de Pratt). No es compacta: \(\{\langle \alpha^* \rangle p\} \cup \{\neg\langle \alpha \rangle^n p : n \in \mathbb{N}\}\) es finitamente satisfacible pero no satisfacible, por la iteración. La lógica dinámica de primer orden, con asignaciones, es mucho más compleja (\(\Pi^1_1\)-completa en la semántica estándar).

Genealogía

La lógica de Hoare usa como lenguaje de aserciones la lógica de primer orden clásica: las condiciones de Floyd y Hoare son fórmulas sobre variables del programa. Pratt la reinterpretó en términos de la lógica modal con semántica de Kripke, lo que convirtió un cálculo para programas en una lógica modal multimodal con modalidades estructuradas. Hacia adelante, Pnueli (1977) extendió la verificación al estilo de Floyd y Hoare a programas concurrentes y reactivos con la lógica temporal; la lógica epistémica dinámica tomó de PDL las modalidades de acción y sus constructores (composición, elección, iteración); y la lógica de la separación de Reynolds y O’Hearn extendió las ternas de Hoare con aserciones sobre la memoria dinámica.

Contexto y relevancia

La lógica de Hoare fue la respuesta teórica a la «crisis del software» de finales de los sesenta y sigue siendo la base de la verificación formal: el cálculo de precondiciones más débiles de Dijkstra (1975), los verificadores automáticos y los asistentes de prueba para programas descienden de ella. PDL se convirtió además en modelo general de las lógicas de la acción y del cambio, en filosofía y en inteligencia artificial. Para la pregunta «¿una lógica o muchas?», muestra que la lógica puede ampliarse con objetos que no son proposiciones (programas y acciones) sin tocar la lógica clásica de base. La pluralidad aparece aquí como especialización: hay lógicas para dominios, no rivales de la clásica.

Fuentes

• Hoare, C. A. R. «An axiomatic basis for computer programming». Communications of the ACM 12 (1969): 576–580, 583.
• Fischer, M. J. y Ladner, R. E. «Propositional dynamic logic of regular programs». Journal of Computer and System Sciences 18 (1979): 194–211.
• Harel, D., Kozen, D. y Tiuryn, J. Dynamic Logic. Cambridge (Mass.): MIT Press, 2000.
• Apt, K. R. «Ten years of Hoare’s logic: a survey, part I». ACM Transactions on Programming Languages and Systems 3 (1981): 431–483.

← Índice de lógicas