Bradley / Manna The Calculus of Computation

Decision Procedures with Applications to Verification
1. Auflage 2007
ISBN: 978-3-540-74113-8
Verlag: Springer Berlin Heidelberg
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 366 Seiten

Written with graduate and advanced undergraduate students in mind, this textbook introduces computational logic from the foundations of first-order logic to state-of-the-art decision procedures for arithmetic, data structures, and combination theories. The textbook also presents a logical approach to engineering correct software. Verification exercises are given to develop the reader's facility in specifying and verifying software using logic. The treatment of verification concludes with an introduction to the static analysis of software, an important component of modern verification systems. The final chapter outlines courses of further study.

Autoren/Hrsg.

Bradley, Aaron R.

Manna, Zohar

Inhaltsverzeichnis

1;Preface;6
2;Contents;10
3;Part I Foundations;15
3.1;1 Propositional Logic;16
3.1.1;1.1 Syn tax;17
3.1.2;1.2 Seman tics;19
3.1.3;1.3 Satisfiabilit y and V alidit y;21
3.1.4;1.4 Equiv alence and Implication;27
3.1.5;1.5 Substitution;29
3.1.6;1.6 Normal F orms;31
3.1.7;1.7 Decision Pro cedures for Satisfiabilit y;34
3.1.8;1.8 Summary;44
3.1.9;Bibliographic Remarks;45
3.1.10;Exercises;45
3.2;2 First-Order Logic;48
3.2.1;2.1 Syn tax;48
3.2.2;2.2 Seman tics;52
3.2.3;2.3 Satisfiabilit y and V alidit y;55
3.2.4;2.4 Substitution;58
3.2.5;2.5 Normal F orms;64
3.2.6;2.6 Decidabilit y and Complexit y;66
3.2.7;2.7;69
3.2.8;Meta-Theorems of First-Order Logic;69
3.2.9;2.8 Summary;79
3.2.10;Bibliographic Remarks;80
3.2.11;Exercises;80
3.3;3 First-Order Theories;82
3.3.1;3.1 First-Order Theories;82
3.3.2;3.2 Equalit y;84
3.3.3;3.3 Natural Num b ers and In tegers;86
3.3.4;3.4 Rationals and Reals;92
3.3.5;3.5 Recursiv e Data Structures;97
3.3.6;3.6 Arra ys;100
3.3.7;3.7;103
3.3.8;Surv ey of Decidabilit y and Complexit y;103
3.3.9;3.8 Com bination Theories;104
3.3.10;3.9 Summary;105
3.3.11;Bibliographic Remarks;106
3.3.12;Exercises;106
3.4;4 Induction;108
3.4.1;4.1 Step wise Induction;108
3.4.2;4.2 Complete Induction;112
3.4.3;4.3 W ell-F ounded Induction;115
3.4.4;4.4 Structural Induction;121
3.4.5;4.5 Summary;123
3.4.6;Bibliographic Remarks;124
3.4.7;Exercises;124
3.5;5 Program Correctness: Mechanics;126
3.5.1;5.1 pi: A Simple Imp erativ e Language;127
3.5.2;5.2 P artial Correctness;136
3.5.3;5.3 T otal Correctness;156
3.5.4;5.4 Summary;162
3.5.5;Bibliographic Remarks;163
3.5.6;Exercises;164
3.6;6 Program Correctness: Strategies;166
3.6.1;6.1 Dev eloping Inductiv e Annotations;166
3.6.2;6.2 Extended Example: QuickSort;177
3.6.3;6.3 Summary;185
3.6.4;Bibliographic Remarks;186
3.6.5;Exercises;186
4;Part I Algorithmic Reasoning;193
4.1;7 Quantified Linear Arithmetic;194
4.1.1;7.1 Quan tifier Elimination;195
4.1.2;7.2 Quan tifier Elimination o v er In tegers;196
4.1.3;• • • • • . . . . ;201
4.1.4;• . • • • . . . . |;201
4.1.5;• . . . . . . . . | ;201
4.1.6;7.3 Quan tifier Elimination o v er Rationals;211
4.1.7;. •;213
4.1.8;.;213
4.1.9;. ;213
4.1.10;. .;213
4.1.11;7.4;215
4.1.12;Complexit y;215
4.1.13;7.5 Summary;215
4.1.14;Bibliographic Remarks;216
4.1.15;Exercises;216
4.2;8 Quantifier-Free Linear Arithmetic;218
4.2.1;8.1 Decision Pro cedures for Quan tifier-F ree F ragmen ts;218
4.2.2;8.2 Preliminary Concepts and Notation;220
4.2.3;8.3 Linear Programs;224
4.2.4;8.4 The Simplex Metho d;229
4.2.5;8.5 Summary;248
4.2.6;Bibliographic Remarks;249
4.2.7;Exercises;249
4.3;9 Quantifier-Free Equality and Data Structures;252
4.3.1;9.1 Theory of Equalit y;253
4.3.2;9.2 Congruence Closure Algorithm;255
4.3.3;9.3 Congruence Closure with D A Gs;262
4.3.4;9.4 Recursiv e Data Structures;270
4.3.5;9.5 Arra ys;274
4.3.6;9.6 Summary;276
4.3.7;Bibliographic Remarks;277
4.3.8;Exercises;278
4.4;10 Combining Decision Procedures;280
4.4.1;10.1 Com bining Decision Pro cedures;280
4.4.2;10.2 Nelson-Opp en Metho d: Nondeterministic V ersion;282
4.4.3;10.3 Nelson-Opp en Metho d: Deterministic V ersion;287
4.4.4;10.4;294
4.4.5;Correctness of the Nelson-Opp en Metho d;294
4.4.6;10.5;298
4.4.7;Complexit y;298
4.4.8;10.6 Summary;299
4.4.9;Bibliographic Remarks;299
4.4.10;Exercises;299
4.5;11 Arrays;301
4.5.1;11.1 Arrays with Unin terpreted Indices;302
4.5.2;11.2 In teger-Indexed Arra ys;309
4.5.3;11.3 Hash tables;314
4.5.4;11.4 Larger F ragmen ts;318
4.5.5;11.5 Summary;319
4.5.6;Bibliographic Remarks;320
4.5.7;Exercises;320
4.6;12 Invariant Generation;321
4.6.1;12.1 In v arian t Generation;321
4.6.2;12.2 In terv al Analysis;335
4.6.3;12.3 Karr’s Analysis;343
4.6.4;12.4;351
4.6.5;Standard Notation and Concepts;351
4.6.6;12.5 Summary;354
4.6.7;Bibliographic Remarks;355
4.6.8;Exercises;355
4.7;13 Further Reading;357
5;References;361
6;Index;366