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