Iterative Algorithm

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

Iterative Algorithm,布布扣,bubuko.com