Now let's test out the rule on a particular hoare triple:
\[
\{?\}\ x := 4\ \{y = x\}
\]
To make the hoare triple valid we would have to use the following precondition:
\[
\vdash \{(x = 4) \to y = x\}\ x := 4\ \{y = x\}
\]
but let's now assume the following initial state:
\[
\sigma _1 = \{x \mapsto 3, y \mapsto 1\}
\]
this does correctly entail our precondition, i.e. we have \(\sigma _1 \vDash P\) as necessary by virtue of vacous truth, then executing the statement we have:
\[
\langle x := 4, \sigma _1 \rangle \Downarrow \sigma _2
\]
In the new context clearly \(x\) is reassigned to 4, thus:
\[
\sigma _2 = \{x \mapsto 4, y \mapsto 1\}
\]
But we can see that clearly \(\sigma _2\) violates our postcondition \(Q\), which is to say, \(\sigma _2 \nvDash (y = x)\). The implication of this is that while the hoare triple is derivable it is not then necessarily also valid, in words this proof rule is unsound.
For completeness let's also provide a proof of soundness. As a reminder soundness states that:
If a hoare triple is derivable using the inference rules of our system, then it is valid (i.e. true in all interpretations.)
Formally we express this as:
\[
\vdash \{P\}\ s\ \{Q\} \to \vDash \{P\}\ s\ \{Q\}
\]
If we instantiate this rule for our hypothetical assignment rule we must demonstrate the following:
\[
\forall \sigma .\ \sigma \vDash (x = e) \to Q \land \exists \sigma '.\ \langle (x := e), \sigma \rangle \Downarrow \sigma ' \to \sigma ' \vDash Q
\]
Let's link the proof of soundness back to the example, so in our inital state \(\sigma _1\) we have that:
\[
\sigma (x) \ \mathrlap {\,/}{=}\ \sigma (y) \equiv 3 \ \mathrlap {\,/}{=}\ 4
\]
Since this means that the equality \(x = 4\) is false we have that implication so the precondition \(P\) is true. This corresponds precisely to the second case where \(\sigma (e) \ \mathrlap {\,/}{=}\ \sigma (x)\). The issue we can then see which naturally follows is that in the new state clearly its the case that:
\[
\sigma _2 = \{x \mapsto 4, y \mapsto 1\} \nvDash (x = y)
\]
In other words we had the case where our precondition was vacuously true thus erroneously implying upon termination the arbitrary \(y = x\) must also hold. Clearly then this proof rule is incorrect as in the case of a vacuous truth we are able to generate unsound hoare triples.
To compare this with the correct assignment rule we have:
\[
\vdash \{P[x \mapsto e]\}\ x := e\ \{P\}
\]
we can notice here that by removing the consequent of the logical implication we ensure that if the assertion of x being substituted / being equal to the expression e before the execution of the statement doesn't hold, then it correctly means that we indeed cannot suggest that after an assignment our assertion \(P\) is somehow correct.