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

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

$\endgroup$

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.