Recent years have seen the development of powerful tools for verifying hardware and software systems, as companies worldwide realise the need for improved means of validating their products. There is increasing demand for training in basic methods in formal reasoning so that students can gain proficiency in logic-based verification methods. The second edition of this successful textbook addresses both those requirements, by continuing to provide a clear introduction to formal reasoning which is both relevant to the needs of modern computer science and rigorous enough for practical application. Improvements to the first edition have been made throughout, with extra and expanded sections on SAT solvers, existential/universal second-order logic, micro-models, programming by contract and total correctness. The coverage of model-checking has been substantially updated. Further exercises have been added. Internet support for the book includes worked solutions for all exercises for teachers, and model solutions to some exercises for students.
Author(s): Michael Huth, Mark Ryan
Edition: 2nd ed
Publisher: Cambridge University Press
Year: 2004
Language: English
Pages: 443
City: Cambridge [U.K.]; New York
Cover......Page 1
Half-title......Page 3
Title......Page 5
Copyright......Page 6
Contents......Page 7
Foreword to the first edition......Page 11
What’s new and what’s gone......Page 13
The interdependence of chapters and prerequisites......Page 14
Added for second edition......Page 15
1 Propositional logic......Page 17
1.1 Declarative sentences......Page 18
1.2 Natural deduction......Page 21
1.2.1 Rules for natural deduction......Page 22
1.2.2 Derived rules......Page 39
1.2.3 Natural deduction in summary......Page 42
1.2.5 An aside: proof by contradiction......Page 45
1.3 Propositional logic as a formal language......Page 47
1.4.1 The meaning of logical connectives......Page 52
1.4.2 Mathematical induction......Page 56
1.4.3 Soundness of propositional logic......Page 61
1.4.4 Completeness of propositional logic......Page 65
1.5 Normal forms......Page 69
1.5.1 Semantic equivalence, satisfiability and validity......Page 70
1.5.2 Conjunctive normal forms and validity......Page 74
1.5.3 Horn clauses and satisfiability......Page 81
1.6 SAT solvers......Page 84
1.6.1 A linear solver......Page 85
1.6.2 A cubic solver......Page 88
1.7 Exercises......Page 94
1.8 Bibliographic notes......Page 107
2.1 The need for a richer language......Page 109
2.2 Predicate logic as a formal language......Page 114
2.2.1 Terms......Page 115
2.2.2 Formulas......Page 116
2.2.3 Free and bound variables......Page 118
2.2.4 Substitution......Page 120
2.3.1 Natural deduction rules......Page 123
2.3.2 Quantifier equivalences......Page 133
2.4 Semantics of predicate logic......Page 138
2.4.1 Models......Page 139
2.4.2 Semantic entailment......Page 145
2.4.3 The semantics of equality......Page 146
2.5 Undecidability of predicate logic......Page 147
2.6 Expressiveness of predicate logic......Page 152
2.6.1 Existential second-order logic......Page 155
2.6.2 Universal second-order logic......Page 156
2.7 Micromodels of software......Page 157
2.7.1 State machines......Page 158
2.7.2 Alma – re-visited......Page 162
2.7.3 A software micromodel......Page 164
2.8 Exercises......Page 173
2.9 Bibliographic notes......Page 186
3.1 Motivation for verification......Page 188
3.2.1 Syntax of LTL......Page 191
3.2.2 Semantics of LTL......Page 194
3.2.3 Practical patterns of specifications......Page 199
3.2.4 Important equivalences between LTL formulas......Page 200
3.2.5 Adequate sets of connectives for LTL......Page 202
3.3.1 Example: mutual exclusion......Page 203
3.3.2 The NuSMV model checker......Page 207
3.3.3 Running NuSMV......Page 210
3.3.4 Mutual exclusion revisited......Page 211
3.3.5 The ferryman......Page 215
3.3.6 The alternating bit protocol......Page 219
3.4 Branching-time logic......Page 223
3.4.1 Syntax of CTL......Page 224
3.4.2 Semantics of computation tree logic......Page 227
3.4.4 Important equivalences between CTL formulas......Page 231
3.4.5 Adequate sets of CTL connectives......Page 232
3.5 CTL and the expressive powers of LTL and CTL......Page 233
3.5.1 Boolean combinations of temporal formulas in CTL......Page 236
3.6 Model-checking algorithms......Page 237
3.6.1 The CTL model-checking algorithm......Page 238
3.6.2 CTL model checking with fairness......Page 246
3.6.3 The LTL model-checking algorithm......Page 248
3.7 The fixed-point characterisation of CTL......Page 254
3.7.1 Monotone functions......Page 256
3.7.2 The correctness of SATEG......Page 258
3.7.3 The correctness of SATEU......Page 259
3.8 Exercises......Page 261
3.9 Bibliographic notes......Page 270
4 Program verification......Page 272
4.1 Why should we specify and verify code?......Page 273
4.2 A framework for software verification......Page 274
4.2.1 A core programming language......Page 275
4.2.2 Hoare triples......Page 278
4.2.3 Partial and total correctness......Page 281
4.2.4 Program variables and logical variables......Page 284
4.3.1 Proof rules......Page 285
4.3.2 Proof tableaux......Page 289
4.3.3 A case study: minimal-sum section......Page 303
4.4 Proof calculus for total correctness......Page 308
4.5 Programming by contract......Page 312
4.6 Exercises......Page 315
4.7 Bibliographic notes......Page 320
5.1 Modes of truth......Page 322
5.2.1 Syntax......Page 323
5.2.2 Semantics......Page 324
Equivalences between modal formulas......Page 329
Valid formulas......Page 330
5.3 Logic engineering......Page 332
5.3.1 The stock of valid formulas......Page 333
5.3.2 Important properties of the accessibility relation......Page 336
5.3.3 Correspondence theory......Page 338
5.3.4 Some modal logics......Page 342
5.4 Natural deduction......Page 344
5.5 Reasoning about knowledge in a multi-agent system......Page 347
5.5.1 Some examples......Page 348
5.5.2 The modal logic KT45n......Page 351
5.5.3 Natural deduction for KT45n......Page 355
5.5.4 Formalising the examples......Page 358
5.6 Exercises......Page 366
5.7 Bibliographic notes......Page 372
6.1 Representing boolean functions......Page 374
6.1.1 Propositional formulas and truth tables......Page 375
6.1.2 Binary decision diagrams......Page 377
6.1.3 Ordered BDDs......Page 382
6.2.1 The algorithm reduce......Page 388
6.2.2 The algorithm apply......Page 389
6.2.4 The algorithm exists......Page 393
6.2.5 Assessment of OBDDs......Page 396
6.3 Symbolic model checking......Page 398
6.3.1 Representing subsets of the set of states......Page 399
6.3.2 Representing the transition relation......Page 401
6.3.4 Synthesising OBDDs......Page 403
6.4.1 Syntax and semantics......Page 406
6.5 Exercises......Page 414
6.6 Bibliographic notes......Page 429
Bibliography......Page 430
Index......Page 434
