How to prove the equivalence between Hoare and Floyd assignment axioms?

Question

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?

Answer 1

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.