Fog Creek Software
Discussion Board

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.

Thanks for any knowledgeable help.

Tayssir J.
Wednesday, July 3, 2002

"Agile Software Development" by Cockburn.

Nat Ersoz
Wednesday, July 3, 2002

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!

Tayssir J.
Wednesday, July 3, 2002

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 for a bibliography (esp. #8).

Andrzej Kocon
Thursday, July 4, 2002

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.

Of course, maybe that's bassackward.  I'm a formal methods newbie. ;)

Thanks for the tips, by the way.  I'll order the Dijkstra book, but too bad Colburn's Program Verification book is $350 at Amazon.

Tayssir J.
Thursday, July 4, 2002

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.

K. Åkesson
Thursday, July 4, 2002

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:

If you're interested in concurrency, check out "Communicating Sequential Processes" by CAR Hoare, and have a look at:

Andrew Simmons
Thursday, July 4, 2002

Formal correctness proofs are interesting stuff, Richard Bornat (an old lecturer of mine) is heavily into this stuff see (several other members of the dept. such as Peter Landin were involved in the early days) has a better page for this stuff.

It's worth pointing out that our primary first year computing course consisted of proving programs written in ML (IIRC it wasn't exactly ML but some bastardisation of it)

Peter Ibbotson
Friday, July 5, 2002

To the original poster,

Take a look at Persuasive Programming by Mead & Shende.

As hinted at by the title it describes a method for proving program correctness. It is unusual in that it assumes no background math knowledge from the reader.

Since you mentioned category theory, try googling for category theory computer scientist.

As you dig into it, you will find that there is no unified topic of "formal methods." It is more of a philosophy that shows up in many areas of computer science. Different topics require different techniques. But you will see the same techniques show up in widely separated areas.

Monday, July 8, 2002

*  Recent Topics

*  Fog Creek Home