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.
C
; so take a look at allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf $\endgroup$