Program Correctness

Abstract

We present a project for students on proving the correctness of a program, studied by reading excerpts from Robert Floyd’s pioneering paper on “Assigning meanings to programs,”  which appeared in 1967. The project is designed to focus on the key ideas in program correctness, rather than on the formal aspects of the theory that is usually presented in an axiomatic introduction to the topic. Terminology such as axioms, inferences, and deductive systems is deliberately avoided. Emphasis is placed on the practice of proving the partial correctness of interesting programs.The project is suitable for an undergraduate upper-level algorithms course or programming languages course. Most of the work can be completed by the students individually.