DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click HERE
to register or log in.
A Comparative Analysis of Functional Correctness.
MARYLAND UNIV COLLEGE PARK DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
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
APPROVED FOR PUBLIC RELEASE