Toward Zero-defect Programming
This book describes current methods for writing (nearly) bug-free programs. These methods are based on practices developed at IBM and elsewhere under the name Cleanroom Software Engineering. In a concise presentation, the author shows how to apply these methods in three key areas of software development: specification, verification, and testing. Requiring formal specifications forces students to program more simply and more clearly, eliminating many defects as a consequence. Performing semiformal verification as part of a team process uncovers additional defects. Testing the program, to compensate for human fallibility in the preceding steps, catches (nearly) all remaining bugs. The author departs somewhat from IBM Cleanroom methods to simplify the formalism that students must learn, and to make specification and verification readily accessible to anyone who can write well-structured programs. Although the book's examples are written in several programming languages, the largest number is in C.
What people are saying - Write a review
The Functions Computed by Programs
9 other sections not shown
abstract algorithm Alice allocated-length Bigstring blanks bugs Chapter char character of input Chris Cleanroom methods conditional concurrent assignment conflicting record conflicting-record conflicts with whenl contains control constructs correct with respect correctness questions data structure defects defined definite iteration elements empty example executed expression formal methods function computed functional languages getchar Harlan Mills Icon identity function if-statement implementation increment initialization integer intended function intended value invariant line in input linelength loop body mathematical names in list nonempty notation NULL number of letters object-oriented programming operation output precondition probably procedure produce programming language projects Python language recursive result return some conflicting routine schedule of whol sequence of statements sequence of values specification and verification specify and verify stdin string sum/n syntax temp terminal symbols termination trace table unit testing users variable verification conditions verification reviews while-loop who2 whol conflicts