Stavely, Allan M. Toward zero-defect programming. Addison-Wesley, September 1998, ISBN 0201385953.
Disclaimer: The author is a close friend and colleague of mine.
I have been making my living by programming since 1966, and it is has always been my central professional interest. I've also resisted most of the fads and trends in the industry---structured programming and objects, for example. But from time to time I've reluctantly admitted that some new techniques have real merit.
After my career passed the 25-year mark, I didn't really expect any dramatic changes in the way I work. But the ideas of Cleanroom Software Development, pioneered by Harlan Mills at IBM, have had a profound positive impact on my work, possibly the most important new technique I've ever learned.
I now wonder how any of my code survived real users before. I hated to admit it (and I think most coders do) but there had always been icky spots in the design where I didn't really have total confidence that it would always work.
Now, though, I actually expect my programs to work in pretty much all cases. This is a novel and rather exhilarating feeling.
One summer a few years back, the National Science Foundation funded the author's trip to IBM to learn Cleanroom. Shortly afterwards, he taught the method as a regular Computer Science course here at New Mexico Tech, and I took the class.
At that time there really weren't any publications that taught the whole method. Some sources discussed intended functions and decomposition but there weren't any good sources for the verification phase, which is a critical part of the method. This book now satisfies the need for a single source describing the whole method. The material is tempered by the author's experience in teaching several repetitions of the course.
The method is not difficult to learn. It does not require much math, although familiarity with algebraic proofs is helpful for understanding why it works. I'm even starting to believe that it can do a lot for you even if you don't go through the peer verification step, although of course that step is really necessary for the highest quality levels.
Moreover, the method is neutral with regard to specific languages and other aspects of methodology. It works with languages like Python that don't have compile-time type checking, as well as the more traditional languages. It works with object-oriented code as well as more traditional straight procedural code.
Cleanroom is no substitute for experience or familiarity with the basic tools of our craft---algorithms, data structures, languages and operating systems. It works better with those who have programming talent and experience.
One of its strongest assets is that it militates against needless complexity and klugey techniques. I work a lot with students, and some of them are infatuated with complexity and cutting-edge techniques for their own sake---as was I at that age. Cleanroom has a merciless way of exposing the parts of a design that have not been thought through completely, or don't have solid grounding in theory.
Best of all, Cleanroom is schedule- and budget-friendly. In my experience, it takes no longer to do things this way. All that changes is the proportions of the subtasks: much more time is spent on design, and much less time is needed for testing. When I finish coding a good-sized application, say around 10,000 lines of Python, it generally goes from first compilation to no known bugs in about a workday. Not a single program I've done in the Cleanroom style has turned out to be a source of pain and aggravation due to flakiness (unlike, alas, some of my earlier products)---they just work.
Neither the author nor I will claim that we can achieve zero defects. But we can come much closer than before. Another positive effect is that the bugs that remain are both easier to find and easier to fix. Subtle bugs have become quite rare in my work, and I hardly ever use a debugger.
In parting, here is an original aphorism I coined about the Cleanroom method and how it has changed my style:
Life is too short to write unverifiable code.