Verifying while loops with invariant relations. (1st January 2014)

• Record Type: Journal Article
• Authors: Louhichi, Asma; Ghardallou, Wided; Bsaies, Khaled; Jilani, Lamia Labed; Mraihi, Olfa; Mili, Ali
• Is Part Of: International journal of critical computer-based systems. Volume 5:Number 1/2(2014)
• Page Start: 78
• Page End: 102
• Publication Date: 2014-01-01
• Subjects: while loops -- invariant assertions -- invariant relations -- invariant functions -- sufficient conditions of correctness -- necessary conditions of correctness -- sufficient condition of termination -- necessary condition of termination; Computer systems -- Periodicals; Computer architecture -- Periodicals; 004
• Languages: English
• ISSNs: 1757-8779

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.