The Calculus of Computation (eBook)

Preface 6
Contents 10
Part I Foundations 15
1 Propositional Logic 16
1.1 Syn tax 17
1.2 Seman tics 19
1.3 Satisfiabilit y and V alidit y 21
1.4 Equiv alence and Implication 27
1.5 Substitution 29
1.6 Normal F orms 31
1.7 Decision Pro cedures for Satisfiabilit y 34
1.8 Summary 44
Bibliographic Remarks 45
Exercises 45
2 First-Order Logic 48
2.1 Syn tax 48
2.2 Seman tics 52
2.3 Satisfiabilit y and V alidit y 55
2.4 Substitution 58
2.5 Normal F orms 64
2.6 Decidabilit y and Complexit y 66
2.7 69
Meta-Theorems of First-Order Logic 69
2.8 Summary 79
Bibliographic Remarks 80
Exercises 80
3 First-Order Theories 82
3.1 First-Order Theories 82
3.2 Equalit y 84
3.3 Natural Num b ers and In tegers 86
3.4 Rationals and Reals 92
3.5 Recursiv e Data Structures 97
3.6 Arra ys 100
3.7 103
Surv ey of Decidabilit y and Complexit y 103
3.8 Com bination Theories 104
3.9 Summary 105
Bibliographic Remarks 106
Exercises 106
4 Induction 108
4.1 Step wise Induction 108
4.2 Complete Induction 112
4.3 W ell-F ounded Induction 115
4.4 Structural Induction 121
4.5 Summary 123
Bibliographic Remarks 124
Exercises 124
5 Program Correctness: Mechanics 126
5.1 pi: A Simple Imp erativ e Language 127
5.2 P artial Correctness 136
5.3 T otal Correctness 156
5.4 Summary 162
Bibliographic Remarks 163
Exercises 164
6 Program Correctness: Strategies 166
6.1 Dev eloping Inductiv e Annotations 166
6.2 Extended Example: QuickSort 177
6.3 Summary 185
Bibliographic Remarks 186
Exercises 186
Part I Algorithmic Reasoning 193
7 Quantified Linear Arithmetic 194
7.1 Quan tifier Elimination 195
7.2 Quan tifier Elimination o v er In tegers 196
• • • • • . . . . 201
• . • • • . . . . | 201
• . . . . . . . . | 201
7.3 Quan tifier Elimination o v er Rationals 211
. • 213
. 213
. 213
. . 213
7.4 215
Complexit y 215
7.5 Summary 215
Bibliographic Remarks 216
Exercises 216
8 Quantifier-Free Linear Arithmetic 218
8.1 Decision Pro cedures for Quan tifier-F ree F ragmen ts 218
8.2 Preliminary Concepts and Notation 220
8.3 Linear Programs 224
8.4 The Simplex Metho d 229
8.5 Summary 248
Bibliographic Remarks 249
Exercises 249
9 Quantifier-Free Equality and Data Structures 252
9.1 Theory of Equalit y 253
9.2 Congruence Closure Algorithm 255
9.3 Congruence Closure with D A Gs 262
9.4 Recursiv e Data Structures 270
9.5 Arra ys 274
9.6 Summary 276
Bibliographic Remarks 277
Exercises 278
10 Combining Decision Procedures 280
10.1 Com bining Decision Pro cedures 280
10.2 Nelson-Opp en Metho d: Nondeterministic V ersion 282
10.3 Nelson-Opp en Metho d: Deterministic V ersion 287
10.4 294
Correctness of the Nelson-Opp en Metho d 294
10.5 298
Complexit y 298
10.6 Summary 299
Bibliographic Remarks 299
Exercises 299
11 Arrays 301
11.1 Arrays with Unin terpreted Indices 302
11.2 In teger-Indexed Arra ys 309
11.3 Hash tables 314
11.4 Larger F ragmen ts 318
11.5 Summary 319
Bibliographic Remarks 320
Exercises 320
12 Invariant Generation 321
12.1 In v arian t Generation 321
12.2 In terv al Analysis 335
12.3 Karr’s Analysis 343
12.4 351
Standard Notation and Concepts 351
12.5 Summary 354
Bibliographic Remarks 355
Exercises 355
13 Further Reading 357
References 361
Index 366