| Preface | 6 |
|---|
| Structure of the Text | 7 |
| Software Tools | 9 |
| The Accompanying Web Site | 9 |
| The Audience of the Book | 10 |
| Acknowledgments | 11 |
|---|
| Contents | 12 |
|---|
| Introduction: What Do We Want To Know About the Program? | 16 |
|---|
| 1 What is the Program Doing: Specification | 16 |
| 2 How to Make Sure That the Program is Doing it Right: Verification | 20 |
| 3 Trying to Show That the Program is Incorrect: Testing | 23 |
| 4 Trying to Locate the Cause of Incorrectness: Debugging | 26 |
| 5 What One Can Tell About The Program Without Executing It: Static Analysis | 30 |
| 6 The Scope of the SAT Methods | 32 |
| 7 Conclusions | 35 |
| Exercises | 36 |
| References | 36 |
| The Semantic Analysis | 37 |
|---|
| Why Not Write Correct Software the First Time? | 38 |
| 1.1 Express Yourself Precisely: The Precondition | 38 |
| 1.2 The Postcondition | 41 |
| 1.3 The Principles of Top-Down Refinement | 45 |
| 1.4 The Example Continued | 46 |
| 1.5 Conclusions | 49 |
| References | 50 |
| How to Prove a Program Correct: Programs Without Loops | 52 |
| 2.1 Program Correctness | 52 |
| 2.2 The Weakest Precondition wp( S , Q) | 55 |
| 2.3 Finding the wp( S , Q ) | 56 |
| 2.4 SPARK Experiments | 58 |
| 2.5 Programs With Many Paths | 62 |
| 2.6 The Derivation of Partial Weakest Precondition (pwp) and Path Traversal ( tr) | 65 |
| 2.7 The Assertion Method | 69 |
| 2.8 Conclusions | 73 |
| References | 74 |
| How to Prove a Program Correct: Iterative Programs | 75 |
| 3.1 When You Cannot Verify All Paths: Programs with Loops | 75 |
| 3.2 From the Particular to the General: Mathematical Induction | 77 |
| 3.3 Loop Invariants | 78 |
| 3.4 Where Do Invariants Come From: Goal Invariant | 82 |
| 3.5 Supporting the Proof: Using the Proof Checker | 84 |
| 3.6 Does the Loop Terminate? Variants | 88 |
| 3.7 Conclusions | 89 |
| References | 91 |
| Prepare Test for Any Implementation: Black- Box Testing | 92 |
| 4.1 Testing Principles | 92 |
| 4.2 Functionality Testing | 96 |
| 4.3 Partition Testing | 99 |
| 4.4 An Example | 100 |
| 4.5 Random Testing | 106 |
| 4.6 Conclusions | 108 |
| References | 110 |
| Static Analysis | 111 |
|---|
| Intermediate Program Representation | 112 |
| 5.1 Introduction | 112 |
| 5.2 Program Parse and Syntax Trees | 113 |
| 5.3 Program Control Flowgraph | 113 |
| 5.4 Labeled Flowgraphs | 118 |
| 5.5 Deriving the Flowgraph | 121 |
| 5.6 Paths in Flowgraphs | 125 |
| 5.7 Conclusions | 132 |
| References | 132 |
| Program Dependencies | 133 |
| 6.1 Motivations | 133 |
| 6.2 Dominators and Attractors | 136 |
| 6.3 Control Dependency: Structured Control | 139 |
| 6.4 Control Dependency: Arbitrary Control | 143 |
| 6.5 Computing Control Dependency | 145 |
| 6.6 Data and General Dependency | 147 |
| 6.7 Conclusions | 149 |
| References | 150 |
| What Can One Tell About a Program Without Its Execution: Static Analysis | 151 |
| 7.1 Motivations | 151 |
| 7.2 Control Flow Anomalies | 153 |
| 7.3 Data Flow Anomalies | 155 |
| 7.4 Modeling Procedure Calls | 160 |
| 7.5 Signature Anomalies | 166 |
| 7.6 Descriptive Static Analysis | 171 |
| 7.7 Events on Program Paths | 173 |
| 7.8 Conclusions | 176 |
| References | 177 |
| Dynamic Analysis | 178 |
|---|
| Is There a Bug in the Program? Structural Program Testing | 179 |
| 8.1 Introduction | 179 |
| 8.2 Code Coverage Criteria | 180 |
| 8.3 Testing Scenario | 185 |
| 8.4 Faults and Errors | 191 |
| 8.5 Fault Detection Power of Code Coverage Testing | 197 |
| 8.6 Program Dependencies in Software Testing | 199 |
| 8.7 Conclusions | 204 |
| References | 207 |
| Dynamic Program Analysis | 209 |
| 9.1 Introduction | 209 |
| 9.2 Operational Semantics: States and Computations | 210 |
| 9.3 Dynamic Analysis Concepts | 214 |
| 9.4 An Application: Dynamic Program Slicing | 217 |
| 9.5 An Application: Handling Dynamic Data Structures | 220 |
| 9.6 Conclusions | 223 |
| References | 225 |
| Index | 226 |
|---|
