Volume 3: Verified Functional Algorithms

  • Table of Contents
    •
  • Index
    •
  • Roadmap
    •

Preface

  • Top
  • Welcome
  • Practicalities
    • Chapter Dependencies
    • System Requirements
    • Exercises
    • Downloading the Coq Files
    • Lecture Videos
    • For Instructors and Contributors
  • Thanks

Basic Techniques for Permutations and Ordering    (Perm)

  • Top
  • The Less-Than Order on the Natural Numbers
    • Relating Prop to bool
    • A Tactic for Boolean destruction
    • Linear Integer Inequalities
  • Permutations
  • Summary: Comparisons and Permutations

Insertion Sort    (Sort)

  • Top
  • Recommended Reading
  • The Insertion-Sort Program
  • Specification of Correctness
  • Proof of Correctness
  • Making Sure the Specification is Right
  • Proving Correctness from the Alternate Spec
    • The Moral of This Story

Insertion Sort With Multisets    (Multiset)

  • Top
  • Correctness
  • Permutations and Multisets
  • The Main Theorem: Equivalence of Multisets and Permutations

Selection Sort, With Specification and Proof of Correctness    (Selection)

  • Top
  • The Selection-Sort Program
  • Proof of Correctness of Selection sort
  • Recursive Functions That are Not Structurally Recursive

Binary Search Trees    (SearchTree)

  • Top
  • Total and Partial Maps
  • Sections
  • Binary Search Tree Implementation
  • Search Tree Examples
  • Efficiency of BSTs
  • What Should We Prove About Search trees?
  • Abstraction Relation
  • Proof of Correctness
  • Correctness Proof of the elements Function
  • Representation Invariants
    • Auxiliary Lemmas About In and list2map
  • Preservation of Representation Invariant
  • We Got Lucky
  • Every Well-Formed Tree Does Actually Relate to an Abstraction
  • It Wasn't Really Luck, Actually
    • Coherence With elements Instead of lookup
  • Implementation

Abstract Data Types    (ADT)

  • Top
  • A Brief Excursion into Dependent Types
    • Search Trees using Sigma Types
  • Summary of Abstract Data Type Proofs
  • Exercise in Data Abstraction

Running Coq Programs in OCaml    (Extract)

  • Top
  • Utilities for OCaml Integer Comparisons
  • SearchTrees, Extracted
    • Maps, on Z Instead of nat
    • Trees, on int Instead of nat
  • Performance Tests

Implementation and Proof of Red-Black Trees    (Redblack)

  • Top
  • Required Reading
  • Implementation
  • Verification
  • Proof Automation for Case-Analysis Proofs.
  • Verifying Preservation of the Representation Invariant
    • Empty and SearchTree
    • Balance and SearchTree
    • Insert and SearchTree
  • Verifying Correctness w.r.t. the Abstraction Relation
    • Empty and Abs
    • Lookup and Abs
    • Balance and Abs
    • Insert and Abs
    • Optional: Verification of Elements
  • Verification of Balance
    • The Red-Black Invariants
    • Empty and RB
    • Insert and RB
  • Extracting and Measuring Red-Black Trees
  • Success!

Number Representations and Efficient Lookup Tables    (Trie)

  • Top
  • LogN Penalties in Functional Programming
  • A Simple Program That's Waaaaay Too Slow.
  • Efficient Positive Numbers
    • Coq's Integer Type, Z
    • From N*N*N to N*N*logN
    • From N*N*logN to N*logN*logN
  • Tries: Efficient Lookup Tables on Positive Binary Numbers
    • From N*logN*logN to N*logN
  • Proving the Correctness of Trie Tables
    • Lemmas About the Relation Between lookup and insert
    • Bijection Between positive and nat.
    • Proving That Tries are a "Table" ADT.
    • Sanity Check
  • Conclusion

Priority Queues    (Priqueue)

  • Top
  • Module Signature
  • Implementation
    • Some Preliminaries
    • The Program
  • Predicates on Priority Queues
    • The Representation Invariant
    • Sanity Checks on the Abstraction Relation
    • Characterizations of the Operations on Queues

Binomial Queues    (Binom)

  • Top
  • Required Reading
  • The Program
  • Characterization Predicates
  • Proof of Algorithm Correctness
    • Various Functions Preserve the Representation Invariant
    • The Abstraction Relation
    • Sanity Checks on the Abstraction Relation
    • Various Functions Preserve the Abstraction Relation
    • Optional Exercises
  • Measurement.

Programming with Decision Procedures    (Decide)

  • Top
  • Using reflect to characterize decision procedures
  • Using sumbool to Characterize Decision Procedures
    • sumbool in the Coq Standard Library
  • Decidability and Computability
  • Opacity of Qed
  • Advantages and Disadvantages of reflect Versus sumbool

Graph Coloring    (Color)

  • Top
  • Preliminaries: Representing Graphs
  • Lemmas About Sets and Maps
    • equivlistA
    • SortA_equivlistA_eqlistA
    • S.remove and S.elements
    • Lists of (key,value) Pairs
    • Cardinality
  • Now Begins the Graph Coloring Program
    • Some Proofs in Support of Termination
    • The Rest of the Algorithm
  • Proof of Correctness of the Algorithm.
  • Trying Out the Algorithm on an Actual Test Case