How to find a loop invariant

Question

I know that the loop invariant is meant to prove the correctness of a problem but i can't quite understand how to come up with one, no matter how trivial the problem is. Here is an example, Can someone point out what are the step i should consider to come up with one. I know that all values that are changing in the loop must be involve in my invariant. Please guide me with this problem, i also have to find the post-condition. An explanation will worth more than an answer; please help.

{M > 0 and N >= 0 }

a = M;
b = N;
k = 1;

while (b > 0) {
    if (b % 2 == 0) {
        a = a * a;
        b = b / 2
    } else {
        b = b – 1;
        k = k * a;
    }
}

{ ? ? }

[Me too faced this same kind of question and Hope this explanation would give you the idea](http://stackoverflow.com/questions/2935295/what-is-the-best-way-of-determining-a-loop-invariant) — Rajpirathap Sakthithasan, Oct 19 '15 at 17:10

score 1 · Answer 1 · answered Oct 25 '15 at 20:18

The tricky part about loop invariants is that there is no algorithm (that I'm aware of) that will always guarantee the "correct" answer.

As a start, for the algorithm in your question, try tracing through the program and figure out the goal of the algorithm (Hint: exponents are fun). While tracing keep track of the variables a, b and k.

For example, use M = 2 and N = 1,2,3,.... After a few values of N you'll notice a relationship will start to develop between the variables a, b and k.

Once you figure out the loop invariant the post-condition should be simple to come up with.

Hope this will get the ball rolling for you!

score 0 · Answer 2 · answered Oct 25 '15 at 21:05

Well, you're going at this a bit backward. As you said, the purpose of the loop invariant is to help you prove the correctness of the program. I guess you didn't write this program -- otherwise you'd know what it was for, and you would have come up with the loop invariant before you wrote the loop, because it's the key to understanding that the loop is correct.

So... what is the program for? How do you know it's correct? The loop invariant will be part of your answer to the second question.

It will sound something like this: At the start and end of every iteration, k=...b.... . After the loop, b==0, so ...., and the program is therefore correct.

I don't want to spell the answer out, because it's probably homework and you'll only learn it if you figure it out yourself.

How to find a loop invariant

2 Answers2