I was introduced to formal reasoning about programs in an introductory course on algorithms and data structures in March. Most of the curriculum was from CLRS,[1] which presents proofs of correctness for many algorithms but doesn't explain how to develop such proofs. The curriculum for the last two weeks of the course, however, was a handout titled Transition Systems,[2] which I found to be an excellent introduction to the subject.

Since that time I've been interested in the idea of proving programs correct. On weekends I'm currently making my way through David Gries's The Science of Programming. Similar books include

- A Discipline of Programming by Dijkstra

- The Evolution of Programs by N. Dershowitz

[1] http://mitpress.mit.edu/algorithms/

[2] http://www.cs.au.dk/dADS1/daimi-fn64.pdf

In a similar vein is Elements of Programming by Alexander Stepanov (designer of the C++ STL) and Paul McJones: http://www.elementsofprogramming.com/book.html

@jhck, drothlis: Thank you very much to both of you, those suggestions are exactly what was asked for. I'd upvote you more if I could. :)

Both the Gries book and Stepanov's book have really impressive reviews on Amazon, am looking forward to diving into them.

http://www.amazon.com/Science-Programming-Monographs-Compute...

http://www.amazon.com/Elements-Programming-Alexander-Stepano...

I think category theory could be the maths for software engineers to the mechanical engineers calculus. Once you get past the arrows and weird Greek nomenclature you realize its just algebra. It seems a reasonable compromise to using formal logic whose cost is simply not worth it in most all cases. Still most presentations are very academic and neither presented in the way that a busy engineer can easily grasp and use. I've been trying to simultaneously learn and break it down to a much simpler core for my self that can be used without thinking - kind of like how engineers use physics - but still serve as a strong scaffolding of support when attacking a problem. Progress is tough though.

You might want to look at something like:

http://en.wikipedia.org/wiki/Formal_semantics_of_programming...

I seem to remember that Dijkstra was keen on identifying weakest preconditions of different statements that can be used to prove a program correct.

However, I warn you that if you try this you will soon find out what this kind of formal reasoning about programs never caught on that widely - at least for imperative programs.