Program Construction and Reasoning
Lecturer: 穆信成 Shin-Cheng Mu
Bird-Meertens style functional program derivation.
Lecture notes and slides. To be announced here.
Day 1. The Expand/Reduce Transformation(2 hours)
- Prelude: Maximum Segment Sum
- Data Structures
- The Expand/Reduce Transformation
- Example: Sum of Squares
- Proving Properties by Induction
- Accumulating parameters
Day 2. Fold, Unfold, and Hylomorphism (2 hours)
- The Fold-Fusion Theorem
- More Useful Functions as Folds
- Finally, Solving Maximum Segment Sum!
- Folds on Trees
- Unfold on Lists
- Folds v.s. Unfolds
- A Museum of Sorting Algorithms
- Hylomorphism and Recursion
- Wrapping Up
Day 3. Procedural Program Derivation (2 hours)
- The Guarded Command Language
- Assignments and Selection
- Procedural Program Derivation
- Taking Conjuncts as Invariants
- Replacing Constants by Variables
- Strengthening the Invariant
- Tail Invariants
- Maximum Segment Sum, Procedually
- Wrapping Up
- Richard S. Bird. Introduction to Functional Programming using Haskell.
- Richard S. Bird and Oege de Moor. Algebra of Programming. Only the functional part.
- Some papers from H. Zantema on list segment problems.
- Anne Kaldewaij. Programming: The Derivation of Algorithms (Prentice Hall, 1990).
- Roland Backhouse. Program Construction: Calculating Implementations from Specifications. John Wiley and Sons, 2003.
- Edsgar W. Dijkstra. A Discipline of Programming. Prentice Hall, 1976.
- David Gries. The Science of Programming. Springer, 1987.