how to find loop invariant java

Question

I'm trying to find the invariant of the loops (for example in the following code) I really don't know how to find an invariant in general. can anyone help me with how to find an invariant and also help me to find it for the following code? thanks

public static int div(int a, int b)
{
   int q = 0;
   while(a >= b)
   {
      a -= b;
      q++;
   }

   return q;
}

Answer 1

First thing to note about loop invariants is that there are many of them. Some of them are more useful, while some are less useful. Since invariants are used in proving correctness of programs, choosing an invariant depends on what you are trying to prove.

For example, q >= 0 is an invariant of the loop. If you want to prove that the function returns a positive number, this is all you need. If you want to prove something more complex, you need a different invariant.

Since parameters in Java are passed by value, and because the program modifies values of the parameter a, let's use a0 to denote the initial values of the a parameter. Now you can write the following invariant expression:

a == a0 - (b * q)

You come up with this invariant by observing that each time that q is increased, a is also decreased by b. So a0 is decreased by b exactly q times on each iteration of the loop.

This invariant can be used to prove that the loop produces q == a0 / b, and that the ending value of a is equal to a0 % b.

Answer 2

A loop invariant is some condition that holds true for every iteration of the loop.

In your loop the predicate q >= 0 is a loop invariant, because it's true always. The need for analyzing loop invariants is that when you exit from the loop both the loop invariant and the loop termination condition can be guaranteed. So in your case upon exit from the loop we can be sure that q >= 0 and a < b.

Answer 3

A loop invariant is some condition that holds true for every iteration of the loop.

in your case one invariant is:

q >= 0