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.
Original language | English (US) |
---|---|
Pages (from-to) | 78-102 |
Number of pages | 25 |
Journal | International Journal of Critical Computer-Based Systems |
Volume | 5 |
Issue number | 1-2 |
DOIs | |
State | Published - 2014 |
All Science Journal Classification (ASJC) codes
- General Computer Science
Keywords
- Invariant assertions
- Invariant functions
- Invariant relations
- Necessary condition of termination
- Necessary conditions of orrectness
- Sufficient condition of termination
- Sufficient conditions of correctness
- While loops