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

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

Re: what is a loop invariant

Show all headers | View raw

On 30.07.2011 21:12, James Kanze wrote:
> On Jul 28, 12:42 am, "Alf P. Steinbach"
> <alf.p.steinbach:use...@gmail.com>  wrote:
>> 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.
>
> 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

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