An iterative algorithm takes one step at a time, ensuring that each step makes progress while maitining the loop invariant.
A paradigm shift:
View an algorithm as a sequence of Actions vs. a sequence of Snapshots/Assertions
Understanding iterative algorithms requires understanding the difference between a loop invariant, which is an assertion or picture of the computation at a particular point in time, and the actions that are required to maintain such a loop invariant.
Pre- and Postconditions:
Pre- and Postconditions provide the initial picture/assertion about the input instance and a corresponding picture/assertion about the required output.
Start in the Middle:
Jump into the middle of the computation and draw a static picture/assertion about the state we would like the computation to be in at the time.
If this assertion is sufficiently genearl, it will capture not just this one point during the computation, but many similar points. Then it might become a part of a loop.
Sequence of Snapshots:
Once we build up a sequence of pictures/assertions in this way, we can see the entire path of the computation laid out before us.
Fill in the actions:
These pictures/assertions are just static snapshots of the computation. No actions have been considered yet. The final step is to fill in the actions (code) between consecutive assertions.
One step at a time:
Each such block of actions can be executed completely independenly of the others. In fact, one can complete these block in any order one wants and modify one block without worrying about the effect on others.
Being in a state in which the ith assertion holds, your task is simply to write some simple code to do a few simple actions that change the state of the computation so that the i+1st assertion holds.
Proof of correctness of each step:
<ith-assertion> & code i => <i+1st-assertion>
Proof of correctness of the algorithm:
Precondition & code => assertion 1
assertion 1 & code 1 => assertion 2
assertion 2 & code2 => assertion 3
...
assertion n-1 & code n-1 => assertion n
assertion n & code n => post condition
Precondition
code
assert 1
code
assert 2
code
assert 3
...
code
assert n
code
Postcondition