2
$\begingroup$

I know from several sources that they are equivalent, but couldn't find a reasonable explanation. My first approach was to show their equivalence by using the logical consequence rule and both axioms, but I couldn't figure out a reasonable solution.

Here is the exact problem definition:

enter image description here

Anybody can give me a hint how to show that both axioms are indeed equivalent?

$\endgroup$
  • $\begingroup$ As a first step, try applying each axiom to obtain the other, i.e. for given $F$, apply the Hoare axiom to $G:=\exists v'(F[v/v']\wedge v=e[v/v'])$, and for given $G$, apply the Floyd axiom to $F:=G[v/e]$. Can you show that the resulting pre-/postcondition are equivalent to $F$ and $G$, respectively? $\endgroup$ – Klaus Draeger May 5 '15 at 17:52
  • 1
    $\begingroup$ We prefer that you not use images for critical content of your post (e.g., the problem definition). This makes your question harder to search and inaccessible to the visually impaired; we don't like that. Please transcribe text and mathematics (note that you can use LaTeX). $\endgroup$ – D.W. May 6 '15 at 0:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.