$(**$ The assignment rule looks backward to almost everyone the first

time they see it$.$ If it still seems puzzling to you, it may help

to think a little about alternative "forward" rules. Here is a

seemingly natural one:

$------------------------------($hoare$\_$asgn$\_$wrong$)$

$\{\{$ True $\}\}$ X :$=$ a $\{\{$ X $=$ a $\}\}$

Give a counterexample showing that this rule is incorrect and use

it to complete the proof below, showing that it is really a

counterexample. $($Hint: The rule universally quantifies over the

arithmetic expression $[$a$],$ and your counterexample needs to

exhibit an $[$a$]$ for which the rule doesn't work.$)*)$

Theorem hoare$\_$asgn$\_$wrong : exists a:aexp,

~ $\{\{$ True $\}\}$ X :$=$ a $\{\{$ X $=$ a $\}\}.$

Proof.

Admitted.

$(*$ FILL IN HERE

$[]*)$