| Introduction: What Do We Want To Know About the Program? | |
| What is the Program Doing: Specification | p. 1 |
| How to Make Sure That the Program is Doing it Right: Verification | p. 5 |
| Trying to Show That the Program is Incorrect: Testing | p. 8 |
| Trying to Locate the Cause of Incorrectness: Debugging | p. 11 |
| What One Can Tell About The Program Without Executing It: Static Analysis | p. 15 |
| The Scope of the SAT Methods | p. 17 |
| Conclusions | p. 20 |
| Exercises | p. 21 |
| References | p. 21 |
| The Semantic Analysis | |
| Why Not Write Correct Software the First Time? | p. 25 |
| Express Yourself Precisely: The Precondition | p. 25 |
| The Postcondition | p. 28 |
| The Principles of Top-Down Refinement | p. 32 |
| The Example Continued | p. 33 |
| Conclusions | p. 36 |
| References | p. 37 |
| How to Prove a Program Correct: Programs Without Loops | p. 39 |
| Program Correctness | p. 39 |
| The Weakest Precondition wp(S, Q) | p. 42 |
| Finding the wp(S, Q) | p. 43 |
| The Assignment Axiom | p. 43 |
| A Sequence of Assignments: The Composition Rule | p. 44 |
| SPARK Experiments | p. 45 |
| Programs With Many Paths | p. 49 |
| The Derivation of Partial Weakest Precondition (pwp) and Path Traversal (tr) | p. 52 |
| The Assertion Method | p. 56 |
| Conclusions | p. 60 |
| Exercises | p. 60 |
| References | p. 61 |
| How to Prove a Program Correct: Iterative Programs | p. 63 |
| When You Cannot Verify All Paths: Programs with Loops | p. 63 |
| From the Particular to the General: Mathematical Induction | p. 65 |
| Loop Invariants | p. 66 |
| Where Do Invariants Come From: Goal Invariant | p. 70 |
| Supporting the Proof: Using the Proof Checker | p. 72 |
| Does the Loop Terminate? Variants | p. 76 |
| Conclusions | p. 77 |
| Exercises | p. 78 |
| References | p. 79 |
| Prepare Test for Any Implementation: Black-Box Testing | p. 81 |
| Testing Principles | p. 81 |
| Functionality Testing | p. 85 |
| Special Values | p. 86 |
| Fixed Points | p. 86 |
| Special Classes | p. 87 |
| Boundary Analysis | p. 87 |
| Partition Testing | p. 88 |
| An Example | p. 89 |
| Random Testing | p. 95 |
| Conclusions | p. 97 |
| Exercises | p. 98 |
| References | p. 99 |
| Static Analysis | |
| Intermediate Program Representation | p. 103 |
| Introduction | p. 103 |
| Program Parse and Syntax Trees | p. 104 |
| Program Control Flowgraph | p. 104 |
| Labeled Flowgraphs | p. 109 |
| Deriving the Flowgraph | p. 112 |
| Paths in Flowgraphs | p. 116 |
| Conclusions | p. 123 |
| Exercises | p. 123 |
| References | p. 123 |
| Program Dependencies | p. 125 |
| Motivations | p. 125 |
| Dominators and Attractors | p. 128 |
| Control Dependency: Structured Control | p. 131 |
| Control Dependency: Arbitrary Control | p. 135 |
| Computing Control Dependency | p. 137 |
| Data and General Dependency | p. 139 |
| Conclusions | p. 141 |
| Exercises | p. 142 |
| References | p. 142 |
| What Can One Tell About a Program Without Its Execution: Static Analysis | p. 143 |
| Motivations | p. 143 |
| Control Flow Anomalies | p. 145 |
| Data Flow Anomalies | p. 147 |
| Undefined-Referenced (UR) Anomaly: The Use of Uninitialized Variables | p. 149 |
| Double Definition (DD) Anomaly | p. 151 |
| Redundant Statement (RS) Anomaly | p. 151 |
| Loop Analysis | p. 151 |
| Modeling Procedure Calls | p. 152 |
| Signature Anomalies | p. 158 |
| Descriptive Static Analysis | p. 163 |
| Control Flow Queries | p. 164 |
| Data flow and Dependency Queries | p. 164 |
| Structural Testing Queries | p. 165 |
| System (Program) and Visibility Queries | p. 165 |
| Events on Program Paths | p. 165 |
| Conclusions | p. 168 |
| Exercises | p. 169 |
| References | p. 169 |
| Dynamic Analysis | |
| Is There a Bug in the Program? Structural Program Testing | p. 173 |
| Introduction | p. 173 |
| Code Coverage Criteria | p. 174 |
| Testing Scenario | p. 179 |
| Faults and Errors | p. 185 |
| Fault Detection Power of Code Coverage Testing | p. 191 |
| Program Dependencies in Software Testing | p. 193 |
| Conclusions | p. 198 |
| Exercises | p. 201 |
| References | p. 201 |
| Dynamic Program Analysis | p. 203 |
| Introduction | p. 203 |
| Operational Semantics: States and Computations | p. 204 |
| Dynamic Analysis Concepts | p. 208 |
| An Application: Dynamic Program Slicing | p. 211 |
| An Application: Handling Dynamic Data Structures | p. 214 |
| Conclusions | p. 217 |
| Exercises | p. 218 |
| References | p. 219 |
| Index | p. 221 |
| Table of Contents provided by Ingram. All Rights Reserved. |
