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 (