
Accession Number : ADA113040
Title : An Investigation of Functional Correctness Issues.
Descriptive Note : Doctoral thesis.
Corporate Author : MARYLAND UNIV COLLEGE PARK COMPUTER SCIENCE CENTER
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