Formal software development book
Hi, does anyone with experience in formal software development know good books to read on the topic? I'm eyeing the Sannella & Tarlecki book, which seems to start from the basics, but it won't be out for at least another year.
"Agile Software Development" by Cockburn.
I just looked at the Agile Manifesto, and I'm more looking for "formal methods," like proving correctness. A fundamental book, that explains stuff like category theory Sorry if I wasn't clear!
A subtle point: are you interested in the so called "a posteriori verification" (i.e., "putting the cart before the horse"), or in any subject to make a degree with, or in the formal techniques of *deriving* correct programs? In the latter case, Dijkstra's "A discipline of programming", Englewood Cliffs, N.J.: Prentice-Hall 1976, is still a good start that illustrates the point. See also http://www.cs.buffalo.edu/~rapaport/451/progver.bib.pdf for a bibliography (esp. #8).
This isn't for a degree, but for my own development. Basically, I would like to know how to come up with a good notation for things, how to reason (with rigor) with it, and at some point I can translate it into whatever language I implement with.
If you are interested in formal issues of concurrency then I think that "Concurrency: State Models & Java Programs by Jeff Magee, Jeff Kramer" has a good balance between theory and practice.
I'd second the Dijkstra recommendation. I don't know if it's still in print, but there's an excellent and slightly gentler introduction to Dijkstra's ideas in "The Science of Programming" by David Gries. It's also worth looking at "Programming from Specifications" by Carroll Morgan, which is available on the Web at:
Formal correctness proofs are interesting stuff, Richard Bornat (an old lecturer of mine) is heavily into this stuff see http://www.dcs.qmul.ac.uk/~richard (several other members of the dept. such as Peter Landin were involved in the early days)
To the original poster,
Fog Creek Home