how to solve Hoare logic problems

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

• 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. Feb 5, 2018 at 0:30
• 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 Feb 27, 2018 at 14:37

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.

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.