Verifying while loops with invariant relations

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

Research output: Contribution to journalArticlepeer-review

7 Scopus citations

Abstract

Traditionally, invariant assertions are used to verify the partial correctness of while loops with respect to pre/post specifications. In this paper we discuss a related but distinct concept, namely invariant relations, and show how invariant relations are a more potent tool in the analysis of while loops: whereas invariant assertions can only be used to prove partial correctness, invariant relations can be used to prove total correctness; also, whereas invariant assertions can only be used to prove correctness, invariant relations can be used to prove correctness and can also be used to prove incorrectness; finally, where traditional studies of loop termination equate termination with iterating a finite number of times, we broaden the definition of termination to also capture the condition that each individual iteration proceeds without raising an exception.

Original languageEnglish (US)
Pages (from-to)78-102
Number of pages25
JournalInternational Journal of Critical Computer-Based Systems
Volume5
Issue number1-2
DOIs
StatePublished - 2014

All Science Journal Classification (ASJC) codes

  • General Computer Science

Keywords

  • Invariant assertions
  • Invariant functions
  • Invariant relations
  • Necessary condition of termination
  • Necessary conditions of orrectness
  • Sufficient condition of termination
  • Sufficient conditions of correctness
  • While loops

Fingerprint

Dive into the research topics of 'Verifying while loops with invariant relations'. Together they form a unique fingerprint.

Cite this