Details:
Title  Reflexive 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  Type  Article in Journal  Abstract  Invariant 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.  Keywords  Function extraction, Loop functions, Invariant assertions, Invariant relations, Invariant functions, Relational calculus, Refinement calculus, Computing loop behavior  ISSN  07477171 
URL 
http://www.sciencedirect.com/science/article/pii/S0747717109000510 
Language  English  Journal  Journal of Symbolic Computation  Volume  45  Number  11  Pages  1114  1143  Year  2010  Note  Special Issue on Invariant Generation and Advanced Techniques for Reasoning about Loops  Edition  0  Translation 
No  Refereed 
No 
