Reglas de conjunción y disyunción de Hoare

Definición

Reglas que combinan dos ternas demostradas para el mismo código, reuniendo sus precondiciones y postcondiciones mediante conjunción o disyunción.

La conjunción acumula garantías cuando ambas hipótesis son válidas; la disyunción reúne dos casos alternativos ya demostrados.

\frac{{ P _{1} } C { Q _{1} } { P _{2} } C { Q _{2} }}{{ P _{1} \land P _{2} } C { Q _{1} \land Q _{2} }},

\frac{{ P _{1} } C { Q _{1} } { P _{2} } C { Q _{2} }}{{ P _{1} \lor P _{2} } C { Q _{1} \lor Q _{2} }} .

si se demostró {P1} C {Q1} y {P2} C {Q2}:
    bajo P1 y P2, conservar Q1 y Q2
    bajo P1 o P2, conservar Q1 o Q2

Para i := i+1, combinar la relación $i = i_{0} + 1$ con la preservación de positividad permite derivar $i > 1$ cuando $i_{0} > 0$ .

Las dos premisas deben referirse al mismo comando $C$ . Además, i=i+1 es ambigua si no se diferencia el valor anterior $i_{0}$ del posterior.

Para ver cómo estas reglas encajan con asignaciones, secuencias y ramas, consulta la guía paso a paso.

Clase: Ternas de Hoare y demostración formal.
Fuente: Programación Avanzada Notas 4 2027, diapositivas 20–22 (láminas 74–76).

tags	concepto, programacion, logica-de-hoare, inferencia
aliases	Regla de conjunción de Hoare, Regla de disyunción de Hoare