1
$\begingroup$

How to show that these two axioms are equivalent:

1: $\{G[v/e]\} v:=e \{G\}$

2: $\{F\} v:=e \{\exists v' (F[v/v'] \land v=e[v/v'])\}$

I've tried with $G = \exists v' (F[v/v'] \land v=e[v/v']) $and then I get $G[v/e] = F$, but when I try $F = G[v/e]$ then from $\exists v' (F[v/v'] \land v=e[v/v'])$ I can't obtain $G$.

Is that even correct way to approach this proof?

Thanks!

p.s. There was a question already, but isn't answered: How to show equivalence of the Hoare assignment axiom vs Floyd assignment axiom?

$\endgroup$
3
$\begingroup$

but when I try $F = G[v/e]$ then from $\exists v' (F[v/v'] \land v=e[v/v'])$ I can't obtain $G$.

We can assume $v'$ not free in $G$. Then, we have

$$ \begin{array}{ll} & \exists v' (F[v/v'] \land v=e[v/v']) \\ \iff & \mbox{\{def. $F$\}}\\ & \exists v' (G[v/e][v/v'] \land v=e[v/v']) \\ \iff & \mbox{\{property of $H[v/-][v/-]$\}}\\ & \exists v' (G[v/(e[v/v'])] \land v=e[v/v']) \\ \iff & \mbox{\{replacing equals with equals\}}\\ & \exists v' (G[v/v] \land v=e[v/v']) \\ \iff & \mbox{\{$[v/v]$ has no effect\}}\\ & \exists v' (G \land v=e[v/v']) \\ \iff & \mbox{\{$v'$ not free in $G$\}}\\ & G \land \exists v' (v=e[v/v']) \\ \implies & \mbox{\{logic\}}\\ & G \end{array} $$

The crucial step is to realize that any $v$ which occurs free in $G[v/e]$ is a $v$ that originated from $e$. Hence, $G[v/e][v/t] = G[v/(e[v/t])]$.

Also note that we don't get exactly $G$ but a slightly stronger postcondition. Since postconditions can be weakened, this is not an issue.

$\endgroup$
  • $\begingroup$ thank you very much @chi! Could you please now clarify me why now these two proofs are sufficient to show the equivalence of axioms? $\endgroup$ – Martin Matak Oct 17 '17 at 14:03
  • $\begingroup$ @MartinMatak Well, the point is that you can show that whatever can be proved by an axiom, it can proved without as long as you have the other axiom. You do that by proving that you can replace each use of Hoare's axiom (on any given $G$) with a combined use of Floyd's (on $F$ taken as above, depnding on the given $G$), and weakening. Then you have to prove the other direction (which you say you have already done). Essentially any application of any axiom can be "simulated" using the other one (plus other rules). $\endgroup$ – chi Oct 17 '17 at 16:18

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.