Invariant relations, invariant functions, and loop functions

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

Research output: Contribution to journalArticlepeer-review

5 Scopus citations


The increasing criticality of software applications, the increasing size and complexity of such applications, and the increasing reliance of software engineering paradigms on third party software assets combine to place a high premium on the ability to analyze software products to an arbitrary level of thoroughness and precision. Yet despite several decades of research, the goal of analyzing the functional properties of software products to an arbitrary level of thoroughness and precision remains unfulfilled. In this paper, we discuss the use of a relation-theoretic approach inspired from Mills' logic to analyze while loops, and we support our approach by an operational prototype tool. The proposed method and tool have applications in program comprehension, reverse engineering, program verification, software maintenance, and programmer education.

Original languageEnglish (US)
Pages (from-to)195-212
Number of pages18
JournalInnovations in Systems and Software Engineering
Issue number3
StatePublished - Sep 2012

All Science Journal Classification (ASJC) codes

  • Software


  • Program analysis
  • Program function
  • Program semantics
  • Refinement calculus
  • Reverse modeling
  • While loop


Dive into the research topics of 'Invariant relations, invariant functions, and loop functions'. Together they form a unique fingerprint.

Cite this