As far as i understand all loops have a loop invariants. My understanding is that loop invariant is an argument that is true at the beginning of the loop block as well as at the end of the loop. For example:
while(P) {
//predicate is true here
body of the loop
//predicate still true here
}
But let`s say i have the following loop (the code is in Java):
while(stack.size() > 0 && stack.peek() < 0) {
stack.pop();
}
What i am trying to do here is to pop all negative numbers from the top of the stack - so at the end of the loop at the beginning of the stack will be a positive number or we have an empty stack. It is not clear from this loop what its invariant? What technic we can use to get loop invariant. In general, i would like to use loop invariants for validation of program correctness.
stack.size()
does destroy the stack in some cases. My guess is that the while condition, if evaluated lazily, might be exactly to guarantee that "there is a stack". For example, thatstack.peek()
doesn't get called ifstack.size()
is zero. Upon termination you can guarantee that "there is a stack" and the negation of thewhile
condition. Namely, there is a stack and it is either empty or the top element doesn't satisfy ${}<0$. $\endgroup$stack.size() > 0 && stack.peek() < 0
is not equivalent tostack.size() <= 0 || stack.peek() >= 0
. $\endgroup$