Program Verification in the 1980s: Problems, Perspectives, and Opportunities.

摘要

Properties of programs can be mathematically proved. This report concerns the use of such mathematical proofs as a means of verifying that programs satisfy their specifications and other expectations of proper behavior. Moreover, the theory by means of which programs are proved can be used in the formal reasoning needed to construct and maintain programs. The primary current needs are: (1) expansion of the theory to encompass more aspects of program correctness; (2) evolution of the theory's mathematical content and form to make it more effective in verifying programs; and (3) experimentation with new and current techniques for using the theory in verification and construction; (4) development of human knowledge and skills to fulfill human roles of specifying and guiding program proofs; (5) technological support to take over mechanical parts of the proofs and follow human guidance in elaborating them. The needed breakthroughs toward the use of program proving as a normal programming activity are: (1) a coherent connection with program testing; (2) evolution of the theory to the point where significant amounts of new program proofs are adapted or reused from previous proofs; (3) development of experimental methodology for effectively evaluating various paradigms and techniques for program proving; (4) greatly increased mechanical theorem proving capacity to reduce the burden on human verifiers; and (5) large-scale demonstrations or program proving to evaluate the validity of the activity and to stimulate future research and development.