Toward Zero-Defect Programming

Allan M. Stavely

  • 出版商: Addison Wesley
  • 出版日期: 1998-09-24
  • 售價: $995
  • 貴賓價: 9.5$945
  • 語言: 英文
  • 頁數: 256
  • 裝訂: Paperback
  • ISBN: 0201385953
  • ISBN-13: 9780201385953






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.

Back to Top

Table Of Contents

(Chapters 2 - 11 contain Exercises and all chapters conclude with Notes.)
1. Introduction.

The Problem: Bugs.
The Cleanroom Method.
About This Book.

2. The Functions Computed by Programs.
Computations: States and Functions.
Representation of Functions: Concurrent Assignments.
Conditional Concurrent Assignments.
Local Variables.
Specification Using Intended Functions.
Other Notation Conventions.
Writing Intended Functions.

3. Verification.
The Structured Control Constructs.
Placement of Intended Functions.
The Substitution Principle.
Sequences of Statements.
Trace Tables.
Conditional Trace Tables.

4. Verification of Iterations.
Proving Termination.
Initialized Loops.
Writing Intended Functions for Loops in Isolation.
Other Forms of Indefinite Iteration.

5. Programming with Intended Functions.
A Pascal Program: Length of the Longest Line.
A C Program: Counting Letters and Digits.
An Icon Routine: Uncompressing a String.
A Study in Abstraction: The Registrar's Program.
Keeping Things Simple.

6. Verification Reviews.
Why Verification Reviews Are Necessary.
Verification Reviews in the Cleanroom Process.
How Verification Reviews Are Done.
Example: Another Routine from the Registrar's Programs.
Example: A Routine from a Test-data Generator.
Discussion of the Examples.

7. Definite Iteration.
Definite Iteration Over Sequences.
Sequence Variables.
Other Sequence Expressions.
Ranges of Integers.
Other Data Structures.
The Iteration Mechanisms.
Sets and Sequences in Program Design.

8. Data Abstraction and Object-oriented Programs.
Data Abstraction and Encapsulation.
The Abstraction Function.
Data Invariants.
Object-oriented Programs.

9. Recursion and Functional Languages.
Recursive Routines.
Mutual Recursion.
Functional Languages.

10. Testing.
The Role of Testing.
Usage-based Testing.
Test-data Generators.
Other Forms of Testing.

11. Incremental Development.
Developing a Program in Increments.
Example: Rehearsal Scheduling.

12. Where Do We Go From Here?
Other Parts of the Cleanroom Process.
Other Formal Methods.
What Have We Accomplished?
Prospects for the Future.

Hints for Selected Exercises.
Index. 0201385953T04062001

Back to Top