2
$\begingroup$

I would like to prove that the following Hoare triple is correct by giving a full Hoare logic proof. (Assuming all variables are real.) How can I do so?

$$\{c = 0\} ~ a := −c; ~ b := a + c; ~ c := a ~ \{ab = c\}$$


My Attempt using the assignment, concatenation, and weakening rules: $$ \{c = 0\} \Rightarrow \{\} \iff \{-c(-c + c) = -c\}$$ $$a := −c;$$ $$\{a(a + c) = a\}$$ $$b := a + c;$$ $$\{ab = a\}$$ $$c := a$$ $$\{ab = c\}$$

$\endgroup$
  • $\begingroup$ Frankly speaking, I have difficult to unserstand... If $c=0$ and we set $a=-c$, also $a$ must be $0$. $\endgroup$ – Mauro ALLEGRANZA Apr 23 '17 at 10:17
  • $\begingroup$ Now, setting $b=a+c$ we get again $0$. $\endgroup$ – Mauro ALLEGRANZA Apr 23 '17 at 10:17

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.