Example

The trippe $\langle \; \rangle \; y := x^2 \; \langle y \geq 0 \rangle$ is correct by the Assignment Rule (if state space is $\mathbb{R}$x$\mathbb{R}$), since we get weakest precondition $\langle x^2 \geq 0 \rangle \; (=) \; \langle \; \rangle$. Hence so is $\langle x > -10 \rangle \; y := x^2 \; \langle y \geq -5 \rangle$.