Cyclic invariant - prove the correctness of the algorithm theoretically

I was reading Introduction to Algorithms recently and in the second chapter I saw a very interesting concept — Loop Invariant. In short, the purpose of a cyclic invariant is to prove theoretically that an algorithm is correct.

So, how do you theoretically prove that an algorithm is correct?

I honestly hadn’t thought about it before. When I debug code, I always try various inputs and look at the corresponding outputs to make sure the program is correct. It’s not that this is wrong, it’s that this habit keeps me from thinking about proving the algorithm right in theory. Blindly trying a few more inputs would be as inelegant as asking a computer to prove goldbach’s conjecture using arithmetic. You can prove that very large numbers satisfy goldbach’s conjecture, but you can never say that Goldbach’s conjecture is correct.

Proving an algorithm is surprisingly simple in theory, the process is similar to mathematical induction. So let’s see what induction looks like.

There are two steps in mathematical induction

Lay cardinality: generally verify that n takes the smallest term is true
Derivation: hypothesisIt can be proved by derivationIs also true.

Let’s take an example

How to verify the arithmetic summation formula?

Verify the formula inWhen set up. That is on the leftThe right =So this formula is inWhen set up.

You need to prove your hypothesisWhen the formula is true, then it can be derivedThe formula is also true. The steps are as follows:

Assuming thatWhen the formula holds, i.e(Equation 1)

And then we can add this to both sides of the equationgetSo this is equal to 2The equation of phi. The next step is to prove that equation 2 is true based on equation 1. By factoring and combining, the right-hand side of equation 2That is

So we’re doneCome into beingThe establishment of the process, proven.

Conclusion: The formula is valid for any natural number n.

So let’s prove the algorithm by proving the cyclic invariant in the same way that we proved the formula by induction.

Let’s take the example of insertion sort (ascending, represented here in pseudocode, with the subscript of an array being) :

INSERTION-SORT(A)
  for j = 2 to A.length
    key = A[j]
    i = j-1
    while i>0 and A[i] > key
      A[i+1] = A[i]
      i = i-1
    A[i+1] = key
Copy the code

As ifHere we can propose a loop invariant for insertion sort: before each iteration of the for loop begins, the subarrayIt’s still where it wasAnd are already sorted.

So, just like proving a mathematical induction formula, we need two steps to prove that it is correct:

Initialization: The loop invariant is true until the first iteration of the loop.
Maintenance: Assuming that it is true until one iteration of the loop, it follows that it is true until the next iteration.

But since we need cyclic invariants to prove the algorithm, we need to focus on what happens at the end of the loop, which leads us to the third property of the cyclic invariants that we need to prove:

Termination: When the loop terminates, the invariant gives us a useful property that helps prove that the algorithm is correct.

So let’s see how this is proved in detail:

Initialize the: before the first iteration of the loop (),By a single elementSo the cyclic invariant holds.
keep: assumingWhen, the loop invariant holds, i.e., subarraysThe original position is atAnd are already sorted. The current iteration of the loop keeps moving to the leftUntil you find the first one that’s smaller than that. When the loop is over,It’s still where it wasAnd are sorted. So it follows thatWhen, the cyclic invariant also holds.
Termination of: The condition that causes the for loop to terminate is, so at the end of the cycle,. In the cyclic invariant, we willwithInstead, it’s subarraysIt’s still where it wasAnd are sorted. So the algorithm is correct.