Wolfram Library Archive

Courseware Demos MathSource Technical Notes
All Collections Articles Books Conference Proceedings

A versatile concept for the analysis of loops

Wided Ghardallou
Olfa Mraihi
Asma Louhichi
Lamia Labed Jilani
Khaled Bsaies
Ali Mili
Journal / Anthology

The Journal of Logic and Algebraic Programming
Year: 2012
Volume: 81
Page range: 606-622

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 showhowthese 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; howto compute aweakest precondition of the loop; howtocompute a strongest postcondition of the loop; howtocompute the termination condition of a loop; howto verify whether the loop computes a given function; howto verify whether the loop is correctwith respect to a given specification; and finally howto 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 (©Wolfram Research). Whenever applicable, we compare the performance of our tool against the performance of others.

*Applied Mathematics > Computer Science
*Mathematics > Algebra

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