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

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.

• In general to prove $\forall x, \exists y, R(x,y)$, you construct a program with with immutable constant $x$ and mutable variable $y$ such that your program assigns a value to $y$ so that $R(x,y)$ is true after the program has completed execution. This is also known as Curry-Howard Correspondence.'' Jun 26, 2018 at 14:40

## 1 Answer

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.