How to prove $c = a + b$ using Program Verification Techniques

Question

I am trying to prove an elementary thing, but it seems at some point you get down to atoms where you can't prove anything else. This is why I am wondering about proving $c = a + b$, it seems like an atom.

\begin{align} \{a, b\}\\ c = a + b\\ \{a, b, c = a + b\} \end{align}

This is my attempt at a Hoare assertion. It says "given $a$ and $b$, if I assign $c$ to $a + b$, then I end up with $a$ and $b$ unchanged, and $c$ assigned to $a + b$." That is, it's saying "if I do $c = a + b$, then I end up with $c = a + b$," which feels reduntant. In addition, this seems hard to formalize in programming. If the form is $\{P_1\}\ Q\ \{P_2\}$, then $Q$ and the $c$ part of $P_2$ is the same code, namely $c = a + b$. So I don't see there being any need to write an assertion for addition, we can just state it's properties (that it returns a number) and it is proven by definition. That is, it's an axiom.

Wondering if this is true, or where I am missing something. Because when I tried writing this out in software I end up with basically what it looks like in that definition of the Hoare assertion above, $c = a + b$ twice.

Answer 1

We can prove the Hoare triple

\begin{align} \{{\sf true}\}\\ c = a + b\\ \{c = a + b\} \end{align}

using the assignment rule. We take the postcondition $c = a + b$ and we substitute backwards $\{(a+b)/c\}$, so we get $(c = a + b)\{(a+b)/c\} = (a+b=a+b)$. That's the weakest precondition. Hence, we proved

\begin{align} \{a+b = a+b\}\\ c = a + b\\ \{c = a + b\} \end{align}

We can then use the weakening/strengthening/pre-post rule to rewrite $a+b=a+b$ as $\sf true$, since they are equivalent logical formulae.