zh-tw:progc [2012 Formosan Summer School on Logic, Language, and Computation (FLOLAC '12)]

Program Construction and Reasoning

Lecturer: 穆信成 Shin-Cheng Mu

Bird-Meertens style functional program derivation.

Course Materials

Lecture notes and slides. To be announced here.

Prerequisites

Outline

Day 1. The Expand/Reduce Transformation(2 hours)

  • Prelude: Maximum Segment Sum
  • Preliminaries
    • Functions
    • Data Structures
  • The Expand/Reduce Transformation
    • Example: Sum of Squares
    • Proving Properties by Induction
    • Accumulating parameters
    • Tupling

Day 2. Fold, Unfold, and Hylomorphism (2 hours)

  • Folds
    • The Fold-Fusion Theorem
    • More Useful Functions as Folds
    • Finally, Solving Maximum Segment Sum!
    • Folds on Trees
  • Unfolds
    • Unfold on Lists
  • Folds v.s. Unfolds
  • Hylomorphism
    • A Museum of Sorting Algorithms
    • Hylomorphism and Recursion
  • Wrapping Up

Day 3. Procedural Program Derivation (2 hours)

  • The Guarded Command Language
    • Assignments and Selection
    • Repetition
  • Procedural Program Derivation
    • Taking Conjuncts as Invariants
    • Replacing Constants by Variables
    • Strengthening the Invariant
    • Tail Invariants
  • Maximum Segment Sum, Procedually
  • Wrapping Up

References

Suggested Reading: