Search

The purpose of this paper is to point out the significant quantity of work in progress on techniques that will enable programmers to prove their programs correct. This work has included: investigations in the theory of program schemas or abstract programs; development of the art of the informal or manual proof of correctness; and development of mechanical or semi-mechanical approaches to proving correctness. At present, these mechanical approaches rely upon the availability of powerful theorem-provers, development of which is being actively pursued. All of these technical areas are here surveyed in detail, and recommendations are made concerning the direction of future research toward producing a semi mechanical program verifier. [ABSTRACT FROM AUTHOR]