Preface

1 Introduction -- 1.1 Motivation for This Book -- 1.2 Lessons from Programming Theory -- 1.3 Formalism: The Good, the Bad and the Ugly

2 Set Theory, Logic and Proofs -- 2.1 Set -- 2.2 Function -- 2.3 Relation -- 2.4 Order Relations: Totaland Partial -- 2.5 Propositional Logic -- 2.6 Predicate Calculus -- 2.7 Formal Proofs -- 2.8 Examples of Proof Construction -- 2.9 Exercises

3 Induction and Recursion -- 3.1 Introduction -- 3.2 Examples of Proof by Induction -- 3.3 Methodologies for Applying Induction -- 3.4 Advanced Examples -- 3.5 Noetherian or Well-founded Induction -- 3.6 Structural Induction -- 3.7 Exercises

4 Reasoning About Programs -- 4.1 Overview -- 4.2 Fundamental Ideas -- 4.3 Formal Treatment of Partial Correctness -- 4.4 A Modest Programming Language -- 4.5 Proof Rules -- 4.6 More on Invariant -- 4.7 Formal Treatment of Termination -- 4.8 Reasoning about Performance of Algorithms -- 4.9 Order of Functions -- 4.10 Recurrence Relations -- 4.11 Proving Programs in Practice -- 4.12 Exercises -- 4.A Appendix: Proof of Theorem -- 4.B Appendix: Termination in Chameleons Problem

5 Program Development -- 5.1 Binary Search -- 5.2 Saddleback Search -- 5.3 Dijkstra's Proof of the am-gm Inequality -- 5.4 Quicksort -- 5.5 Heapsort -- 5.6 Knuth-Morris-Pratt String-matching Algorithm -- 5.7 A Sieve Algorithm for Prime Numbers -- 5.8 Stable Matching -- 5.9 Heavy-hitters: A Streaming Algorithm -- 5.10 Exercises

6 Graph Algorithms -- 6.1 Introduction -- 6.2 Background -- 6.3 Specific Graph Structures -- 6.4 Combinatorial Applications of Graph Theory -- 6.5 Reachability in Graphs -- 6.6 Graph Traversal Algorithms -- 6.7 Connected Components of Graphs -- 6.8 Transitive Closure -- 6.9 Single Source Shortest Path -- 6.10 Minimum Spanning Tree -- 6.11 Maximum Flow -- 6.12 Goldberg-Tarjan Algorithm for Maximum Flow -- 6.13 Exercises -- 6.A Appendix: Proof of the Reachability Program -- 6.B Appendix: Depth-first Traversal

7 Recursive and Dynamic Programming -- 7.1 What is Recursive Programming -- 7.2 Programming Notation -- 7.3 Reasoning About Recursive Programs -- 7.4 Recursive Programming Methodology -- 7.5 Recursive Data Types -- 7.6 Dynamic Programming -- 7.7 Exercises -- 7.A Appendices

8 Parallel Recursion -- 8.1 Parallelism and Recursion -- 8.2 Powerlist -- 8.3 Pointwise Function Application -- 8.4 Proofs -- 8.5 Advanced Examples Using Powerlists -- 8.6 Multi-dimensional Powerlist -- 8.7 Other Work on Powerlist -- 8.8 Exercises -- 8.A Appendices

Bibliography

Authors' Biographies

Index

Abstract freely available; full-text restricted to subscribers or individual document purchasers.

Also available in print.

Mode of access: World Wide Web

System requirements: Adobe Acrobat Reader