A Comparative Analysis of Functional Correctness.

Abstract

The functional correctness technique is presented and explained. An implication of the underlying theory for the derivation of loop invariants is discussed. The functional verification conditions concerning program loops are shown to be a specialization of the commonly used inductive assertion verification conditions. The functional technique is compared and contrasted with subgoal induction. Finally, the difficulty of proving initialized loops is examined in light of the inductive assertion and functional correctness theories. (Author)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 01, 1980
Accession Number
ADA090487

Entities

People

  • Douglas D. Dunlop
  • Victor Basili

Organizations

  • University of Maryland

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Air Force
  • Behavior And Behavior Mechanisms
  • Computer Science
  • Computers
  • Decomposition
  • Human Behavior
  • Hypotheses
  • Identities
  • Iterations
  • Language
  • Maryland
  • Notation
  • Security
  • Specifications
  • Universities
  • Verification

Readers

  • Mathematical Modeling and Probability Theory.
  • Regression Analysis.