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

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:

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

• The $P[e/x]$ notation is not just a problem for people with dyslexia. It's 50/50 whether a given author uses this to mean "substitute $e$ for all occurrences of $x$" or "substitute $x$ for all occurrences of $e$". You always have to check the definitions in the particular text you are reading. Same with $P[e \rightarrow x]$ – you can read this as "assign $e$ to $x$" or as "replace $e$ with $x$", getting opposite results depending on which way you read it. – Aaron Rotenberg Dec 11 '19 at 17:14

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.

• You write "Then we run the assignment and all instances of $e$ disappear and we get $x$'s to replace them." But 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. – Aaron Rotenberg Dec 10 '19 at 17:54
• @AaronRotenberg oh wow! That is super subtle. I was about to comment that Why don't we write the assignment rule as: $$\{ Q \} x:= e \{Q[x/e]\}$$ which it isn't correct, for the reason you outlined (i.e. my rule replaces all instances of $e$ with $x$ but we might not want that. In other words, the post condition is allowed to have $e$'s. So in the pre-condition we must only substitute $e$'s for $x$'s and leave other $e$'s alone. I don't know if I will remember this subtle point but its crucial. – Pinocchio Dec 11 '19 at 16:23
• @Pinocchio Yes, and the rule you propose could be fooled by adding some silly "$+0$" inside an occurrence of $e$ in $Q$. E.g. we can write $x+0+y$ instead of $e = x+y$. Doing so we get an equivalent expression to $e$, but one which is not affected by the substitution $[x/e]$. That's why we usually like to substitute variables with expressions, but not the other way around. – chi Dec 11 '19 at 18:06

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.