A versatile concept for the analysis of loops

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

Research output: Contribution to journalArticlepeer-review

5 Scopus citations

Abstract

Ever since their introduction by Hoare in 1969, invariant assertions have, justifiably, played a key role in the analysis of while loops. In this paper, we discuss a distinct but related concept, viz invariant relations, and show how these can be used to answer many questions pertaining to the analysis of loops, including: how to compute the function of the loop; how to compute an invariant assertion of the loop; how to compute a weakest precondition of the loop; how to compute a strongest postcondition of the loop; how to compute the termination condition of a loop; how to verify whether the loop computes a given function; how to verify whether the loop is correct with respect to a given specification; and finally how to compute an invariant function for the loop. Using a tool we have developed at the University of Tunis to derive invariant relations, we show how all these tasks can be automated by means of a computer algebra system, viz Mathematica (

Original languageEnglish (US)
Pages (from-to)606-622
Number of pages17
JournalJournal of Logic and Algebraic Programming
Volume81
Issue number5
DOIs
StatePublished - Jul 2012

All Science Journal Classification (ASJC) codes

  • Software
  • Theoretical Computer Science
  • Logic
  • Computational Theory and Mathematics

Keywords

  • Invariant assertion
  • Invariant function
  • Invariant relation
  • Loop functions
  • Loop semantics
  • Strongest postcondition
  • Termination condition
  • Weakest precondition
  • While loop

Fingerprint

Dive into the research topics of 'A versatile concept for the analysis of loops'. Together they form a unique fingerprint.

Cite this