Invariant assertions, invariant relations, and invariant functions

Olfa Mraihi, Asma Louhichi, Lamia Labed Jilani, Jules Desharnais, Ali Mili

Research output: Contribution to journalArticlepeer-review

14 Scopus citations


Invariant assertions play an important role in the analysis and documentation of while loops of imperative programs. Invariant functions and invariant relations are alternative analysis tools that are distinct from invariant assertions but are related to them. In this paper we discuss these three concepts and analyze their relationships. The study of invariant functions and invariant relations is interesting not only because it provides alternative means to analyze loops, but also because it gives us insights into the structure of invariant assertions, hence it may help us enhance techniques for generating invariant assertions.

Original languageEnglish (US)
Pages (from-to)1212-1239
Number of pages28
JournalScience of Computer Programming
Issue number9
StatePublished - Sep 1 2013

All Science Journal Classification (ASJC) codes

  • Software
  • Information Systems
  • Computational Theory and Mathematics
  • Modeling and Simulation


  • Invariant assertions
  • Invariant functions
  • Invariant relations
  • Loop functions
  • Loop invariants
  • Program analysis
  • Program verification
  • While loops

Cite this