1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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.'' $\endgroup$ – Musa Al-hassy Jun 26 '18 at 14:40
1
$\begingroup$

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.

$\endgroup$

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.