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

Details:

   
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
ISSN0747-7171
URL http://www.sciencedirect.com/science/article/pii/S0747717109000510
LanguageEnglish
JournalJournal of Symbolic Computation
Volume45
Number11
Pages1114 - 1143
Year2010
NoteSpecial Issue on Invariant Generation and Advanced Techniques for Reasoning about Loops
Edition0
Translation No
Refereed No
Webmaster