This Article 
 Bibliographic References 
 Add to: 
Some Aspects of the Verification of Loop Computations
November 1978 (vol. 4 no. 6)
pp. 478-486
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.
Index Terms:
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, Nov. 1978, doi:10.1109/TSE.1978.233871
Usage of this product signifies your acceptance of the Terms of Use.