Definición:
La precondición más débil de un progrmama $S$ respecto de una postcondición $Q$ es el predicado $P$ más débil posible tal que $\{P\}S\{Q\}$.
Notación: $\text{wp}(S,Q)$
Teorema:
Una tripla de Hoare $\{P\}S\{Q\}$ es válida si y sólo si
$$ P \Longrightarrow_L \text{wp}(S,Q) $$
Definiciones anteriores:
Predicado $\text{def } (E)$
Dada una expresión $E$ llamamos $\text{def } (E)$ a las condiciones necesarias para que $E$ esté definida (no se indefina).
Para simplificar asumimos que todas las variables están definidas desde la precondición.
Predicado $Q_E^x$
Dado un predicado $Q$ definimos el predicado $Q_E^x$ que se obtiene reemplazando en $Q$ todas las apariciones libres de la variable $x$ por $E$.
$$ ⁍ $$
$$ \text{wp}(\text{skip},Q) \equiv Q $$
$$ \text{wp}(S1;S2,Q) \equiv \text{wp}\big(S1,\text{wp}(S2,Q)\big) $$
$$ S = \text{if $B$ then $S1$ else $S2$ endif} \\ \text{wp}(S,Q) \equiv \text{def}(B) \land_L \Big(\big(B \land \text{wp}(S1,Q)\big) \lor \big(\lnot B \land \text{wp}(S2,Q)\big)\Big) $$
Teorema derivado del Axioma 4
Si
$$ P \implies \text{def}(B) \land\\ \{P \land B\} \space S1 \space \{Q\} \land \\ \{P \land \lnot B\}\space S2 \space\{Q\} $$
Entonces
$$
\{P\} \space \text{if $B$ then $S1$ else $S2$ endif} \space \{Q\} $$
Definición: