5
$\begingroup$

I am trying to understand Hoare logic presented at Wikipedia, Hoare logic at Wikipedia Apparently, if I understand correctly, a Hoare triple $$\{P\}~ C ~\{Q\}$$ means

if P just before C, then Q holds immediately after C, as long as C terminates. (A)

However, the assignment axiom schema seems to be interpreted in a different way:

$$\frac{}{\{P[x/E]\} ~~x:=E~~ \{P\}}$$

The wikipedia says:

The assignment axiom means that the truth of $\{P[x/E]\}$ is equivalent to the after-assignment truth of $\{P\}$. Thus were $\{P[x/E]\}$ true prior to the assignment, by the assignment axiom, then $\{P\}$ would be true subsequent to which. Conversely, were $\{P[x/E]\}$ false prior to the assignment statement, $\{P\}$ must then be false consequently.

I think the Hoare triple only affirms that if P[x/E] before x:=E, then P(x) holds after x:=E. It DOES NOT affirm, by its definition, that if P(x) holds after x:=E, then P[x/E] holds before x:=E.

My naive question is, how can $\{P[x/E]\}$ before the assignment can be equivalent to $\{P\}$ after the assignment? Does this contradict with point (A) at the beginning of my post?

$\endgroup$

3 Answers 3

6
$\begingroup$

Notice that what Wikipedia is saying is that

The assignment axiom means that the truth of $\{P[x/E]\}$ is equivalent to the after-assignment truth of $\{P\}$.

In other words, ($P$ holds after the execution of $x:= E$) if ($P[x/E]$ holds before the execution). This is equivalent to the definition $A$ you provided, which is generally a more intuitive definition for Hoare triple.

$\endgroup$
4
  • $\begingroup$ Thanks for this precision. However, I think the Hoare triple only affirms that if P[x/E] before x:=E, then P(x) holds after x:=E. It DOES NOT affirm, by its definition, that if P(x) holds after x:=E, then P[x/E] holds before x:=E. Am I right?? $\endgroup$
    – zell
    May 16, 2012 at 14:18
  • $\begingroup$ Correct; Hoare triple says "if", not "iff". It is only in this particular case that iff holds. $\endgroup$
    – Charles Fu
    May 16, 2012 at 15:13
  • $\begingroup$ Thanks. If I understand well, your "in other words (P holdes after ) if and only if (... before ....) part is wrong. Can I remove the "änd only if"part? $\endgroup$
    – zell
    May 16, 2012 at 17:29
  • $\begingroup$ Right, As I understand it, "equivalent" means "iff" in the original quote. But for clarity I think it's a good idea to just say "if". I've modified my answer. $\endgroup$
    – Charles Fu
    May 16, 2012 at 17:39
3
$\begingroup$

It seems that the wording of the Wikipedia text is flakey to some extent:

The assignment axiom means that the truth of {P[x/E]} is equivalent to the after-assignment truth of {P}.

The assignment axiom does not mean that. It only means that the truth of {P[x/E]} implies the after-assignment truth of {P}. It does not mean the "equivalence".

However, the equivalence is also a valid fact. It is just that the Hoare axiom for assignment doesn't say it.

A good source for a clear and rigorous treatment of Hoare-like proof systems is Apt and Olderog's Verification of Sequential and Concurrent Programs.

$\endgroup$
2
$\begingroup$

It means more something like

if P was true before C then Q will be true after that.

There are time considerations because usually C will change the environment.

Think of this example: $C=(x := 42)$ and $P=(x > 10)$. Then the instance of your rule makes sense.

EDIT: time considerations are important. Here, $P$ where "$x=E$" (i.e. after) is equivalent to $P[x/E]$ (before). Note that "$x=E$" is just to designate the "after": it is not a real equality since $x$ can appear in $E$.

For example

$$ \{ 0 +42>10\} ~~ x:=0 ~~ \{ x+42>10 \}$$ $$ \{ x + 42 > 10\} ~~ x:=x+42 ~~ \{ x>10 \}$$

can help you prove that

$$ \{ \mbox{true} \} ~~ x:=0 ~;~ x := x + 42 ~~ \{ x>10 \}$$

On a side note, I personally found the notation $P[x/E]$ very confusing.

$\endgroup$
1
  • $\begingroup$ Thanks, I had forgotten to put that precision. My question is more about the assignment. I don't see why P[x/E] before x:=E should be equivalent to P(x) as stated in Wikipadia, because the original definition of Hoare triple does not imply that I suppose? $\endgroup$
    – zell
    May 16, 2012 at 11:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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