Software Verification and Analysis (eBook)

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