3
$\begingroup$

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

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Aaron Rotenberg Dec 11 '19 at 17:14
3
$\begingroup$

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

| cite | improve this answer | |
$\endgroup$
  • 5
    $\begingroup$ 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. $\endgroup$ – Aaron Rotenberg Dec 10 '19 at 17:54
  • $\begingroup$ @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. $\endgroup$ – Pinocchio Dec 11 '19 at 16:23
  • $\begingroup$ @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. $\endgroup$ – chi Dec 11 '19 at 18:06
  • $\begingroup$ @AaronRotenberg 1) why doesn’t: {Q} x:=e {Q[x/e]} 2) this is not correct because the post condition we want to allow the post condition to be able to have e’s and this does not allow it. 3) { P[e/x] } x:=e {P} this replaces in the pre condition the fact that x holds the value of e, so every place where there was an x we place an e. But this does not necessarily mean we want x to be everywhere because we want this to mean just assigning e to x and not just replacing every instance of e with x. $\endgroup$ – Pinocchio Mar 15 at 21:12
2
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ is this correct? 1) why doesn’t: {Q} x:=e {Q[x/e]} 2) this is not correct because the post condition we want to allow the post condition to be able to have e’s and this does not allow it. 3) { P[e/x] } x:=e {P} this replaces in the pre condition the fact that x holds the value of e, so every place where there was an x we place an e. But this does not necessarily mean we want x to be everywhere because we want this to mean just assigning e to x and not just replacing every instance of e with x.. $\endgroup$ – Pinocchio Mar 15 at 21:11
  • $\begingroup$ @Pinocchio I don't completely understand your questions 2 and 3. BTW, you should make a new question, and ask people to answer that, not a comment. Still, 1) does not hold because that would lead to {x<10}x:=x+3{x+3<10} which is not valid (if x<10 before the assignment, we can't claim x<7 after it). Instead, {x+3<10}x:=x+3{x<10} is valid (if x<7 before the assignment, x<10 after it). $\endgroup$ – chi Mar 16 at 8:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.