This is a book for programmers who want to write programs with no bugs, or at least with as few bugs as is humanly possible with current technology.
Programmers can do this by using a particular kind of specification and verification, which I will present in the book. By verification, I mean proving, mathematically, that a program agrees with its specification.
Don't panic. You will see that this does not require great mathematical sophistication, only knowledge of a few particular techniques and ways of doing things (and then, of course, practice). There is no rigorous mathematical formalism in this book. In fact, the specifications and proofs are usually only semiformal and are sometimes quite informal indeed.
Why verify programs? Because it is a very effective way of detecting bugs. We often find that, as we attempt to verify a program, that our efforts fail because the program is not, in fact, correct. When this happens, we have found a defect. Then, of course, we fix it.
This will be our fundamental assumption: The purpose of verification is to eliminate defects.
This is a very pragmatic view. Others may take the 'all-or-nothing' position that verification is a mathematical exercise that produces mathematically perfect objects and is worthless if it can't do that, but we won't say any such thing here. You won't see any claims in this book that verified programs cannot possibly contain any defects, do not need to be tested, and can be trusted unconditionally. On the contrary, we cannot always detect all defects in a program using verification: we are human, and we make mistakes. Thus, verified programs still need to be tested carefully, and I will present methods for doing this as well.
The methods presented in this book are based on a set of interrelated techniques developed at IBM in the late 1970s and early 1980s, under the name Cleanroom Software Engineering. IBM has used them on a number of substantial projects since then, with impressive success, and since the late 1980s their use has been spreading to other companies and organizations.
These methods work. Cleanroom methods can reduce the number of defects in software by an order of magnitude or more. The extra time spent in specifying and verifying is more than made up in reduced debugging and reworking time, so using these methods costs nothing extra in terms of effort or schedule time. And the methods scale up well to large systems. You don't need to take my word for it: the results have been reported in the open literature. You will see some of the data, with literature citations, in Chapter 1. And I, along with my colleagues and students, get similar results.
There is no magic here. Our methods require programmers to work carefully and systematically, to check their work, and above all to understand their programs very thoroughly. But these are things that they should be doing anyway, even if many donit. You can think of methods as merely tools that help programmers to do these things.
This book presents my adaptation of Cleanroom methods and should not be taken as an official statement of what Cleanroom Software Engineering is. I do not speak for the Cleanroom community, which in any case has dispersed and expanded far beyond the original group at IBM. In my presentation, I have chosen to emphasize the parts of the Cleanroom process that seem to me to be the most valuable (other Cleanroom practitioners may well disagree), and to deemphasize or omit others. I have also introduced a few new ideas of my own.
The book was written with classroom use in mind and is based on a course that I have been teaching since 1993. Besides presenting the fundamentals of specification, programming, verification, and testing in the Cleanroom style, I have included extra explanations, hints, and examples covering parts of the process that students seem to find difficult at first. Mine is a one-semester undergraduate course for computer science students, but a similar course could be taught at the graduate level. The book is also suitable for an intensive short course in an industrial or continuing-education setting.
Programming professionals will also find this book useful for self-study. You will see in Chapter 6, however, that the recommended way to do the verification is in small groups, in review meetings, rather than on your own. Thus, if you intend to study this book outside a course, you will get the best results if you can work with at least two or three other people who already know these methods or who would like to study them with you.
As a minimum, the reader should be familiar with the basics of algorithms and data structures, as taught in the usual first course in the subject, and with the rudiments of discrete mathematics (sets, relations, functions, and so on). The reader should also, of course, have enough experience in programming and debugging to appreciate how valuable zero-defect programming would be if we could do it!
I also assume the ability to read and understand the structure, at least in general terms, of programs written in languages in the Algol family (including Pascal, C, Modula, Icon, and so on). In Section 9.4 I also use the functional languages Scheme and ML, but that section can be omitted by readers who have no familiarity at all with functional languages. Similarly, in Section 8.4 I use the object-oriented features of C++ and Python languages in my examples, but that section can be skipped by readers who have no familiarity at all with object-oriented programming or languages.
The methods of this book can be applied to programs in a wide variety of languages. To demonstrate this, extended examples of programs, parts of programs, and program development will be presented using the following languages: C, C++, Icon, ML, Pascal, Python, and Scheme. Particular features of these languages are explained where they are used, so a detailed knowledge of all these languages is not required. However, more of the examples are written in C than in the other languages, so familiarity with C would be helpful.
In many places in the text, short fragments of programming-language code are used to illustrate the ideas being presented. Most of these fragments are written in a generic, 'ordinary' procedural programming language: except for trivial details such as where the semicolons are, the language of each fragment might be Pascal, or Modula, or Turning, or Icon, or Ada, or any of a dozen others. The syntax may vary, but the meaning should always be apparent. When an example is meant to be in a particular programming language, I will say so.
Literature citations and comments on related work appear in the Notes sections at the end of each chapter.
My most important source does not appear in those citations. I received my first training in Cleanroom methods at a one-week intensive workshop at the Rochester (New York) Institute of Technology in the summer of 1992. The workshop was sponsored by the (U.S.) National Science Foundation. It was a condensed version of IBM's in-house training course and was conducted by Philip Hausler, Mark Pleszkoch, and Steve Rosen, of the IBM Cleanroom Software Technology Center. I am most grateful to them and to IBM, NSF, and RIT for making the workshop possible. Although I do not cite this workshop in the Notes in specific chapters of the book, the workshop was a primary source for much of the material, particularly the material of Chapters 2 through 6 and Chapters 10 and 11.
I am also most grateful to friends and colleagues who have made valuable contributions to this book through consultation, suggestions, and corrections: Michael Deck, John Duncan, Doug Dunston, Suzanne Flandreau, Alex Kent, Ray Piworunas, Steve Powell, John Shipman (for help on more occasions than I can count), and Laurie Williams; also to Peter Gordon at Addison Wesley Longman, for support and suggestions; and to all of the students in my classes over the past five years, for helping me to debug my presentation of this material. Many thanks to all of you.
Cleanroom methods are the best that I have found for producing high-quality software, and experience has shown that they can take us a long way toward the goal of zero defects. I am confident that they will continue to be developed and refined and reasonably sure that different but even better methods will eventually be developed. Meanwhile, Cleanroom methods have proven their worth and are ready for practical use today, and I hope that the presentation in this book of my version of them will help to promote their use.
In any case, we can begin by changing our attitude toward bugs: they are not inevitable, and they are not acceptable. Zero defects is the goal that we should strive for. We will not always be able to achieve it, but we should try.
A. M. S.
Socorro, New Mexico
0201385953P05082001 
