Deductive verification of object-oriented software : dynamic frames, dynamic logic and predicate abstraction

Software Verification......Page 25
KeY......Page 27
Problems and Contributions......Page 30
Outline......Page 33
Specification......Page 35
Background on JML......Page 37
Expressions......Page 38
Pre- and Postconditions......Page 40
Modifies Clauses......Page 43
Object Invariants......Page 45
Subtyping and Inheritance......Page 47
Data Abstraction......Page 48
Ghost Fields......Page 49
Model Fields and Data Groups......Page 52
Pure Methods and Depends Clauses......Page 56
Conclusion......Page 59
Issues with Object Invariants......Page 61
Issues with Data Groups......Page 63
Dynamic Frames......Page 64
JML*......Page 66
Example......Page 69
Discussion......Page 76
Related Work......Page 78
Conclusion......Page 85
Verification......Page 87
The Java Heap......Page 89
Logical Models of the Heap......Page 90
Fields as Non-Rigid Functions......Page 91
The Heap as a Binary Non-Rigid Function......Page 93
The Heap as a Program Variable......Page 94
Conclusion......Page 95
Java Dynamic Logic with an Explicit Heap......Page 97
Dynamic Logic with Updates......Page 98
Syntax......Page 101
Semantics......Page 106
Calculus......Page 113
Rules for Types......Page 115
Rules for Unique Function Symbols......Page 117
Rules for Well-formedness of Heap Arrays......Page 118
Rules for Updates......Page 122
Rules for Symbolic Execution of Java Programs......Page 125
Loop Invariant Rule......Page 130
Example Proofs......Page 136
Reading and Writing the Heap......Page 137
Aliasing......Page 139
Object Creation......Page 141
Loops......Page 142
Conclusion......Page 146
Expressions......Page 149
Createdness of Observed Objects......Page 155
Pure Methods......Page 156
Represents Clauses......Page 157
Object Invariants......Page 160
Method Contracts......Page 161
Dependency Contracts......Page 164
Proof Obligations......Page 165
Proof Obligations for Method Contracts......Page 166
Proof Obligations for Dependency Contracts......Page 168
Contract Rules......Page 170
Rule for Method Contracts......Page 171
Rule for Dependency Contracts......Page 173
Example......Page 176
Related Work......Page 183
Conclusion......Page 185
Loop Invariant Generation......Page 187
Background on Abstract Interpretation......Page 189
Control Flow Graphs......Page 190
Abstract Domains......Page 191
Consistency of Abstract Domains......Page 198
Widening......Page 199
Iteration Strategies......Page 203
Example Abstract Domains......Page 204
Pointer Structure Domains......Page 205
Tools......Page 206
Conclusion......Page 207
Predicate Abstraction in Java Dynamic Logic......Page 209
Approach......Page 210
Converting Updates into Formulas......Page 212
Merging Proof Branches......Page 214
Setting Back Proof Branches......Page 215
Predicate Abstraction......Page 216
Proof Search Strategy......Page 218
Predicate Abstraction Algorithm......Page 223
Generating Loop Predicates......Page 224
Example......Page 225
Experiments......Page 229
Dependency Proofs......Page 230
Related Work......Page 235
Conclusion......Page 237
Summary......Page 239
Future Work......Page 240
Preparatory Observations......Page 243
Proof of Lemma 5.1: A Consequence of Well-formedness......Page 245
Proof of Lemma 5.2: Well-formedness after Storing an Object......Page 246
Proof of Lemma 5.3: Well-formedness after Anonymisation......Page 247
Proof of Lemma 5.4: Connection between frame and anon......Page 249
Proof of Theorem 5.5: Soundness of loopInvariant......Page 251
Proof of Theorem 6.1: Soundness of useMethodContract......Page 256
Proof of Lemma 6.2: No Deallocations......Page 261
Proof of Theorem 6.3: Soundness of useDependencyContract......Page 262
Proof of Theorem 8.1: Soundness of shiftUpdate......Page 265
Proof of Theorem 8.4: Soundness of predicateAbstraction......Page 267
Bibliography......Page 269
Index......Page 289