Program Correctness

Introduction

Robert W Floyd (Source: Stanford Computer Science).

We present a project for students on proving the correctness of a program, studied by reading excerpts from the pioneering paper of Robert W. Floyd (1936-2001) on “Assigning meanings to programs” [1].

Another pioneering paper in program correctness was C. A. R. Hoare’s “An axiomatic basis for computer programming” [2]. Almost all treatments of program correctness in advanced textbooks are based on Hoare’s logical or axiomatic approach, in which mathematical axioms and inference rules are employed. But as Hoare admitted, “The formal treatment of program execution presented in this paper is clearly derived from Floyd” [2, p. 583] and the treatment “is essentially due to Floyd but is applied to texts rather than flowcharts” [2, p. 577]. That is, conceptually Hoare’s method is no different than Floyd’s. However, Hoare’s axiomatic approach, which is presented with the notation and terminology of axioms and inference rules, may be quite difficult for an upper level computer science undergraduate student. In practice, Hoare’s technique, while based on axioms and inference rules, is often carried out by annotating a program with assertions.

In Floyd’s approach, programs are presented as flowcharts. One may wonder if flowchart programs are realistic, and whether Floyd’s technique applies to programs that people write nowadays. In this project, we propose to replace flowchart programs by assembly-like programs with the use of “goto” statements. Each statement is accompanied by an assertion.

By adopting assembly-like programs as our preferred programming style, we are able to present the correctness proof technique in a simple and unified manner without the need to revise the technique for each new programming language. We assume that a junior level computer science student is able to convert mechanically a program in a high level language into an assembly-like program. As the mechanical conversion preserves the same program execution behavior, we can establish the correctness of the original program in a high level language by proving the correctness of the derived assembly-like program.

Our project, Program Correctness, is ready for students, and the Latex source is also available for instructors who may wish to modify the project for students. The comprehensive “Notes to the Instructor” presented next are also appended to the project itself. Our project is part of a larger collection published in Convergence. For additional projects, see Primary Historical Sources in the Classroom: Discrete Mathematics and Computer Science.

Notes to the Instructor

The project is designed to focus on the key ideas in program correctness, rather than on the formal aspects of the theory. Terminology like axioms, inferences, and deductive systems is deliberately avoided. Emphasis is placed on the practice of proving the partial correctness of interesting programs. It is the author’s belief that the students will appreciate better the power of program correctness through the analysis of seemingly simple and yet non-trivial programs. Furthermore, the students will hopefully learn how to write better programs as a result of this study.

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.

Floyd’s flowchart program for correctness proof is an excellent example. The instructor should go over this example slowly. Students should be given ample time to analyze the annotations given in the flowchart program. The objective is to develop an informal understanding through the induction principle that the annotations together constitute a partial correctness proof.

The correctness proof (Task 13) of the Partition procedure is very challenging. It may be skipped if time is limited, or if the students are finding it too difficult. Students can also tackle Task 13 collaboratively. Work can be assigned in three parts (Tasks 1-10, Tasks 11-12, and Task 13) with one week given for each part. Task 14 can be considered as extra credit. After students’ answers for the first part (Tasks 1-10) have been turned in, the instructor can discuss the uses of back substitution (as given in the verification condition for the assignment operator) that are required for the answers for Tasks 9 and 10, so as to be sure that the students are ready to take on the tasks given in Sections 5, 6 and 7.

The project does not cover termination proof. Unlike partial correctness proof, the concept of termination proof is quite straightforward. Students will find good discussions of termination proof in their textbooks.

Finally, students may be interested to know that both Robert Floyd and Tony Hoare were awarded the Alan M. Turing Award, generally considered to be the highest award in computer science, Floyd in 1978 [5] and Hoare in 1980 [3].

Download the project Program Correctness as a pdf file ready for classroom use.

Download the modifiable Latex source file for this project.

For more projects, see Primary Historical Sources in the Classroom: Discrete Mathematics and Computer Science.

Bibliography

[1] Floyd, Robert W., “Assigning meanings to programs,” Proceedings of Symposia in Applied Mathematics, Vol. 19 (1967), pages 19–32.

[2] Hoare, C. A. R., “An axiomatic basis for computer programming,” Communications of the ACM, Vol. 12, No. 10 (1969), pages 576–583.

[3] Jones, Cliff, “C. Antony (“Tony”) R. Hoare, United Kingdom – 1980,” Association for Computing Machinery (ACM) A. M. Turing Award website, 2012, 
http://amturing.acm.org/award_winners/hoare_4622167.cfm

[4] Levy, Dawn, “Professor Robert W. Floyd,” In Memorium, Stanford University Computer Science website, September 2001, 
http://www-cs.stanford.edu/faculty/memoriam
http://www-cs.stanford.edu/content/professor-robert-w-floyd

[5] “Robert (Bob) W Floyd, United States – 1978,” Association for Computing Machinery (ACM) A. M. Turing Award website, 2012, 
http://amturing.acm.org/award_winners/hoare_4622167.cfm

Acknowledgment



The development of curricular materials for discrete mathematics has been partially supported by the National Science Foundation's Course, Curriculum and Laboratory Improvement Program under grants DUE-0717752 and DUE-0715392 for which the authors are most appreciative. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation.