The Semiautomatic Generation of Inductive Assertions for Proving Program Correctness.
Interim rept. 1 May 73-31 May 74,
STANFORD RESEARCH INST MENLO PARK CALIF
Pagination or Media Count:
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.
- Computer Programming and Software