Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitleReflexive transitive invariant relations: A basis for computing loop functions
Author(s) Lamia Labed Jilani, Asma Louhichi, Ali Mili, Olfa Mraihi, Chaitanya Nadkarni, A.I. Shirshov
TypeArticle in Journal
AbstractInvariant assertions play an important role in the analysis and verification of iterative programs. In this paper, we introduce a related but distinct concept, namely that of invariant relation. While invariant assertions are useful to prove the correctness of a loop with respect to a specification (represented by a precondition/ postcondition pair) in Hoare’s logic, invariant relations are useful to derive the function of the loop in Mills’ logic.
KeywordsFunction extraction, Loop functions, Invariant assertions, Invariant relations, Invariant functions, Relational calculus, Refinement calculus, Computing loop behavior
URL http://www.sciencedirect.com/science/article/pii/S0747717109000510
JournalJournal of Symbolic Computation
Pages1114 - 1143
NoteSpecial Issue on Invariant Generation and Advanced Techniques for Reasoning about Loops
Translation No
Refereed No