1

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;
}
Daniel Daranas
  • 22,454
  • 9
  • 63
  • 116
Navid Koochooloo
  • 285
  • 1
  • 5
  • 20
  • Homework? Search this site, there are many explanations on what a loop invariant is. An example: http://stackoverflow.com/questions/3221577/what-is-a-loop-invariant – Armen Michaeli Jun 09 '13 at 09:30
  • This might help you, it was helpful for me too. http://stackoverflow.com/questions/2935295/what-is-the-best-way-of-determining-a-loop-invariant – Roshan Jun 09 '13 at 09:33

3 Answers3

6

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.

Sergey Kalinichenko
  • 714,442
  • 84
  • 1,110
  • 1,523
  • thanks a lot, it's so clear for me now. The expression with a0 is exactly what i wanted. something i don't get is that why we did write a function with "a" and not "b" for example. – Navid Koochooloo Jun 09 '13 at 10:24
  • @NavidKoochooloo There are many ways to write that same invariant by moving parts of the expression to the different sides of `==`. For example, you can write it as `(b*q) == (a0-a)`, but that's the same exact expression. – Sergey Kalinichenko Jun 09 '13 at 10:32
  • it's a bit hard to extract the expression, without looking at your expression, i thought a lot over it but couldn't reach such expression also didn't know I should use "a0" for example :/ anyway thanks :) it was really helpful what u explained – Navid Koochooloo Jun 09 '13 at 10:37
1

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.

Deepu
  • 7,592
  • 4
  • 25
  • 47
0

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

in your case one invariant is:

q >= 0

kishoredbn
  • 2,007
  • 4
  • 28
  • 47