Issue No.06 - November (1978 vol.4)
J. Misra , Department of Computer Science, University of Texas
The problem of proving whether or not a loop computes a given function is investigated. We consider loops which have a certain "closure" property and derive necessary and sufficient conditions for such a loop to compute a given function. It is argued that closure is a fundamental concept in program proving. Extensions of the basic result to proofs involving relations other than functional relations, which typically arise in nondeterministic loops, are explored. Several applications of these results are given, particularly in showing that certain classes of programs may be directly proven (their loop invariants generated) given only their input-output relationships. Implications of these results are discussed.
proving program schemas, Inductive assertions, loop invariants, nondeterministic programs, program verification, proof rules, proving programs correct
J. Misra, "Some Aspects of the Verification of Loop Computations", IEEE Transactions on Software Engineering, vol.4, no. 6, pp. 478-486, November 1978, doi:10.1109/TSE.1978.233871