Issue No.04 - December (1976 vol.2)
D. Gries , Department of Computer Science, Cornell University
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.
programming language semantics, Correctness proof, derivation of programs, programming methodology
D. Gries, "An Illustration of Current Ideas on the Derivation of Correctness Proofs and Correct Programs", IEEE Transactions on Software Engineering, vol.2, no. 4, pp. 238-244, December 1976, doi:10.1109/TSE.1976.233828