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) {

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.

  • $\begingroup$ "There is a stack" remains true. Add to or replace this with any property that the methods called don't change. I don't know Java well. Maybe 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, that stack.peek() doesn't get called if stack.size() is zero. Upon termination you can guarantee that "there is a stack" and the negation of the while condition. Namely, there is a stack and it is either empty or the top element doesn't satisfy ${}<0$. $\endgroup$
    – plop
    Commented Oct 1, 2020 at 17:07
  • 1
    $\begingroup$ Do you need a loop invariant for this one? Remember that the postcondition also includes the inverse of the condition. So in the postcondition we know that stack.size() <= 0 || stack.peek() >= 0 $\endgroup$ Commented Oct 1, 2020 at 17:27
  • 1
    $\begingroup$ A loop invariant is usually something that is useful for proving the postcondition you need, not just any old thing that is true. $\endgroup$ Commented Oct 1, 2020 at 17:45
  • $\begingroup$ @user253751 Any "old thing that is true" and remains true is part of the loop invariant, by definition. Together with the negation of the loop condition it can be asserted once the loop finishes. $\endgroup$
    – plop
    Commented Oct 1, 2020 at 17:46
  • $\begingroup$ @user253751 Also, the negation of stack.size() > 0 && stack.peek() < 0 is not equivalent to stack.size() <= 0 || stack.peek() >= 0. $\endgroup$
    – plop
    Commented Oct 1, 2020 at 18:11

1 Answer 1

    Pre: stack is empty or contains only integers
    Post: Stack top is non-negative Integer
    P:  Stack top is an Integer   ( P is the invariant )
    BB: Stack top is negative
    T:  Stack size

" Establish P "
stack size > 0 or: [stack push: 0].
[ stack top negative
] whileTrue:
    [ " reduce T "
      stack pop. 
      " restore P "
      stack size > 0 or: [stack push: 0]
" P && non BB => Post "
  • $\begingroup$ Now you've changed the algorithm though. $\endgroup$ Commented Oct 2, 2020 at 9:11
  • $\begingroup$ Sure--but if empty stack case is important, there is an easy fix. Change the first line to (ok := stack size > 0) $\endgroup$
    – Jim Sawyer
    Commented Oct 4, 2020 at 2:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.