how to solve Hoare logic problems

Question

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

Answer 1

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.

Answer 2

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.