The Semiautomatic Generation of Inductive Assertions for Proving Program Correctness.
Interim rept. 1 Jul 74-30 Jun 77,
SRI INTERNATIONAL MENLO PARK CALIF
Pagination or Media Count:
This interim report describes progress on a project aimed at solving a serious problem that has been encountered in attempts to make program correctness proving a practical technique for software verification. The principal problem addressed here is the difficulty of synthesizing so-called loop assertions in connection with the main method now under study for program proving. Several rather diverse approaches, some of them constituting such alternatives to the present technique, are considered here transformation of programs into primitive recursive form before verification, the method of generator induction for proof of properties of complex data structures, the use of a hierarchical design methodology to structure programs so as to minimize the need for loop assertions, and methods related to subgoal induction and computational induction. The two latter methods were analyzed in detail and compared with the present approach to arrive at a better understanding of their mutual relationships.
- Computer Programming and Software
- Computer Hardware