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?

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top