Well, let's look at an example.
Here is the classic NOD calculation algorithm:
if (m < 0) m = -m; if (n < 0) n = -n; while (m != 0 && n != 0) { if (m > n) m -= n; else n -= m; } gcd = m + n;
Let's think that we have an invariant step.
On the one hand, it is obvious that, by virtue of testing, m and n are always positive or 0. This is an invariant: at the beginning it is executed, and at every step we always have a decrement that is not less than that which is subtracted, so that after the step of the loop the invariant is still executed.
But this is a weak invariant, because the necessary postcondition will not be obtained from it: we want to prove that gcd contains the greatest common divisor! And from our invariant it does not follow.
Therefore, we must look for a stronger condition. It will be like this: m and n are always positive (or 0), and the GCD ( m , n ) does not change!
We have already proved the first part of the condition (it coincides with the former, weak invariant). The second one also follows easily from the fact that GCD ( m , n ) = GCD ( m - n , n ). Thus, we see that if the cycle ends, then in gcd there will be a nonzero number of m , n , which is equal to the desired GCD (since GCD ( m , 0) = m , GCD (0, n ) = n ).
(It should be added that the algorithm is guaranteed to end, since at each step the largest of m , n decreases by at least 1, but due to the invariant m and n cannot be negative, therefore the algorithm cannot continue more than ( m + n ) iterations. That's the first condition of the invariant handy!)
