An Investigation of Functional Correctness Issues.

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)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1982
Accession Number
ADA113040

Entities

People

  • Douglas D. Dunlop

Organizations

  • University of Maryland

Tags

DTIC Thesaurus Topics

  • Air Force
  • Artificial Intelligence
  • Composite Materials
  • Computations
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Identities
  • Sequences
  • Software Development
  • Specifications
  • Standards
  • Structured Programming
  • Theses
  • Trees (Data Structures)
  • Verification

Fields of Study

  • Computer science
  • Engineering

Readers

  • Computer Science.
  • Mathematical Modeling and Probability Theory.
  • Systems Analysis and Design