TY - GEN

T1 - Relational methods in the analysis of while loops

T2 - 11th International Conference on Relational Methods in Computer Science, RelMiCS 2009 and 6th International Conference on Applications of Kleene Algebra, AKA 2009

AU - Louhichi, Asma

AU - Mraihi, Olfa

AU - Jilani, Lamia Labed

AU - Bsaies, Khaled

AU - Mili, Ali

PY - 2009/12/1

Y1 - 2009/12/1

N2 - Despite much progress in the design of programming languages, the vast majority of software being written and deployed nowadays remains written in languages where iteration is the main inductive construct, and the main source of algorithmic complexity. For the past four decades, the analysis of iterative constructs has been dominated, not undeservedly, by the concept of invariant assertions. In this paper we submit relation-based alternatives, namely invariant relations and invariant functions, and show how these can provide complementary perspectives, and can enrich the analysis of iterations. Whereas loop invariants can be used to establish the correctness of iterative programs in Hoare logics, invariant relations and invariant functions are used to derive program functions in Mills' logic. In keeping with the conference format, we do not delve too much into theoretical results, and focus instead on the applied aspects of our relation-theoretic approach.

AB - Despite much progress in the design of programming languages, the vast majority of software being written and deployed nowadays remains written in languages where iteration is the main inductive construct, and the main source of algorithmic complexity. For the past four decades, the analysis of iterative constructs has been dominated, not undeservedly, by the concept of invariant assertions. In this paper we submit relation-based alternatives, namely invariant relations and invariant functions, and show how these can provide complementary perspectives, and can enrich the analysis of iterations. Whereas loop invariants can be used to establish the correctness of iterative programs in Hoare logics, invariant relations and invariant functions are used to derive program functions in Mills' logic. In keeping with the conference format, we do not delve too much into theoretical results, and focus instead on the applied aspects of our relation-theoretic approach.

KW - Computing loop behavior

KW - Function extraction

KW - Invariant assertions

KW - Invariant functions

KW - Invariant relations

KW - Loop functions

KW - Refinement calculus

KW - Relational calculus

UR - http://www.scopus.com/inward/record.url?scp=70549113667&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=70549113667&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-04639-1_17

DO - 10.1007/978-3-642-04639-1_17

M3 - Conference contribution

AN - SCOPUS:70549113667

SN - 364204638X

SN - 9783642046384

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 242

EP - 259

BT - Relations and Kleene Algebra in Computer Science - 11th Int. Conference on Relational Methods in Computer Science, RelMiCS 2009 and 6th Int. Conference on Applications of Kleene Algebra, AKA 2009, Proc.

Y2 - 1 November 2009 through 5 November 2009

ER -