Why is the assignment rule the way it is in Hoare Logic?

Question

Why is the assignment rule the way it is in Hoare Logic/Axiomatic Semantics? I can't wrap my head around why the assignment rule is backwards from what I expected.

I understand Hoare logic is use to prove formal propositions of the state of a program as commands are executed. Thus, if we execute the command $$x:=e$$ I would have expected that the next state has such substitution...but it seems the substitution happens before we execute the assignment which I find bizzare. I would have expected:

$$ \{ P \} x:= e \{P[e/x]\}$$

Given that $P$ are statements about the program state.

I'm sure there is a good explanation for this and sorry if this is a basic question, I know it must be. But can someone explain it to me?

---

Bonus Question:

Why don't we write the assignment rule as:

$$ \{ Q \} x:= e \{Q[x/e]\}$$

note its NOT the same as my original suggestion because we have the $x$ and $e$ swapped around. i.e. in the post condition wherever we have an $e$ we place an $x$ (which is fine because the statement we just execute is that $x$ holds the value of $e$, so we should be able to replace $e$ for $x$ in the post condition if the pre condition help.

---

Related posts that I've read that have not helped:

• Hoare triple for assignment P{x/E} x:=E {P}
• Wikipedia Hoare logic
• https://www.quora.com/unanswered/Why-is-the-assignment-rule-the-way-it-is-in-Hoare-Logic
• https://www.reddit.com/r/ProgrammingLanguages/comments/e8suhh/why_is_the_assignment_rule_the_way_it_is_in_hoare/

---

Appendix:

For us dyslexics, in this question this is what the substitution notation means:

$$ P[e/x] = P[e \to x] $$

i.e. replace every free occurrence of $x$ with expression/term/thingie $e$.

Answer 1

So after reading and thinking about it more this is my explanation (thanks software foundations):

The key confusion for me seems to be the meaning of $P[e/x]$ (replaces every free instance of x with e). What this does is wherever you see the symbol $x$ literally remove it and place $e$. e.g. $ P[e/x] = (x+y+1)[e/x] \to P[e/x] = (e+y+1)$ so notice how $x$ literally disappeared from $P$. So what we want is once we do the assignment:

$$ x:= e$$

that the statement is true if we had $x$ instead of $e$. So if the rule is:

$$ \{ P[e/x] \} x:= e \{ P \}$$

then what we want is, when we plug $x$ for $e$ we want the statement in consideration to be true. So before we started the code we have $P[e/x]$. Then we run the assignment and all instances of $e$ disappear and we get $x$'s to replace them. That must be true if the code that ran was assignment (since $x$ now hold the value $e$, so you can remove $e$'s and place $x$).

Thats the explanation of the abstract concept. Lets (shamelessly) use the software foundations (SF) example:

{{ Y = 1 }} X ::= Y {{ X = 1 }} In English: if we start out in a state where the value of Y is 1 and we assign Y to X, then we'll finish in a state where X is 1. That is, the property of being equal to 1 gets transferred from Y to X.

Another useful paragraph from SF:

Similarly, in {{ Y + Z = 1 }} X ::= Y + Z {{ X = 1 }} the same property (being equal to one) gets transferred to X from the expression Y + Z on the right-hand side of the assignment. More generally, if a is any arithmetic expression, then {{ a = 1 }} X ::= a {{ X = 1 }} is a valid Hoare triple.

---

Addendum from comment's great observation:

it is important to recognize that the rule { P [ e / x ] } x := e { P } allows both the expression e and the variable x to occur in the postcondition. In other words, the inference rule allows you to deduce a postcondition in which any subset of the occurrences of e in the precondition have been replaced with x , including none of them. Moreover, it allows you to deduce all of these different postconditions simultaneously.

---

Reply to bonus why is

1) $ \{P[e/x]\} x:=e \{P\} $

better than

2) $ \{ Q \} x:=e \{Q[x/e]\} $:

Besides the subtle point of replacing x with expressions that might be invisible (e.g. e=0, should we replace $0$ with an infinite number of $x$'s? What if the zeros are not there...the rules should be syntactic but I think it's better to avoid such confusions), I think this is the reason:

What the rule of assignment should capture is that we are assigning the expression e to the variable x. Thus, only x should be "replaced" by e. Intuitively, in the code (or more precisely the state of the program $\sigma$) when x starts holding the value e, it doesn't randomly mean that everywhere where there might be an e it becomes x after executing the assignment $x:=e$. In fact what it does mean is that now in the post condition we have x's. Now those x's if we did not have the assignment should have the value of $e$ i.e. we only "undo" the replacement/assignment the assignment command did. Not every other random expression e. In short, the only way to know where to place the correct e's is by starting in the post condition after the assignment has been done, then starting from there place e's. If we do it backwards we might be replacing e's we didn't want to replace (even if they were probably true, which I guess they should since we are saying x holds the value e after assigning e to x).

Answer 2

Assume we are running program x := e, and let $\sigma$ be the initial state, and $\sigma'$ be the final state.

The crucial intuition here is: the value of $x$ in the final state $\sigma'$ is the same as the value of the expression $e$ in the initial state $\sigma$. Indeed, the latter is the value we assign to $x$ with the command x := e.

Hence, if $P(-)$ is a property on values, the formula $P(\mbox{$x$-in-the-final-state})$ is equivalent to $P(\mbox{$e$-in-the-initial-state})$. In other words $P(x)$ in the postcondition (in state $\sigma'$) is really equivalent to $P(e)$ in the precondition (in state $\sigma$).

Using the substitution is only a more formal way to consider the postcondition as a "formula which depends on $x$", i.e. as $P(x)$, and then requiring $P(e)$ as precondition.