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.

Recursive Algorithm Correctness!

Next Milestone After Recurrences arrived was Proving Correctness of Algorithm...

Danny worked Through the Correctness of Binary Search Algorithm in class...
The Pre conditions of Binary Search algorithm were Straight forward, But post conditions were not, Normally Post conditions are supposed to be the desired output from the algorithm But the post conditions of Binary Search made sense on the output but were not obvious to the mind.

By doing examples from course notes The Idea Stick to the mind.
And then we realize that Recursive Algorithm correctness is far more easier, 

Assume the pre conditions Use Induction to prove Correctness leading to post conditions Fairy Simple.

Recurrences

Recurrences:

Next topic came in the course, which includes finding Time Complexity of recursive algorithms.

where we define the exact number of steps for base cases and a recurrence relation in terms of T(n) based on the algorithm for arbitrary values of  n > b, where b is a natural number.

This looked fairly simple until we got into proving upper and lower bounds of Recursive binary search

and merge sort algorithm,   To get the idea of bound for a certain Algorithm we basically unwind the recurrence based on its definition.  Normally Recursive algorithms involve Divide and conquer technique to define a recurrence, where we Split the input in two or more halves. So, then after unwinding the recurrence, we end up getting a closed form our recurrence relation.

That closed form tells us the exact bound for our algorithm.

Then we set out to prove Big O and Big Omega that bound for our recursive Algorithm.

The Proof Of Big Omega for recursive Binary search is straight forward, 

But Big O is difficult if your trying to prove it all by yourselves, it involves one trick which is not obvious and cannot be thought of easily,   Even Great researchers came to know it through trial and error.

So, I looked in to course notes, Theory of computation book, Google searches you tube videos

to understand the Big O notation for recursive binary search

and talk about Big O and Big Omega for merge sort algorithm, which both involve similar kind of trick in opposite direction.