Regla de composición de Hoare

Definición

Regla que demuestra una secuencia (C_1;C_2) conectando la postcondición del primer fragmento con la precondición del segundo:

$$\frac{\{P\}{C}_1\{R\}\{R\}{C}_2\{Q\}}{\{P\}{C}_1;C_2\{Q\}}.$$

(R) es la aserción intermedia.

Intuición

El estado final de (C_1) es el estado inicial de (C_2). Si (C_1) garantiza (R) y (C_2) funciona siempre que (R) sea cierta, la secuencia completa transforma (P) en (Q).

Ejemplo mínimo

$$\{\top \}c:=a+b\{c=a+b\},$$ $$\{c=a+b\}c:=c/2\left\{c=\frac{a+b}{2}\right\}.$$

Por composición:

$$\{\top \}c:=a+b;c:=c/2\left\{c=\frac{a+b}{2}\right\}.$$

Contraejemplo o límites

No se pueden concatenar dos ternas si la postcondición de la primera no garantiza la precondición de la segunda. En ese caso se ajustan las aserciones mediante la regla de consecuencia o se busca otra condición intermedia.

Ejercicio rápido

Para x:=x+1; y:=2*x y meta $y\ge 10$, la condición intermedia antes de la última asignación es $x\ge 5$ y la precondición inicial es $x\ge 4$. El desarrollo completo está en Secuencias paso a paso.

Relaciones

• Compone: ternas de Hoare.
• Las condiciones intermedias suelen obtenerse con: precondiciones más débiles.
• Para asignaciones utiliza: axioma de asignación.
• Ajusta condiciones con: regla de consecuencia.

Procedencia

• Clase: Composición, invariantes y condicionales de Hoare.
• Fuente: Programación Avanzada Notas 5, diapositivas 3–8 (láminas 84–89).
• Fuente complementaria: /Users/diegovillalba/Downloads/AllLectures.pdf, páginas PDF 24–25.