|
|
|
|
|
|
 |
|
|
A versatile concept for the analysis of loops
|
|
|
|
|
|
|
|
|
|
|
|
| The Journal of Logic and Algebraic Programming |
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
Invariant relation, Invariant assertion, Invariant function, Weakest precondition, Strongest postcondition, While loop, Termination condition, Loop functions, Loop semantics
|
|
|
|
|
|
|
| | | | | |
|
For the newest resources, visit Wolfram Repositories and Archives »
