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

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

prog.txt · 上一次變更: 2010/07/04 12:45 來自 scm