Example Three

Pick $X = \mathbb{Z}$, the integers.

$$\langle \; \rangle \;$$   while$$(P \geq 1)\{P := P + 1 \; \langle P < 1 \rangle$$

is partially correct (as if $P < 1$, the entry condition is not satisfied and if $P \geq 1$ it does not terminate). But

$$\langle P < 1 \rangle \;$$   while$$(P \geq 1)\{P := P + 1 \; \langle P < 1 \rangle$$

is totally correct.