Lecturer: 穆信成 Shin-Cheng Mu

This course gives an introduction to derivation and verification of imperative programs using Hoare Logic and Dijkstra's weakest precondition calculus. After learning how to verify the correctness of a program by checking the validity of its Hoare triple annotation, we introduce a systematic approach to program construction and problem solving by discovering possibly useful loop invariants. It is emphasized that a program and its correctness proof shall be constructed together. Examples covered include the famous maximum segment sum problem, the Dutch national flag, and binary search, a problem much more difficult to get right than it seems.

• Lecture notes and slides (up to last-minute changes!).
• In-class exercise 1 (answers), exercise 2 (answers), exercise 3.

Logic.

• Introduction: On Programs Correctness
  • The Maximum Segment Sum Problem
  • The Binary Search Challenge
• Program Verication using Hoare Logic
  • Assignments
  • Sequencing
  • Selection
  • Loop and Loop Invariants
• Binary Search Revisited
  • The van Gasteren-Feijen Approach
  • Searching in a Sorted List
  • Searching with Premature Return

• What is a Proof, Anyway?
• Quantifier Manipulation
• Loop Construction
  • Taking Conjuncts as Invariants
  • Replacing Constants by Variables
  • Strengthening the Invariant
  • Tail Invariants
• Maximum segment sum solved
• Where to Go from Here?

• A brief history of ALGOL and its first compiler
• On “Goto considered harmful”
• On “Structured programming with goto”

Most of the technical contents will be extracted from Anne Kaldewaij's book Programming: The Derivation of Algorithms (Prentice Hall, 1990). Other related books include:

• 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.