Accession Number:

ADA090487

Title:

A Comparative Analysis of Functional Correctness.

Descriptive Note:

Technical rept.,

Corporate Author:

MARYLAND UNIV COLLEGE PARK DEPT OF COMPUTER SCIENCE

Personal Author(s):

• Dunlop,Douglas D.
• Basili,Victor R.

Report Date:

1980-08-01

Pagination or Media Count:

26.0

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

Descriptors:

• *COMPUTER PROGRAMMING
• *FUNCTIONAL ANALYSIS
• *COMPUTER PROGRAM VERIFICATION
• *INVARIANCE
• RANDOM VARIABLES
• SEMANTICS
• COMPUTER APPLICATIONS
• ITERATIONS
• INPUT OUTPUT MODELS
• FUNCTIONS(MATHEMATICS)
• CLOSED LOOP SYSTEMS
• EQUATIONS OF STATE
• THEOREMS

Subject Categories:

• Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE