Fortaleza lógica de una aserción

Definición

Una aserción $R$ es más fuerte que $S$ si todo estado que satisface $R$ también satisface $S$; equivalentemente, $R\Rightarrow S$ es válida.

Intuición

Una condición más fuerte es más restrictiva y admite menos estados. Debilitar una condición permite más estados.

Formulación

Si $[[P]]$ es el conjunto de estados que satisfacen $P$:

$$R\Rightarrow S⟺[[R]]\subseteq [[S]].$$

$\perp$ es la aserción más fuerte y $\top$ la más débil.

Ejemplo mínimo

$$i>5\Rightarrow i>0,i>0\nRightarrow i>5.$$

false  ->  i > 5  ->  i > 0  ->  true
más fuerte                         más débil

Contraejemplo o límites

La implicación no suele ser reversible. $y=4\Rightarrow y\ne 0$, pero $y\ne 0$ permite muchos valores distintos de $4$.

Aplicación práctica

Si una prueba hacia atrás calcula $wlp(C,Q)$, la precondición declarada $P$ basta exactamente cuando

$$P\Rightarrow wlp(C,Q).$$

Esa implicación es una condición de verificación. Practica la comparación de condiciones en los ejercicios graduados.

Relaciones

• Compara: aserciones de programa.
• Fundamenta: Regla de consecuencia de Hoare.
• Permite comparar una precondición declarada con la precondición más débil.

Procedencia

• Clase: Ternas de Hoare y demostración formal.
• Fuente: Programación Avanzada Notas 4 2027, diapositivas 11–15 (láminas 65–69).