Recursion is closely linked to iteration. In fact, a while loop can be written as a recursive subroutine (and this how the language Prolog achieves ‘iteration’: see page 77). In com- puter science we would like to prove correctness and other properties about algorithms. Proofs about algorithms can be more difficult than the proofs about simple properties of the integers that I often use as examples this book.
A tool that helps us to prove properties about algorithms is an invariant. For ex- ample, a loop invariant is a property P of a loop such that:
1. P is true before the loop is executed, and
2. P remains true after each execution of the body of the loop (but not necessarily
in-between the steps within the body).
So to prove that an algorithm A has the property Q (the post-condition), we can find an invariant P of A such that Q follows from P, together with the fact that A has terminated. This last fact that A has terminated means that the loop condition (the guard of the loop) has become false.
In more detail, we need to find an invariant and show four things about it:
1. Initialization or basis property. The invariant holds before the first iteration of the loop.
2. Maintenance or inductive property. If the invariant holds before an iteration, then it also holds before the next iteration.
3. Termination and falsity of guard. After a finite number of iterations the guard be- comes false and the loop terminates.
4. Correctness of the post-condition. The invariant together with the negation of the guard imply that the post-condition holds, in which case the program is correct.
In one of the pencasts of this course, we prove the correctness of analgorithm using an invariant. You can find that pencast here: youtu.be/GSvqF48TVM4.
As an example, consider the simple loop:
while (x < 10) x = x+1;
What does this loop achieve? What is an invariant that helps us to prove the loop correctly achieves this? The invariant is x ≤ 10—check that it does satisfy the above four properties!
While invariants can be useful, a suitable invariant can be difficult to find.
There is a form of logic, Floyd–Hoare logic, in which we can express invariants and can formally prove the (partial) correctness of a program. Read about it on wikipedia: en.wikipedia.org/wiki/Loop_invariant.