Preface
Basic Techniques for Comparisons and Permutations (Perm)
Insertion Sort (Sort)
Insertion Sort Verified With Multisets (Multiset)
Insertion Sort With Bags (BagPerm)
Selection Sort (Selection)
Merge Sort, With Specification and Proof of Correctness (Merge)
Total and Partial Maps (Maps)
Binary Search Trees (SearchTree)
- BST Implementation
- BST Invariant
- Correctness of BST Operations
- BSTs vs. Higher-order Functions (Optional)
- Converting a BST to a List
- A Faster elements Implementation
- An Algebraic Specification of elements
- Model-based Specifications
- An Alternative Abstraction Relation (Optional, Advanced)
- Efficiency of Search Trees
Abstract Data Types (ADT)
- The Table ADT
- Implementing Table with Functions
- Implementing Table with Lists
- Implementing Table with BSTs
- Tables with an elements Operation
- Encapsulation with the Coq Module System (Advanced)
- Model-based Specification
- Summary of ADT Verification
- Another ADT: Queue
- Representation Invariants and Subset Types