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!).

- Introduction: On Programs Correctness
- The Maximum Segment Sum Problem
- The Binary Search Challenge

- Program Verication 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?
- Quantifier 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.

Powered by Dokuwiki. Template derived from mmClean, courtesy of zenzire. Banner image courtesy of aireheru, distributed under CC 2.0-by-nc-sa.