Weakest precondition

Remarks

Example: for the assignment $x := E$, one has $\mathrm{wp}(x := E, Q) = Q[E/x]$, the substitution of $E$ for $x$ in $Q$, provided $E$ is always defined. So $\mathrm{wp}(x := x - 3,\ x > 0)$ is $x - 3 > 0$, that is, $x > 3$. Property 1 holds since from $x > 3$ the new value is positive, and property 2 holds since any state with $x \le 3$ ends with $x \le 0$.

Non-example: the predicate $x > 5$ satisfies property 1 for $x := x - 3$ and $x > 0$, but not property 2, since $x = 4$ also works. So $x > 5$ is a precondition but not the weakest one.

Other standard rules are $\mathrm{wp}(C_1; C_2, Q) = \mathrm{wp}(C_1, \mathrm{wp}(C_2, Q))$ and $\mathrm{wp}(\mathsf{if}\ B\ \mathsf{then}\ C_1\ \mathsf{else}\ C_2, Q) = (B \land \mathrm{wp}(C_1, Q)) \lor (\lnot B \land \mathrm{wp}(C_2, Q))$. For a loop, $\mathrm{wp}$ is a least fixed point and in practice is approximated with an invariant. The weakest liberal precondition $\mathrm{wlp}(C, Q)$ drops the termination requirement and matches partial correctness: the Hoare triple $\set{P}\, C\, \set{Q}$ is valid exactly when $P$ implies $\mathrm{wlp}(C, Q)$.