1
$\begingroup$

I'm having trouble proving Hoare logic questions as I'm not sure of the process that is taken to prove them. I understand that they're rules such as assignment axiom, pre-condition strengthening, post-condition weakening etc... but how you actually apply these rules to the question is a little out of my understanding.

Cheers

photo of question

$\endgroup$
  • $\begingroup$ Mathematical proof is a creative act. In general, there aren't recipes that you can just follow. I'm voting to close this question as too broad -- at the moment, you're just asking for a tutorial on Hoare logic, which could easily be a textbook chapter or even a whole book. If you can narrow it down to something more specific, that would make a better question. $\endgroup$ – David Richerby Feb 5 '18 at 0:30
  • $\begingroup$ It may help to play around with such things in a programming language such as C; so take a look at allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf $\endgroup$ – Musa Al-hassy Feb 27 '18 at 14:37
1
$\begingroup$

Usually one starts from the postcondition ($s=2^i$ in your example) and tries to compute a (weakest) precondition, walking the code backwards. At the very last step, after having computed a precondition for the whole code, one tries to strengthen it to obtain precisely the given precondition, completing the task.

For instance, starting from $s=2^i$, we can find a precondition for s:=s*2, which according to the assignment rule is $(s=2^i)\{s*2/s\} = (s*2=2^i)$. This must, in turn, be the postcondition to i:=i+1, so we repeat the process, using the assignment rule once again.

You should now get the idea, at least for chains of assignments.

For conditional it is a bit more complex. For loops, it is far more complex, and requires finding a suitable invariant. There is no general automatic procedure to infer a loop invariant, similarly to how there is no general automatic procedure to find a mathematical proof. Still, in many cases, it is possible to guess a working invariant -- how to do so, at least in common cases, is a skill that (arguably) each computer scientist should learn, especially when focusing on program verification or algorithms.

$\endgroup$
1
$\begingroup$

Here is the idea behind proving this triple. Let us denote by $s_0,i_0$ the values before the block, and by $s_1,i_1$ the values after the block. We are given that $s_0 = 2^{i_0}$, and furthermore it is clear that $i_1 = i_0 + 1$ and $s_1 = 2s_0$. But then $$ s_1 = 2s_0 = 2\cdot 2^{i_0} = 2^{i_0+1} = 2^{i_1}. $$ Whether this constitutes a proof of not depends on your normative environment.

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