## Abstract

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 show how these 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; how to compute a weakest precondition of the loop; how to compute a strongest postcondition of the loop; how to compute the termination condition of a loop; how to verify whether the loop computes a given function; how to verify whether the loop is correct with respect to a given specification; and finally how to 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 (

Original language | English (US) |
---|---|

Pages (from-to) | 606-622 |

Number of pages | 17 |

Journal | Journal of Logic and Algebraic Programming |

Volume | 81 |

Issue number | 5 |

DOIs | |

State | Published - Jul 2012 |

## All Science Journal Classification (ASJC) codes

- Software
- Theoretical Computer Science
- Logic
- Computational Theory and Mathematics

## Keywords

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