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

Problem Detail: 

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?

Asked By : zell

Answered By : Charles Fu

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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/1864