Abstract
This paper formally describes a technique for proving that computer programs will always execute correctly. In order to do this, an abstract model for a program and its execution is given. Then, correctness of programs and proofs of correctness of programs are defined with respect to that model. Copyright © 1971 by The Institute of Electrical and Electronics Engineers, Inc.