A versatile concept for the analysis of loops

Ever since their introduction by Hoare in 1969, invariant assertions have, justifiably, played a key role in the analysis of while loops. In this paper, we discuss a distinct but related concept, viz invariant relations, and show how these can be used to answer many questions pertaining to the analysis of loops, including: how to compute the function of the loop; how to compute an invariant assertion of the loop; how to compute a weakest precondition of the loop; how to compute a strongest postcondition of the loop; how to compute the termination condition of a loop; how to verify whether the loop computes a given function; how to verify whether the loop is correct with respect to a given specification; and finally how to compute an invariant function for the loop. Using a tool we have developed at the University of Tunis to derive invariant relations, we show how all these tasks can be automated by means of a computer algebra system, viz Mathematica (©Wolfram Research). Whenever applicable, we compare the performance of our tool against the performance of others.

► All invariant assertions stem from invariant relations, though the inverse is not true. ► Invariant relations can be used to prove partial correctness as well as termination. ► Invariant relations enable us to conclusively determine whether a loop is correct or not. ► While invariant assertions depend on the context of a loop, invariant relations do not.