Program Construction and Reasoning

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.

Course Materials

Prerequisites

Outline

Part 1: Hoare Logic and Guarded Command Language

  • 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

Part 2: Program Derivation

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

Part 3: "Goto considered harmful" and Related Stories

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

References

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:

 
en/prog.txt · Last modified: 2010/07/04 12:45 (external edit)
Recent changes · Show pagesource · Login