On program verification and easy to veryfy programming

In the first part of the paper, a discussion of program verification techniques is given. After a brief survey of formal and informal methods for proving the correctness of programs, special attention is focused on programs involving compound recursion since, in many instances in computer science (e. g. parsing of BNF languages), compound recursion provides the most natural way of stating the problem to be solved. Several examples of proving such programs are discussed and the ease of proving them is commented on. Then, ways of writing programs which simplify verification are discussed. The problem of writing a PL/1 program using based variables for setting up and processing a deque is given and programs written with and without proof techniques in mind are compared for ease of verification as well as efficiency. Finally, conclusions are drawn about how the “top-down” design process could help in the proof of programs.