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

Question

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?

Answer 1

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.

Answer 2

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.

Answer 3

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.