Design Iterative Algorithms

If you are designing describing and proving correct an algorithm using loop invariants, the following is the list the things must consider.

Specification: Define the problem (pre and post conditions): likely defined by the problem.

Define Loop Invariant: It needs to be a picture of what is true every time the algorithm is at the top of the loop. 

Establishing the Loop Invariant:

  <pre-cond> & code_pre-loop => <Loop Invariant>

·      state what you know about the input instance because of <pre-cond>

·      state the effect of the code before the loop

·      State how it then follows that <loop invariant> has been established.

Define steps:  Define the step code_loop that is executed each iteration and is guaranteed to maintain the loop invariant while making progress. though this step, when actually coding, may require a nested loop or other fancy code, here it suffices to give a quick description of what actions take place. 

maintaining the Loop Invariant:

   <loop-invariant^’> & ^~<exit-cond> & code_loop  => <loop-invariant^’’>

·      Imagine that you have just flown in from mars and are at the top of the loop. All you know about the state of the data structure is that the loop invariant is true and the exit condition is not.

·      Let x^’  be the current values of the variables and x^’’ after going around the loop again.

·      State what you know about x^’ from the fact that <loop-invariant^’> holds for these values.

·      The step code_loop constructs the values x^’’ from the values x^’. State what this tells you x^’’.

·      State how it then follows that <loop-invariant^’’> holds for the values x^’’.

Exit: Define the Exit condition.

·      Not post condition: It would be natural to exit when you are done and hence it si natural to make the exit condition be the same as the post condition. But this just passes the problem of will the post condition ever be met onto whether your loop will ever exit.

·      Sufficient Progress:  Instead, define a measure of progress and have your exit conition be that sufficient progress has been made. If it is clear that progress is made each iteration, then it will be obvious that the loop will eventually exit. In this case, you can skip the Termination step.

·      Panic: Another good exit condition is the reason that you can no longer maintain the loop invariant. Note that defining such an exit condition makes it easier to do the previous step of proving that if the exit condition is not true then the step taken maintains the loop invariant.

Obtaining the Postcondition:

  <loop Invariant> & <exit-Cond> & code_post-loop => <post-cond>

·      state what you know because of <loop-invariatn>

·      state what you know because of <exit-cond>

·      state what you know because of code_post-loop

·      state how it then follows that <post-cond.

Termination:

·      Define measure of progress.

·      Initially finite progress required

·      Prove that each iteration you make progress

·      Proof that with sufficient progress, the exit condition will be met.

Running Time: Give an upper bound on the number of times that this algorithm iterates. Also estimate the total running time.