5
$\begingroup$

$\small\textit{''The obvious things are the most difficult to understand''}$

May be the question does not make sense, but let me ask it anyway.

The Hoare assignment axiom is $$ \dfrac{}{\{Q[v \mapsto expr]\} \;\; v:=expr \;\; \{Q\}} $$

Is there an intuitive explanation of the axiom?

I "agree" with the Floyd assignment axiom: $$ \dfrac{}{\{Q\} \;\; v:=expr \;\; \{\exists old: Q(old,..) \land v=expr(old,...)\}} $$ which can be thought as "if Q holds before the assignment, then after the assignment we know that the variables should satisfy: 1) Q(old) holds for some old variables (since we assume Q holds), 2) variable v has the new valueexpr(old,...)".

Is there a similar intuition for the Hoare assignment axiom?

$\endgroup$
  • $\begingroup$ |-{Q[e/x]} x:=e{Q} One way to think about it could be: if you know that the property Q holds for the expression e (that is Q[e/x] holds), then if you assign e to x then the property has to hold for x (that is Q holds). e flows into the variable x so x inheritates what held for e before the assignment. $\endgroup$ – sh0t Aug 17 at 23:23
6
$\begingroup$

Hoare Logic proceeds backwards. It is a method to compute a precondition such that the desired postcondition holds. In fact, the inference rules given in your standard Hoare Logic deductions compute weakest preconditions, or the most "specific" precondition that still guarantees that the post-condition holds at the next program point.

I think this is the salient difference. There's no comparable interpretation (of reasoning about the next program point) for backwards predicate transformers because we have to reason about the "state" before an operation given that we know its "state" after. In comparison, the alternative axiom reasons about the postcondition given a precondition.

Now, the two axioms are duals of each other, in the sense that the backwards axiom computes a weak precondition while the forward axiom computes a strong postcondition (most "general" postcondition such that all possible postconditions are subsumed). Logically, they are equivalent. Therefore, not only do we have a singular backwards intuition of the Hoare axiom, but we should also have some sort of connections between the intuitions behind the backwards axioms and those behind the forward axioms.

  • The intuition behind the backwards axiom: This is actually relatively easy to see, given that you know what the deduction system is doing. Let's look at the Hoare assignment rule: $$ \frac{}{\{P : Q [x \mapsto e]\} ~x = e ~\{Q\}} $$ which roughly says that the weakest precondition of $Q$ preceding an assignment $x = e$ is just $Q$ with every occurrence of $x$ replaced by the expression $e$. To see this in action, say you have the goal $Q = (x^2 = 4)$ and you want to see if $x = 3$ satisfies this goal. Well, the assignment axiom tells us that we should transform this post-condition into $(x^2 = 4)[x \mapsto 3] \to (9 = 4) \equiv \bot$, which says that there is no precondition that can get us to the goal. On the other hand, a goal of $Q = (x^2 = 9)$ allows us to compute a weakest precondition of $(9 = 9) \equiv \top$, so any precondition will satisfy this program.
  • The connection between the forward and backward systems: Recall that we said that the two deduction systems are duals of each other. In other words, given a deduction (in the form of an inference rule) in the forward system, we can infer a similar deduction (in the backward system) by joining the leaves/exit points of this tree together, and inverting the proof. In other words, there's a (rough) correspondence. Suppose that the forward system is characterized by the rule function $F$, such that $F(\{\phi_1, \dots\}) e$ returns the set of propositions that might hold after executing $e$ given that we know $\{\phi_1, \dots\}$ before hand. Similarly, we also have a backwards rule function $B$, such that $B(\{\psi_1, \dots\}) e$ returns the set of propositions that must be true before $e$ so that $\{\psi_1, \dots\}$ holds afterwards. We can see that $$ Q = B(F(Q)) $$ (though the other direction $Q = F(B(Q))$ does not necessarily hold, since $B$ can produce $\bot$ and $F(\bot) = \bot$)
$\endgroup$
  • $\begingroup$ Thanks you for detailed answer. You write "The intuition behind the axiom.. this is easy to see.. the axiom tells us" --- but can you describe the intuition without referring to the axiom?:) In other words -- is it possible to justify the axiom without using "this is because the axiom tells us.."? $\endgroup$ – Ayrat Nov 22 '16 at 11:00
2
$\begingroup$

The precondition is in fact the weakest (liberal) precondition that guarantees a valid Hoare triple for that postcondition and assignment statement. ("liberal" because termination is not considered.) So what does this precondition express? The precise condition that has to hold if we "undo" the assignment but want the postcondition: everything in the state is the same except for the value of the variable we assign to.

So maybe alluding to a common "undo" operation can connect to your students' understanding.

$\endgroup$
0
$\begingroup$

What about just considering a simple case? Let Q: x != y, v: x, expr: 3. Then if 3 != y before executing x := 3, then x != y afterwards. Can you see why (and an example which would fail if you e.g. exchange pre- and postconditions in the rule)?

$\endgroup$
  • $\begingroup$ yes, I considered examples, incl. those that show that other versions of the axiom fail:) But in the end, when you present this axiom in the lecture, no matter how many examples you consider, the question remains: "why? why is so un-intuitive?" (students really struggle with this, as do myself.) $\endgroup$ – Ayrat Nov 22 '16 at 10:03
  • $\begingroup$ To your question Can you see why?. I would pretend that this is because: "to make x!=y fail, we need x==y after the assignment. This is possible only if x is assigned to y (or other way). But we assign x to 3. Hence in the end x!=y". $\endgroup$ – Ayrat Nov 22 '16 at 10:17

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.