Help with Loop Invariants

[BebopSong]

Hi,

 

I've been reading an algorithm book and after learning and understanding the insertion loop the topic of loop invariants comes up which confuses me somewhat. They appear, to me, to be just statements that the loop will work, i.e. the loop invariant remains true at the beginning of each iteration of the loop and when it terminates. This seems non-sensical to me as that is the entire reason for creating the algorithm in the first place so why do we need to state it?

 

I'm more practical than theoretical which I believe is halting my ability to understand the theory behind it. Can someone explain the use of loop invariants please? Do they help to create algorithms or are they just to prove correctness, in which case what is the process of proving an algorithm before creating it using loop invariants?

 

Thanks.

 

BebopSong

[Xittenn]

If the condition were to change during the loop should it break or continue until the next iteration? What consequence would either of these choices have?

 

If the condition is invariant under the iteration then these choices can be avoided and the consequences as well. It is an abstract concept and not something one would concern themselves with much while creating functional programs.

[khaled]

Loop = Code + Condition

 

a loop will execute the Code, if the Condition returns TRUE,

 

The Condition can be pre-condition like in for and while loops, post-condition like do-while and loop-until loops,

 

or in-condition such as base-case, intelligent-search and decision-problem ...

 

pre-condition:

LOOP ( CONDITION )
    CODE
END-LOOP

 

post-condition:

LOOP
    CODE
UNTIL ( CONDITION )

 

in-condition:

LOOP ( FOREVER )
    CODE
    IF ( BASE-CASE ) THEN BREAK
    CODE
END-LOOP

[BebopSong]

Ah ok, that makes sense now. So loop invariants explain the setup of the loop and the 3 parts of loop invariants; initialization, maintenance and termination explain the individual sections of the loop that must result in true for the loop to be correct.

 

Initialization specifies that the variant meets the required condition to enter the loop. Maintenance states that the variant meets the required condition to stay in the loop for all the necessary times required to complete the task. Termination makes sure the variant will terminate after some time (hopefully a short amount of time).

 

It's useful then to consider these concepts when designing a loop but, in my opinion, subconsciously they are. Still thinking up all scenarios of what will make the loop break is a good idea.

 

Thanks for the help.