what is a loop invariant

[johan1990]

i am reading introduction to algorithms and i have no idea of what the
concept "loop invariant" means. i really appreciate it if there is a
easy way to explain it. :~)

 

[Victor Bazarov]

i am reading introduction to algorithms and i have no idea of what the
concept "loop invariant" means. i really appreciate it if there is a
easy way to explain it. :~)

Uh... http://en.wikipedia.org/wiki/Loop_invariant isn't easy? Try it.
Also, consider 'comp.programming' for general questions like that.

V

 

[Saeed Amrollahi]

i am reading introduction to algorithms and i have no idea of what the
concept "loop invariant" means. i really appreciate it if there is a
easy way to explain it.  :~)

Hi
From Accelerated C++ by Andrew Koenig & Barbara Moo, page 20:
... loop invariant is a property that we assert will be true about
a loop [like while or for loop] each time it is about to test
its condition.

for example:
int i = 0;
// invariant: we have said "hello" i times so far
while (i < 10) {
std::cout << "Hello, world!\n";
// we just said "hello" one more time and
// the invariant is false now
++i;
// increment i and now invariant is true again
}
// invariant is true, because at this point
// we have said "hello" 10 times

As Victor mentioned the loop invariant is a general
programming concept and it's not limited to C++.

Regards,
-- Saeed Amrollahi

 

[Nick Keighley]

Dunno what is a varaint and and invariant?
Sounds like a varaible and a ?? maybe I am on the wroing track

yes

 

[Juha Nieminen]

Dunno what is a varaint and and invariant?
Sounds like a varaible and a ?? maybe I am on the wroing track

If you don't know, why do you answer?

 

[Todd Carnes]

Uh... http://en.wikipedia.org/wiki/Loop_invariant isn't easy? Try it.
Also, consider 'comp.programming' for general questions like that.

V

Actually, the Wikipedia article is NOT written very well. For example,
the very first sentence reads... "In computer science, a loop invariant
is an invariant used to prove properties of loops." When one is defining
something for someone, one should NEVER use the same word they are
explaining in the explanation. (in this case "invariant").

Also, the rest of the explanation expects the reader to be fairly well
versed in computer science & logic, which one cannot assume from the OP's
question.

Todd

 

[Juha Nieminen]

Because its a discussion group not just Q and A's.

If someone asks a question, he is expecting people who know the answer
to tell him. He does not expect people who have no idea to start guessing.
It was not a quiz to see who wins the prize for giving the correct answer.

If you don't know, but are interested in the answer yourself, the proper
reply is "I'm interested in knowing the answer to this question too".

 

[Jorgen Grahn]

Actually, the Wikipedia article is NOT written very well.

It reads like many other CS-related article: as if it's written by a
student who just came back from a lecture explaining loop invariants,
but who hasn't really digested it yet.

For example,
the very first sentence reads... "In computer science, a loop invariant
is an invariant used to prove properties of loops." When one is defining
something for someone, one should NEVER use the same word they are
explaining in the explanation. (in this case "invariant").

Also, the rest of the explanation expects the reader to be fairly well
versed in computer science & logic, which one cannot assume from the OP's
question.

This part of the intro doesn't ring true, either:

Informally, a loop invariant is a statement of the conditions that
should be true on entry into a loop and that are guaranteed to
remain true on every iteration of the loop. This means that on exit
from the loop both the loop invariant and the loop termination
condition can be guaranteed.

Maybe I have forgotten too much of what I once learned, but in this code

// A
while(expr) {
// B
}
// C

I understand a loop invariant to be something which I assert is always
true during all of B -- but not necessarily at C!

To the original poster: ask your lecturer. It's a course on algorithms
-- that's what (s)he's there for!

/Jorgen

 

[Alf P. Steinbach]

Maybe I have forgotten too much of what I once learned, but in this code

// A
while(expr) {
// B
}
// C

I understand a loop invariant to be something which I assert is always
true during all of B -- but not necessarily at C!

No, that would be of little practical value.

The point of the loop INVARIANT is that it's true before the loop, and
after each iteration, so that it's guaranteed to be true after the loop.

The word "invariant" simply means unchanging, that it keeps on having
the same (boolean) value, namely the value true. We say that it HOLDS
when it's true, and that it doesn't hold or is BROKEN when it's false.
As with a class invariant it can and usually must be broken by the code
that does things, because things can't practically be done with that
invariant being true all the time. So the code must very carefully break
the invariant and then RE-ESTABLISH the invariant, every iteration.

It's the main thing that guarantees that IF the loop terminates, then
one knows that the loop invariant is true.

For example, to compute the integer power x^n (x raised to the n'th
power), one might choose an invariant like

pow = x^i

where i is a loop variable.

Then one might write

i = 0; pow = 1; // pow = x^i
while( i != n )
{
pow *= x; ++i; // pow = x^i
}
cout << pow << endl; // pow = x^i && i = n


One still doesn't know that the loop will terminate, however.

Maybe it will just go on forever?

So that part of proving a loop correct, relies on another value called
the loop VARIANT, where "variant" means "changing". It's an integer that
on every iteration gets closer to some value X (mathematicians prefer to
say that it decreases, and choose X = 0). And then you simply choose as
your loop continuation condition that the variant is not X.

Since the variant is an integer, it will reach X at some point.

In the example above, the variant is the variable i plus the fact that
it increases every loop iteration plus the ceiling value n.

A mathematician or computer scientist, being bound by the necessity of
conforming, will instead say that the variant is the expression n-i (or
any expression that behaves roughly the same way, like 2*(n-i)), where
it's implicit that it decreases every iteration, and that the floor
value is 0. With the implicit stuff it's simpler to communicate the
variant, but it's more difficult to reason about it. So that's their
choice, ease of communication rather than ease of reasoning.

I think the best treatment I have read about loop invariants and
variants was by Niklaus Wirth in an article in Scientific American.

He demonstrated how an algorithm expressed as a loop could be optimized
by changing it in ways that preserved the invariant and variant. This
resulted in a new and mucho faster algorithm. As I recall his article
involved the text search idea of skipping ahead a maximum number of
characters, with those maximum skips precomputed before the search.

Cheers & hth.,

- Alf

 

[Geoff]

i am reading introduction to algorithms and i have no idea of what the
concept "loop invariant" means. i really appreciate it if there is a
easy way to explain it. :~)

A loop invariant is any statement, variable or expression that does
not depend on the actions of the loop or any control variable of the
loop.

 

[Oliver Jackson]

This is not always the case, sometimes one asks a question as a starter for
discussion and debate


This would not make a very interesting disucssion, how would someone reply
to such a post? With something like ..." oh ok, thanks for letting us know"
or something along these lines?

Here is your post, verbatim:

Dunno what is a varaint and and invariant?
Sounds like a varaible and a ?? maybe I am on the wroing track

It hasn't happened yet, but I anticipate your post to lead to some of
the most interesting discussion this forum has seen in recent years.

 

[Jorgen Grahn]

No, that would be of little practical value.

The point of the loop INVARIANT is that it's true before the loop, and
after each iteration, so that it's guaranteed to be true after the loop.

[long explanation]

....

I think the best treatment I have read about loop invariants and
variants was by Niklaus Wirth in an article in Scientific American.

And your explanation also seems to match what Bertrand Meyer writes
about in his book (Object-oriented something). I was going to refer to
it, but it was late last night and I didn't understand it. (The
examples in Eiffel didn't help either.)

So clearly I /have/ forgotten what I once learned. I reason informally
about the correctness of loops, but not like that.

/Jorgen

 

[James Kanze]

On 27 Jul 2011 21:22:32 GMT, Jorgen Grahn <[email protected]>
wrote:
[...]
I think the OP may be more interested in:

http://en.wikipedia.org/wiki/Loop-invariant_code_motion

rather than the other article,

Why? Given the question, I doubt that he's writing an optimizer
for a compiler, and the article you cite handles compiler
optimization techniques.

which is about formally proving
properties of loops.

Which is something just about every programmer is concerned
with.`

 

[James Kanze]

No, that would be of little practical value.

Yes and no. (But I can't see how anything could be guaranteed
true at the end of B, but not be true at the start of C. Unless
the loop control expression had side effects, in which case, all
bets about anything are off.)

[...]

It's the main thing that guarantees that IF the loop terminates, then
one knows that the loop invariant is true.

And that you don't have any anomolous cases in between.

For example, to compute the integer power x^n (x raised to the n'th
power), one might choose an invariant like

pow = x^i

where i is a loop variable.

Then one might write

i = 0; pow = 1; // pow = x^i
while( i != n )
{
pow *= x; ++i; // pow = x^i
}
cout << pow << endl; // pow = x^i && i = n

There's another important loop invariant here that you've
forgotten: i < n. Except that your code is incorrect, because
if n is negative, it doesn't work. One way of handling this is
with an assert(n >= 0) at the top. Or simply by specifying that
the function has undefined behavior if n < 0. Another, perhaps more
robust, is to use i < n as the condition. Generally, the
condition in a while is an explicit part of the loop invariant.

 

[Alf P. Steinbach]

No, that would be of little practical value.

Yes and no. (But I can't see how anything could be guaranteed
true at the end of B, but not be true at the start of C. Unless
the loop control expression had side effects, in which case, all
bets about anything are off.)

[...]

It's the main thing that guarantees that IF the loop terminates, then
one knows that the loop invariant is true.

And that you don't have any anomolous cases in between.

For example, to compute the integer power x^n (x raised to the n'th
power), one might choose an invariant like

pow = x^i

where i is a loop variable.

Then one might write

i = 0; pow = 1; // pow = x^i
while( i != n )
{
pow *= x; ++i; // pow = x^i
}
cout<< pow<< endl; // pow = x^i&& i = n

There's another important loop invariant here that you've
forgotten: i< n.

That's not a loop invariant.

The main reason why you can't include that in the loop invariant is that
it would be disastrous if that was true after the loop.

You want i=n after the loop, which can't happen if i<n is guaranteed.

Except that your code is incorrect,

Nope, it's correct.

because if n is negative, it doesn't work.

As stated, the code computes an *integer power*. n >= 0 is a
precondition for integer power. This precondition is simple to check.

There is also a precondition that x^n >=
std::numeric_limits<TheIntegerType>::max(), i.e. no overflow.

That latter precondition is an example that design level conditions can
not always be easily or efficiently expressed in the code. ;-)

One way of handling this is
with an assert(n>= 0) at the top. Or simply by specifying that
the function has undefined behavior if n< 0.

Yes, that's one reasonable way to handle preconditions, which is a
different discussion/thread.

Another, perhaps more
robust, is to use i< n as the condition. Generally, the
condition in a while is an explicit part of the loop invariant.

Using i<n as continuation condition for the loop is a practical
solution, but isn't that good in a basic example of loop invariants.

That's because all that it tells you on its own is that after the loop
i>=n, and hence, all that it tells you on its own about the computed
value is that the computed value x^i is greater or equal to the desired
x^n...

So I chose the i!=n condition very carefully -- and now you found out
why. TOGETHER with the invariant, it guarantees the desired result.
Namely, i==n && pow=x^i implies pow=x^n, the desired result.


Cheers & hth.,

- Alf