Hoare Calculus Incorrect Assignment Axiom
Question
I'm currently preparing for an exam and recently came across the following exercise and would like to know whether my solution would be correct.
Exercise: Prove that the following axiom is not correct in the Hoare Calculus:
{true} u:= t {u=t}
My Proof via Reductio ad absurdum:
Assumption:
Axiom is valid Hoare Calculus Axiom and therefore agrees with the other Axioms.
Proof:
Consider the Hoare Triple: {t = u+1} u:=t {u = t}
This triple is obviously invalid because it does not agree with the Assignment Axiom of the Hoare Calculus.
However, given our Assumption, we can derive it as a valid triple:
(t= u+1) => (true) (Weaken Precondition)
{true} u:=t {u=t} (Axiom of the Assumption)
=> {t = u+1} u:=t {u=t} <- contradiction! => Assumption was false, Axiom is not correct.
q.e.d
No correct solution