Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.c++ > #8292

Re: what is a loop invariant

Show all headers | View raw

On 27.07.2011 23:22, Jorgen Grahn wrote:
>
> 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

Back to comp.lang.c++ | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

what is a loop invariant johan1990 <81378989@qq.com> - 2011-07-26 06:26 -0700
  Re: what is a loop invariant Victor Bazarov <v.bazarov@comcast.invalid> - 2011-07-26 10:02 -0400
    Re: what is a loop invariant Todd Carnes <toddcarnes@gmail.com> - 2011-07-27 12:29 +0000
      Re: what is a loop invariant Jorgen Grahn <grahn+nntp@snipabacken.se> - 2011-07-27 21:22 +0000
        Re: what is a loop invariant "Alf P. Steinbach" <alf.p.steinbach:usenet@gmail.com> - 2011-07-28 01:42 +0200
          Re: what is a loop invariant Jorgen Grahn <grahn+nntp@snipabacken.se> - 2011-07-28 08:52 +0000
          Re: what is a loop invariant James Kanze <james.kanze@gmail.com> - 2011-07-30 12:12 -0700
            Re: what is a loop invariant "Alf P. Steinbach" <alf.p.steinbach:usenet@gmail.com> - 2011-07-31 02:52 +0200
        Re: what is a loop invariant Robert Wessel <robertwessel2@yahoo.com> - 2011-07-27 22:10 -0500
          Re: what is a loop invariant James Kanze <james.kanze@gmail.com> - 2011-07-30 12:03 -0700
  Re: what is a loop invariant Saeed Amrollahi <amrollahi.saeed@gmail.com> - 2011-07-26 09:04 -0700
  Re: what is a loop invariant "Paul" <pchristor@yahoo.co.uk> - 2011-07-26 22:55 +0100
    Re: what is a loop invariant Juha Nieminen <nospam@thanks.invalid> - 2011-07-27 07:50 +0000
      Re: what is a loop invariant "Paul" <pchristor@yahoo.co.uk> - 2011-07-27 11:11 +0100
        Re: what is a loop invariant Juha Nieminen <nospam@thanks.invalid> - 2011-07-27 13:44 +0000
          Re: what is a loop invariant "Paul" <pchristor@yahoo.co.uk> - 2011-07-27 15:38 +0100
            Re: what is a loop invariant Oliver Jackson <chexmofo@hotmail.com> - 2011-07-27 23:25 -0700
              Re: what is a loop invariant "Paul" <pchristor@yahoo.co.uk> - 2011-07-28 19:45 +0100
    Re: what is a loop invariant Nick Keighley <nick_keighley_nospam@hotmail.com> - 2011-07-27 00:46 -0700
  Re: what is a loop invariant Geoff <geoff@invalid.invalid> - 2011-07-27 21:41 -0700

csiph-web