expl045

Por la regla de la asignación, deberá cumplirse que $R_{z}^{z^2} \wedge (z<1)$ o $R_{z}^{z+2} \wedge \neg (z<1)$ .

$R_{z}^{z^2}\equiv\{z^2\geq 0\}$ y $R_{z}^{z+2}\equiv\{z+2\geq 0\}$, por lo que se cumplirá $(z^2\geq 0 \wedge z<1) \vee (z+2\geq 0 \wedge z\geq 1)$.

Como $\forall z.z^2\geq 0$ la primera conjunción sería $\cierto\wedge z<1$ o, lo que es lo mismo, z<1

En cuanto a la segunda conjunción, aplicando la negación y restando 2 a ambos lados de la desigualdad, queda $((z>-2)\wedge (z\geq 1))$

Como $z\geq 1 \Rightarrow z+2\geq 0$, se puede eliminar el conjuntante menos restrictivo, de manera que queda $z\geq 1$.

Así, la disyunción completa sería $z<1 \vee z\geq 1$, que es equivalente a

De la precondición encontrada se deduce que cualquiera que sea el valor previo de z, el valor después de ejecutar la sentencia cumplirá la postcondición señalada.