Invariant Relations: An Automated Tool to Analyze Loops

Since their introduction more than four decades ago, invariant assertions have, justifiably, dominated the analysis of while loops, and have been the focus of sustained research interest in the seventies and eighties, and renewed interest in the last decade. In this paper, we tentatively submit an alternative concept for the analysis of while loops, explore its attributes, its applications, and its relationship to invariant assertions. Also, we discuss the design, implementation and use of a tool that analyzes while loops using this concept.