Hoare Calculus Incorrect Assignment Axiom
题
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
没有正确的解决方案