Last year, I got the assignment to work through The Calculus of Computation by Bradley & Manna. The result is — in my humble opinion — a neat introduction to static reasoning for imperative languages. If you are new to that, but know a bit about predicate logic, then it might be a short and hopefully nice read to you.
Heuristics Methods for Inductive Invariant Generation in Pi explains the basics such as weakest precondition and strongest postcondition, why it is important to have inductive assertions for loops, why they are hard to find (hard as in undecidably-hard), and further what heuristics we could apply to simple standard cases to generate inductive assertions automatically.
If you enjoy it (or hate it), leave me a comment. Now, I finally found the blogger.com option to notify me, when new comments come in, so that I have a chance to reply.
Comments