Title: Verifying while loops with invariant relations

Authors: 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

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: 10.1504/IJCCBS.2014.059596

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

Published online: 21 Oct 2014 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article