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
Y1 - 2009
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 -