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
