Software Foundations Logo
Volume 3: Verified Functional Algorithms
  • Table of Contents
  • Index
  • Roadmap

Preface

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

Basic Techniques for Comparisons and Permutations    (Perm)

  • The Less-Than Order on the Natural Numbers
  • Swapping
    • Reflection
    • A Tactic for Boolean Destruction
    • Finishing the maybe_swap Proof
  • Permutations
    • Correctness of maybe_swap
  • An Inversion Tactic

Insertion Sort    (Sort)

  • The Insertion-Sort Program
  • Specification of Correctness
  • Proof of Correctness

Insertion Sort Verified With Multisets    (Multiset)

  • Multisets
  • Specification of Sorting
  • Verification of Insertion Sort
  • Equivalence of Permutation and Multiset Specifications

Insertion Sort With Bags    (BagPerm)

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

Selection Sort    (Selection)

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

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

    • Split and its properties
    • Defining Merge
    • Defining Mergesort
    • Correctness: Sortedness
    • Correctness: Permutation

Binary Search Trees    (SearchTree)

  • BST Implementation
  • BST Invariant
  • Correctness of BST Operations
  • Converting a BST to a List
    • Part 1: Same Bindings
    • Part 2: Sorted (Advanced)
    • Part 3: No Duplicates (Advanced and Optional)
  • A Faster elements Implementation
  • An Algebraic Specification of elements
  • Model-based Specifications
  • Efficiency of Search Trees

Abstract Data Types    (ADT)

  • The Table ADT
  • Implementing Table with Functions
    • Encapsulation
  • Implementing Table with Lists
  • Implementing Table with BSTs
  • Tables with an elements Operation
    • A First Attempt at ETable
    • A Second Attempt at ETable
    • A Final Attempt at ETable
  • Model-based Specification
  • Summary of ADT Verification
  • Representation Invariants and Subset Types
    • Example: The Even Naturals
    • Defining Subset Types
    • Using Subset Types to Enforce the BST Invariant

Running Coq Programs in OCaml    (Extract)

  • Extraction
  • Lightweight Extraction to int
  • Insertion Sort, Extracted
  • Binary Search Trees, Extracted
  • Performance Tests

Red-Black Trees    (Redblack)

  • Implementation
  • Case-Analysis Automation
  • The BST Invariant
  • Verification
  • Efficiency
  • Performance of Extracted Code

Number Representations and Efficient Lookup Tables    (Trie)

  • 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)

  • 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)

  • 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)

  • 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)

  • 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