The teaching of program correctness

For the past seven years, including three years at the University of California (Berkeley) and four years at The George Washington University, this author has taught material relating to the correctness of programs in both undergraduate and graduate courses. The simplest material on correctness that we teach is the proof of correctness of Euclid's algorithm, implemented as a program in FORTRAN, AL-GOL 60, PL/I, or BASIC, depending on the language to which elementary students are first introduced. (It would work just as easily in PASCAL.) This proof is found in (1), pp. 14-20. We usually give a simplified version of it, because the program in (1), for purposes of efficiency, works by dividing and taking the remainder, and we feel it is easier to illustrate the relevant concepts by using an algorithm that works by simple subtractions.