The Semiautomatic Generation of Inductive Assertions for Proving Program Correctness.
Abstract
This report presents results of the first year of research on semiautomatic techniques for the development of inductive assertions to be used in proving the correctness of programs by the method of Floyd. The principal technique that has been investigated is the use of finite difference equations to characterize the overall action on program variables of executing a program control loop. It is shown that in many significant cases such difference equations can be solved--either manually, or, more importantly, with the aid of a mechanical deductive system--to yield a subset of the required inductive assertions that hold every time control returns to the head of a loop. It has been found that the remaining inductive assertions can generally be determined by application of heuristic techniques involving an 'outside-in' analysis of the program in conjunction with its input-output specifications.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 01, 1974
- Accession Number
- ADA003711
Entities
People
- Bernard Elspas
Organizations
- SRI International