0
$\begingroup$

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

$\endgroup$
  • $\begingroup$ For reference, here is the Assignment axiom: en.wikipedia.org/wiki/Hoare_logic#Assignment_axiom_schema $\endgroup$ – Andrej Bauer Sep 2 '14 at 9:10
  • 1
    $\begingroup$ You should also state whether $t$ is a variable or any expression. If $t$ is an expression, you should state whether $u$ is allowed to appear in $t$. $\endgroup$ – Andrej Bauer Sep 2 '14 at 9:11
  • $\begingroup$ Your question already includes a complete answer to the original problem but no question about this answer. Thus, only "yes/no" answers may remain, helping neither you nor future visitors. Please read related meta discussions here and here and adjust your question accordingly, e.g. by formulating a specific question about a single element of your answer you are uncertain about. If you just want general feedback, you are welcome to visit us in Computer Science Chat. $\endgroup$ – Raphael Sep 2 '14 at 10:57
  • $\begingroup$ What is the OP supposed to ask if he thinks he has a correct solution but just wants someone to have a look at what he did, as is the case here? $\endgroup$ – Andrej Bauer Sep 2 '14 at 11:04
0
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

Your solution is incorrect because you did not reach a contradiction. You claim that you reached a contradiction with the Assignment axiom. For this to be true, you must produce the negation of an instance of the axiom.

The axiom of assignment states that $$\{P[e/x]\} \; x \mathbin{:=} e \; \{ P \}$$ In your example we would have $u$ instead of $x$, $t$ instead of $e$, and $P$ would be the statement $u = t$, which gives us the following instance of the axiom $$\{ t = t \} \; u \mathbin{:=} t \; \{ u = t \}$$ You seem to think this is in contradiction with $$\{ t = u + 1\} \; u \mathbin{:=} t \; \{ u = t \}$$ but that is a logical error. In fact, the axiom of assignment implies your statement:

  1. $\{ t = t \}\; u \mathbin{:=} t \; \{ u = t \}$ (instance of the axiom of assignment, as above)
  2. $\{ t = u + 1 \}\; u \mathbin{:=} t \; \{ u = t \}$ (weakening of the precondition because $t = u + 1 \Rightarrow t = t$.)

Hint: to solve the exercise, consider the possibility that the expression $t$ contains $u$.

$\endgroup$
  • $\begingroup$ I actually just stated the exercise as it was, apparently the exercise assumed somewhat implicitly that t was an expression and that u was allowed to be a part of it(something i rejected completely initially). Also thanks for pointing out the flaw in my reasoning, i understand what went wrong and will post another attempt in a minute. $\endgroup$ – Nablezen Sep 2 '14 at 9:42
  • $\begingroup$ Sorry, but I still don't seem to quite get it. Considering your last post, I'm confused up to the point that I think I could actually PROVE the new axiom in the Hoare Calculus using the Assignment Axiom. For example: $$ \forall P, t, u\ holds:\ (P[t/u] \implies t = t)\ |\ (Weaken\ Precondition)$$ $$\{t=t\}\ u:= t\ \{ u = t\}\ |\ (Regular\ Assignment\ Axiom) $$ Where is my mistake? Any additional help will be greatly appreciated. Greetings. $\endgroup$ – Nablezen Sep 2 '14 at 11:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.