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
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
