Example Two

$\langle \; \rangle \; a := b \; \langle a = b \rangle$ is totally correct for any choice of state space $X_1$x$X_1$. Here $\langle \;\rangle$ is called the empty precondition, equivalent to $\langle$   true$\rangle$ - it is always satisfied.