There are always infinitely many valid loop invariants. The trick is to find one that suffices to prove what you want to prove about the algorithm, and that you can prove (usually by induction over the number of loop iterations).
There are three parts in proving the correctness of this algorithm:
- The algorithm never performs an incorrect step. Here, the potential incorrect steps are to access an array element outside the bounds of the array.
- When the algorithm returns
YES
or NO
, this output is correct.
- The algorithm terminates for every input.
For correctness, you need to prove that $1 \le i \le n$ and $1 \le j \le n$. This had better be part of your invariant. Given the loop condition $i < j$, you can condense this to $1 \le i < j \le n$ at the entry into the loop body. This condition is not true when the loop test is reached at the end, but it may come in useful to notice that $i \le j$ (because inside the loop body, with $i < j$, $i$ and $j$ only change by $1$, which can at worst turn this strict inequality into an equality).
When return YES
is executed, $A[i] + A[j] = b$ is apparent. So this part doesn't need anything particular to be proved.
When the last return NO
statement is executed, meaning that the loop terminated normally (and so $i < j$ is false), you need to prove that $\forall i, \forall j, A[i] + A[j] \ne b$. This property is obviously not true in general: it doesn't hold if the answer is YES
. You need to strengthen this property: you have a special case, which needs to be generalized. This is a typical case of a property that applies only to the part of the array that has been traversed already: the loop is constructed so that if $(x,y)$ is a previous value of $(i,j)$ (i.e. $1 \le x \le i$ and $j \le y \le n$ and $(x,y) \ne (i,j)$) then $A[x] + A[y] \ne b$. This had better be expressed in the loop invariant.
Are we done there? Not quite; all we know on the normal loop termination is that $\forall x \le i, \forall y \le j, A[x] + A[y] \ne b$. What if we had $x > i$ and $y \le j$, or $x \le i$ and $y > j$: could we have $A[x] + A[y] \ne b$? That's difficult to tell without more information. In fact, we'd better distinguish some cases when $A[x] + A[y] > b$ and the cases when $A[x] + A[y] < b$. With these properties, we can use the fact that the array is sorted to deduce facts about other positions in the array; with only $\ne b$, we have nothing to work on. We don't know which way $A[x] + A[y]$ lies for some random $x < i$ and $y > j$; but we do know what happens at the boundary: if $i$ is incremented, it's because $A[i] + A[j]$ is too small, and if $j$ is decremented, it's because $A[i] + A[j]$ is too large. Think what loop invariant could express this; I'll give a possibility below.
Note that this property doesn't directly give you the desired condition for the return NO
statement; you'll still need to look at what happened in the last run of the loop, or alternatively to prove a stronger loop invariant that takes a closer look at when $A[x] + A[y] < b$ and when $A[x] + A[y] > b$.
Finally, for termination, you need to relate $i$ and $j$ with the number of iterations through the loop. Here, this is simple: either $i$ or $j$ moves at each turn, so $j - i$ decreases by $1$ at each loop iteration; you don't need to use a loop invariant to prove this.
We've obtained the following invariant:
$$ \begin{array}{l}
1 \le i \le j \le n \wedge \\
(\forall x < i, \forall y < j, A[x] + A[y] \ne b) \wedge \\
(\forall x < i, A[x] + A[j] < b) \wedge \\
(\forall y > j, A[i] + A[y] > b)
\end{array}$$
A
being sorted. 2)i
andj
switch roles at the end of the loop depending on the input. 3) The number of loop executions depends on the input. $\endgroup$ – Raphael♦ Apr 9 '12 at 17:58