Relational methods in the analysis of while loops: Observations of versatility

Asma Louhichi, Olfa Mraihi, Lamia Labed Jilani, Khaled Bsaies, Ali Mili

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationRelations 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.
Pages242-259
Number of pages18
DOIs
StatePublished - Dec 1 2009
Event11th International Conference on Relational Methods in Computer Science, RelMiCS 2009 and 6th International Conference on Applications of Kleene Algebra, AKA 2009 - Doha, Qatar
Duration: Nov 1 2009Nov 5 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5827 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other11th International Conference on Relational Methods in Computer Science, RelMiCS 2009 and 6th International Conference on Applications of Kleene Algebra, AKA 2009
CountryQatar
CityDoha
Period11/1/0911/5/09

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Keywords

  • Computing loop behavior
  • Function extraction
  • Invariant assertions
  • Invariant functions
  • Invariant relations
  • Loop functions
  • Refinement calculus
  • Relational calculus

Fingerprint Dive into the research topics of 'Relational methods in the analysis of while loops: Observations of versatility'. Together they form a unique fingerprint.

Cite this