Cyclic invariant

Cyclic invariants are used primarily to help understand the correctness of algorithms. For cyclic invariants, three properties must be proved:

Initialization: The loop invariant is true at the beginning of the first iteration of the loop.
Hold: If a loop invariant is true before one iteration begins, then it is true until the next iteration
Termination: When the first two properties are satisfied, it is guaranteed that the invariant is true each time the cycle begins. So we can use this property to verify the correctness of our algorithm.

In fact, cyclic invariants are analogous to mathematical induction. Proving that the initialization property is satisfied is like proving the base case in induction, proving the retention property is like proving the induction step in induction, except in mathematical induction the induction step is infinite, and our algorithm has to stop induction at the right time, otherwise it doesn’t make sense.

Take a chestnut

Fibonacci numbers

int fib(x) {
    A ==fib(I)&&b==fib(I +1)
    int a = 0, b = 1, tmp;
    // Initialization: a==0==fib(0)&&b==1==fib(1) before the iteration starts, the loop invariant is true.
    for (int i = 0; i < x; i++){
        // Assume that a==fib(I)&&b==fib(I +1) is true before the start of an iteration
        tmp = a;
        // A becomes fib(I +1)
        a = b;
        // b becomes fib of I +1 +fib of I =fib of I +2.
        b = tmp + b;
        // Hold: at the end of the loop, at the beginning of the next iteration, I becomes I +1, a==fib(I +1)&&b==fib(I +2), so the loop invariant is still true
    }
    If a==fib(x), the result is correct and therefore the algorithm is correct.
    return a;
}
Copy the code

Cyclic invariant