An Algorithm a Day: Loop invariant to prove correctness

Metaphor

   So, you got the formula directly fetched from Wikipedia!! Did you understand it? :) The funny part this is logical mathematics which doesn’t have a metaphor or beauty to compare with.

  This technique is like theorem proving, where you consider something is true through out. Only if it is true, the theorem is also true. There are many popular theoretical way to prove a theorem,

   - proof by induction

   - proof by contradiction

There are many more theorem proving techniques available. But logical way to prove a computer program is: Hoare logic which is the formula given above

here, I is the loop invariant, C is the condition for loop termination, if you see the formula, I is maintained initial and in body and also in termination.

Concept

   Why do you want to prove correctness of a computer program? An algorithm can always fail!! There are boundary conditions, negative inputs, infinite loops and all such possibilities when you write a code which is never covered in an algorithm. How would you know that an algorithm never gives infinite loop? the simple way is loop invariants.

   In all the algorithms discussed till now, we should have used loop invariant to confirm the correctness of the code. But since this concept is little bit complex, we have covered a separate section for this. This is really important if you want to write a valid unit test for any code.

  How would you find a loop invariant??

Read full article from An Algorithm a Day: Loop invariant to prove correctness