Title: Verifying while loops with invariant relations

 

Author: Asma Louhichi; Wided Ghardallou; Khaled Bsaies; Lamia Labed Jilani; Olfa Mraihi; Ali Mili

 

Addresses:
Faculty of Sciences, University of Tunis El Manar, Tunis, 1080, Tunisia
Faculty of Sciences, University of Tunis El Manar, Tunis, 1080, Tunisia
Faculty of Sciences, University of Tunis El Manar, Tunis, 1080, Tunisia
Institut Superieur de Gestion, Bardo 2000, Tunisia
Institut Superieur de Gestion, Bardo 2000, Tunisia
CCS, NJIT, Newark NJ 07102-1982, USA

 

Journal: Int. J. of Critical Computer-Based Systems, 2014 Vol.5, No.1/2, pp.78 - 102

 

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.

 

Keywords: while loops; invariant assertions; invariant relations; invariant functions; sufficient conditions of correctness; necessary conditions of correctness; sufficient condition of termination; necessary condition of termination.

 

DOI: http://dx.doi.org/10.1504/IJCCBS.2014.059596

 

Available online 02 Mar 2014

 

 

Editors Full Text AccessAccess for SubscribersPurchase this articleComment on this article