Invariant Relations: An Automated Tool to Analyze Loops
Asma Louhichi, Olfa Mraihi, Wided Ghardallou, Lamia Labed Jilani, Khaled Bsaïes, Ali Mili · Electronic workshops in computing · 2011
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.