Maps: Total and Partial Maps
Preface
Perm: Basic Techniques for Permutations and Ordering
Sort: Insertion Sort
- Recommended Reading
- The Insertion-Sort Program
- Specification of Correctness
- Proof of Correctness
- Making Sure the Specification is Right
- Proving Correctness from the Alternate Spec
Multiset: Insertion Sort With Multisets
Selection: Selection Sort, With Specification and Proof of Correctness
- The Selection-Sort Program
- Proof of Correctness of Selection sort
- Recursive Functions That are Not Structurally Recursive
SearchTree: Binary Search Trees
- Total and Partial Maps
- Sections
- Program for Binary Search Trees
- Search Tree Examples
- What Should We Prove About Search trees?
- Efficiency of Search Trees
- Proof of Correctness
- Correctness Proof of the elements Function
- Representation Invariants
- Preservation of Representation Invariant
- We Got Lucky
- Every Well-Formed Tree Does Actually Relate to an Abstraction
- It Wasn't Really Luck, Actually
ADT: Abstract Data Types
- A Brief Excursion into Dependent Types
- Summary of Abstract Data Type Proofs
- Exercise in Data Abstraction
Extract: Running Coq programs in ML
- Utilities for OCaml Integer Comparisons
- SearchTrees, Extracted
- Performance Tests
- Unbalanced Binary Search Trees
- Balanced Binary Search Trees
Redblack: Implementation and Proof of Red-Black Trees
- Required Reading
- Proof Automation for Case-Analysis Proofs.
- The SearchTree Property
- Proving Efficiency
- Extracting and Measuring Red-Black Trees
- Success!
Trie: Number Representations and Efficient Lookup Tables
- LogN Penalties in Functional Programming
- A Simple Program That's Waaaaay Too Slow.
- Efficient Positive Numbers
- Tries: Efficient Lookup Tables on Positive Binary Numbers
- Proving the Correctness of Trie Tables
- Conclusion
Priqueue: Priority Queues
Binom: Binomial Queues
- Required Reading
- The Program
- Characterization Predicates
- Proof of Algorithm Correctness
- Measurement.
Decide: Programming with Decision Procedures
- Using reflect to characterize decision procedures
- Using sumbool to Characterize Decision Procedures
- Decidability and Computability
- Opacity of Qed
- Advantages and Disadvantages of reflect Versus sumbool