Cheap and Secure Web Hosting Provider : See Now

[Solved]: Hoare Calculus Incorrect Assignment Axiom

, , No Comments
Problem Detail: 

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

Asked By : Nablezen

Answered By : Gilles

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.

Your mistake is in the obviously. In order to prove that the triple is invalid, you need to prove that there is no way to derive it from any combination of the axioms of the Hoare calculus — whether from the assignment axiom alone (perhaps with a strange postcondition) or from that and other axioms. As Andrej Bauer has explained, this tripe is in fact valid in the Hoare calculus.

You can prove that the axiom is invalid by contradiction. However, you'll need to find the contradiction; I don't think this approach leads to an intuitive way of spotting one.

Since the proposed rule is very close to the assignment axiom, let's consider how one might prove it from the assignment axiom, and see where the proof gets difficult. This is often a good way of finding a potential counterexample.

We want to prove that $$\dfrac{}{\{\mathrm{true}\} \; u := t \; \{u=t\}} \tag{A}$$ is valid. The assignment axiom lets us derive any triple of the form $\{P[u \leftarrow t]\} \; u := t \; \{P\}$. Ok, so let's take $P = (u=t)$ to get the right postcondition. So the precondition for this application of the assignment axiom is $P[u \leftarrow t] = (t = t[u \leftarrow t])$. We would like to have the precondition $\mathrm{true}$, which is logically equivalent to $t = t$, but that isn't exactly what we have. The assertion $t = t[u \leftarrow t]$ is $t = t$ only when the variable $u$ doesn't appear in $t$. What if it does?

This suggests a counterexample where the variable $u$ appears in the expression $t$. For example, let's take $t$ to be the expression $u+1$, i.e. the instance of the proposed axiom $(A)$ is $\{\mathrm{true}\} \; u := u + 1 \; \{u = u + 1\}$. The precondition is always true, whereas the postcondition is always false, so a calculus that allows us to derive this triple is inconsistent. Therefore the axiom schema $(A)$ is invalid.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/29586

3.2K people like this

 Download Related Notes/Documents

0 comments:

Post a Comment

Let us know your responses and feedback