How to choose and set the correct loop invariant?

Question

Hi,

I've been given the following problem about loop invariants:

Consider

x=4; for(i=5;i<k;i++) { a=a+x+i; x=x*2; }

Define the appropiate loop invariant that utilizes a closed formula for a and x.

Now, How do you know you have the right loop invariant here? I mean you can set the loop invariant to be: "At j'th iteration 'x' is less than 'a'" which will be correct but will not use any closed formulas right?

How can a statement (the loop invariant) can be used to determine the value of "a" when the loop is over? All the examples I've seen just state the loop invariant and its not being used as a closed formula.

Any ideas?

Thanks for all of your help.

Answer 1

Start with the closed formulas: clearly for x(j) [for j from 0 to k-5], x at entry to the j-th leg of the loop, x(j+1) = x(j) * 2, so, x(j) is 4 * 2**j (using ** for "raise to power") since x(0) is 4; and a(j+1) = a(j) + x(j) + j + 5 -- we're not told what a(0) is, but we can factor it out and write a(j) as a(0) + something. Can you figure out what that something is, given the above closed-formula resoution for x(j)? I'm reluctant to do your homework from you -- have you yet started studying Concrete Mathematics or whatever your textbook IS...?

Once you're written down the closed-form formula for a(j), to go with the trivial one I supplied for x(j), can you see how they combine to make a loop invariant...?