[jhck]

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

[drothlis]

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

[limist]

@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...