Accession Number:

ADA050154

Title:

The Semiautomatic Generation of Inductive Assertions for Proving Program Correctness.

Descriptive Note:

Interim rept. 1 Jul 74-30 Jun 77,

Corporate Author:

SRI INTERNATIONAL MENLO PARK CALIF

Report Date:

1977-11-01

Pagination or Media Count:

126.0

Abstract:

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.

Subject Categories:

  • Computer Programming and Software
  • Computer Hardware

Distribution Statement:

APPROVED FOR PUBLIC RELEASE