Regla condicional de Hoare

Definición

Regla que demuestra un condicional separando los estados que satisfacen (B) de los que satisfacen (\neg B). Cada camino debe garantizar una postcondición común (Q).

Formulación

Con else:

$$\frac{\{P\wedge B\}{C}_1\{Q\}\{P\wedge \neg B\}{C}_2\{Q\}}{\{P\}\text{if }B\text{ then }{C}_1\text{ else }{C}_2\{Q\}}.$$

Sin else, la rama falsa equivale a skip:

$$\frac{\{P\wedge B\}{C}_1\{Q\}(P\wedge \neg B)\Rightarrow Q}{\{P\}\text{if }B\text{ then }{C}_1\{Q\}}.$$

Intuición

(B) y (\neg B) cubren todos los resultados de evaluar la condición. Si ambos caminos terminan satisfaciendo (Q), el condicional completo garantiza (Q).

Ejemplo mínimo

$$\{\top \}\text{if }max<a\text{ then }max:=a\{max\ge a\}.$$

• Si (max<a), la asignación deja (max=a).
• Si (\neg(max<a)), ya se cumple (max\ge a).

Contraejemplo o límites

Verificar solo la rama con asignación es insuficiente. En un if sin else, el camino falso conserva el estado y debe satisfacer (Q) por implicación. La regla no prueba que evaluar (B) esté definido ni que las ramas terminen.

Lista de comprobación

1. Escribir la guarda $B$ y su negación $\neg B$.
2. Agregar $P$ a las dos ramas.
3. Calcular las precondiciones de cada cuerpo hacia atrás.
4. Verificar que las dos ramas llegan a la misma $Q$.

Ejemplo resuelto: valor absoluto paso a paso.

Relaciones

• Verifica: ternas de Hoare con bifurcación.
• Usa dentro de las ramas: axioma de asignación.
• Ajusta condiciones con: regla de consecuencia.
• Se integra en: verificación formal.

Procedencia

• Clase: Composición, invariantes y condicionales de Hoare.
• Fuente: Programación Avanzada Notas 5, diapositivas 13–19 (láminas 94–100).
• Fuente complementaria: /Users/diegovillalba/Downloads/AllLectures.pdf, páginas PDF 26–27 y 61–62.