what is a loop invariant

Discussion in 'C++' started by johan1990, Jul 26, 2011.

  1. johan1990

    johan1990 Guest

    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. :~)
     
    johan1990, Jul 26, 2011
    #1
    1. Advertising

  2. On 7/26/2011 9:26 AM, johan1990 wrote:
    > 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
    --
    I do not respond to top-posted replies, please don't ask
     
    Victor Bazarov, Jul 26, 2011
    #2
    1. Advertising

  3. On Jul 26, 4:26 pm, johan1990 <> wrote:
    > 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
     
    Saeed Amrollahi, Jul 26, 2011
    #3
  4. On Jul 26, 10:55 pm, "Paul" <> wrote:
    > "johan1990" <> wrote in message
    >
    > news:...
    >
    > >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.  :~)

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


    yes
     
    Nick Keighley, Jul 27, 2011
    #4
  5. Paul <> wrote:
    >
    > "johan1990" <> wrote in message
    > news:...
    >>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. :~)

    >
    > 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?
     
    Juha Nieminen, Jul 27, 2011
    #5
  6. johan1990

    Todd Carnes Guest

    On Tue, 26 Jul 2011 10:02:50 -0400, Victor Bazarov wrote:

    > On 7/26/2011 9:26 AM, johan1990 wrote:
    >> 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


    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
     
    Todd Carnes, Jul 27, 2011
    #6
  7. Paul <> wrote:
    >> If you don't know, why do you answer?

    >
    > 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".
     
    Juha Nieminen, Jul 27, 2011
    #7
  8. johan1990

    Jorgen Grahn Guest

    On Wed, 2011-07-27, Todd Carnes wrote:
    > On Tue, 26 Jul 2011 10:02:50 -0400, Victor Bazarov wrote:
    >
    >> On 7/26/2011 9:26 AM, johan1990 wrote:
    >>> 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

    >
    > 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

    --
    // Jorgen Grahn <grahn@ Oo o. . .
    \X/ snipabacken.se> O o .
     
    Jorgen Grahn, Jul 27, 2011
    #8
  9. 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
     
    Alf P. Steinbach, Jul 28, 2011
    #9
  10. johan1990

    Geoff Guest

    On Tue, 26 Jul 2011 06:26:49 -0700 (PDT), johan1990 <>
    wrote:

    >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.
     
    Geoff, Jul 28, 2011
    #10
  11. On Jul 27, 7:38 am, "Paul" <> wrote:
    > "Juha Nieminen" <> wrote in message
    >
    > news:4e301654$0$2852$...> Paul <> wrote:
    > >>>  If you don't know, why do you answer?

    >
    > >> 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.

    >
    > This is not always the case, sometimes one asks a question as a starter for
    > discussion and debate
    >
    > >  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".

    >
    > 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.
     
    Oliver Jackson, Jul 28, 2011
    #11
  12. johan1990

    Jorgen Grahn Guest

    On Wed, 2011-07-27, Alf P. Steinbach 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.
    >
    > 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

    --
    // Jorgen Grahn <grahn@ Oo o. . .
    \X/ snipabacken.se> O o .
     
    Jorgen Grahn, Jul 28, 2011
    #12
  13. johan1990

    James Kanze Guest

    On Jul 28, 4:10 am, Robert Wessel <> wrote:
    > On 27 Jul 2011 21:22:32 GMT, Jorgen Grahn <>
    > 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
     
    James Kanze, Jul 30, 2011
    #13
  14. johan1990

    James Kanze Guest

    On Jul 28, 12:42 am, "Alf P. Steinbach"
    <alf.p.steinbach:> 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. 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.

    --
    James Kanze
     
    James Kanze, Jul 30, 2011
    #14
  15. On 30.07.2011 21:12, James Kanze wrote:
    > On Jul 28, 12:42 am, "Alf P. Steinbach"
    > <alf.p.steinbach:> 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
     
    Alf P. Steinbach, Jul 31, 2011
    #15
    1. Advertising

Want to reply to this thread or ask your own question?

It takes just 2 minutes to sign up (and it's free!). Just click the sign up button to choose a username and then you can ask your own questions on the forum.
Similar Threads
  1. DaKoadMunky

    Handling class invariant violations

    DaKoadMunky, Dec 4, 2004, in forum: C++
    Replies:
    8
    Views:
    1,478
    Victor Bazarov
    Dec 5, 2004
  2. Giovanni Bajo

    min/max: "stable" invariant?

    Giovanni Bajo, Mar 11, 2008, in forum: Python
    Replies:
    1
    Views:
    255
    Terry Reedy
    Mar 11, 2008
  3. Jonathan Lee
    Replies:
    3
    Views:
    511
    James Kanze
    Jul 31, 2010
  4. James Kanze
    Replies:
    0
    Views:
    454
    James Kanze
    Jul 30, 2010
  5. Isaac Won
    Replies:
    9
    Views:
    397
    Ulrich Eckhardt
    Mar 4, 2013
Loading...

Share This Page