Partial Correctness And Iterative Algorithms

To prove Correctness of Iterative Algorithms.
The Procedure is :
Assume Preconditions:

Derive and Prove a loop invariant (Partial Correctness)
Prove Termination
In the End Show that: Precondition + Partial Correctness + Termination implies Post-condition.

Loop Invariant is something which is True Before and End of Every loop Iteration.
We normally use induction to Prove Loop Invariant.

Termination: Loop Invariant helps us prove termination also,
To prove termination we need to come up with a sequence  which is decreasing and in the end meets termination condition, Then Use of Principle of Well Ordering to show that This sequence hits the least element of the set and loop breaks.

Based on what Algorithm does, we show that output meets Post - condition.

Danny's Power algorithm example helps a lot to get the idea of proving correctness of iterative Algorithms.