Accession Number : ADA113040

Title :   An Investigation of Functional Correctness Issues.

Descriptive Note : Doctoral thesis.


Personal Author(s) : Dunlop,Douglas D

PDF Url : ADA113040

Report Date : Jan 1982

Pagination or Media Count : 103

Abstract : Given a program and an abstract functional specification that the program is intended to satisfy, a fundamental question is whether the program executes in accordance with (i.e. is correct with respect to) the specification. A simple functional correctness technique is initially defined which is based on prime program decomposition of composite programs. This technique is analyzed and the problems of the need for each intended loop function and the inflexibility of the prime program decomposition strategy are discussed. The notion of a reduction hypothesis is then defined which can be used in the place of an intended loop function in the verification process. Furthermore, an efficient proof decomposition strategy for composite programs is suggested which is based on a sequence of proof transformations. (Author)

Descriptors :   *Computer program verification, *Corrections, Specifications, Loops, Functions, Reduction, Hypotheses, Efficiency, Strategy, Sequences, Heuristic methods, Theses

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE