Some Aspects of the Verification of Loop Computations

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.