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

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top