# Elementary Hoare logic proof

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\}$$

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