4
$\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$
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$
  • $\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 '12 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 '12 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 '12 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 '12 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$
  • $\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 '12 at 11:51

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.