Invariant functions and invariant relations: An alternative to invariant assertions

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

Research output: Contribution to journalArticlepeer-review

6 Scopus citations


Whereas the analysis of loops in imperative programs is, justifiably, dominated by the concept of invariant assertion, we submit a related but different concept, of invariant relation, and show how it can be used to analyze diverse aspects of a while loop. We also introduce the concept of invariant function, which is used to generate a broad class of invariant relations.

Original languageEnglish (US)
Pages (from-to)1-36
Number of pages36
JournalJournal of Symbolic Computation
StatePublished - Jan 2013

All Science Journal Classification (ASJC) codes

  • Algebra and Number Theory
  • Computational Mathematics


  • Invariant assertions
  • Invariant functions
  • Invariant generation
  • Invariant relations
  • Loop functions
  • Reasoning about loops
  • While loops


Dive into the research topics of 'Invariant functions and invariant relations: An alternative to invariant assertions'. Together they form a unique fingerprint.

Cite this