# Hoare triple for assignment P{x/E} x:=E {P}

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?

## 3 Answers

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.

• 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?? – zell May 16 '12 at 14:18
• Correct; Hoare triple says "if", not "iff". It is only in this particular case that iff holds. – Charles Fu May 16 '12 at 15:13
• 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? – zell May 16 '12 at 17:29
• 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. – Charles Fu May 16 '12 at 17:39

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.

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.

• 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? – zell May 16 '12 at 11:51