An Illustration of Current Ideas on the Derivation of Correctness Proofs and Correct Programs
David Gries · IEEE Transactions on Software Engineering · 1976
The ideas behind correctness proofs for programs are outlined, and conventional definitions of assignment, etc., are given. The main part of this paper is the idealized development of a nontrivial program in a disciplined fashion. The use of Dijkstra's "calculus" for the formal development of programs as a guide to structuring program development is discussed in relation to the example presented.