Regla de consecuencia de Hoare

Definición

Regla que permite reemplazar la precondición de una terna por una condición más fuerte y su postcondición por una más débil.

Intuición

Si un programa funciona para un conjunto de entradas, funciona para cualquier subconjunto. Si garantiza una salida precisa, también garantiza cualquier consecuencia menos exigente.

Formulación

$$\frac{P^{\prime }\Rightarrow P\{P\}C\{Q\}Q\Rightarrow Q^{\prime }}{\{P^{\prime }\}C\{Q^{\prime }\}}.$$

Ejemplo mínimo

y = 4 implica y != 0
{y != 0} x := 1/y {x = 1/y}
--------------------------------
{y = 4}  x := 1/y {x = 1/y}

También, de $max=b\Rightarrow max\ge b$, se pasa de la postcondición exacta a la más débil.

Contraejemplo o límites

Las direcciones importan: debilitar la precondición o fortalecer la postcondición exige una demostración adicional y no se obtiene con esta regla.

Regla mnemotécnica

• Antes: se permite pedir más al estado inicial: $P^{\prime }\Rightarrow P$.
• Después: se permite prometer menos: $Q\Rightarrow Q^{\prime }$.

En una prueba completa, estas implicaciones se convierten en condiciones de verificación. Véase el procedimiento paso a paso.

Relaciones

• Se aplica a: Terna de Hoare.
• Usa: Fortaleza lógica de una aserción.
• Simplifica resultados de: Axioma de asignación de Hoare.

Procedencia

• Clase: Ternas de Hoare y demostración formal.
• Fuente: Programación Avanzada Notas 4 2027, diapositivas 16–19 (láminas 70–73).
• Fuente complementaria: /Users/diegovillalba/Downloads/AllLectures.pdf, páginas PDF 21–23.