[bmer]

Backhouse's more playful book, focuses primarily on teaching one how to write and use proofs in the "calculational style" of Dijkstra/Hoare/Lamport/others.

Backhouse's less playful book covers the same topic, but has some more programming examples:

* cyclic code error correction * simple sorting algorithms * real number to integer conversion is used to introduce Galois connections

Again, this isn't a lot in terms of "practical examples". No production level software is built here. If you're looking for that sort of stuff, maybe you want to try out L. Lamport's book: http://www.amazon.com/Specifying-Systems-Language-Hardware-E...

I haven't read that book though.

[nickpsecurity]

Anyone that knows about all these resources should really scour them to put together a list of their application to real-world problems. Any researchers that like the stuff should apply them to real-world problems. The reason is that we don't know if such methods are a waste of time or useful until that happens. So, I'm interested in anything you have on that.

EDIT: Your recommendation was good as it clearly has practical advice. I can tell just looking at table of contents. And, as a gift, I found the whole book for free plus other things in link below. :)

http://research.microsoft.com/en-us/um/people/lamport/tla/bo...