Loop invariant for an algorithm

Question

I have developed the following pseudocode for the sum of pairs problem:

Given an array $A$ of integers and an integer $b$, return YES if there are positions $i,j$ in $A$ with $A[i] + A[j] = b$, NO otherwise.

Now I should state a loop invariant that shows that my algorithm is correct. Can someone give me a hint of a valid loop invariant?

PAIRSUM(A,b):
YES := true;
NO := false;
n := length(A);
if n<2 then
  return NO;

SORT(A);
i := 1;
j := n;
while i < j do  // Here I should state my invariant
   currentSum := A[i] + A[j];
   if currentSum = b  then
      return YES;
   else 
    if currentSum < b then
      i := i + 1;
    else
      j := j – 1;
return NO;

Answer 1

First simplification: this algorithm, by inspection, cannot say YES when it shouldn't, since saying YES is immediately after a test verifying that the sum at the current positions is $b$.

Second simplification: It always terminates, since $i$ and $j$ move in a monotone way up and down respectively, and one always moves. Thus, eventually they become equal and the loop ends.

So let's assume that that answer is YES, and $x$ and $y$ are the indices we are interested in, after sorting, with $x$ as small as possible and then $y$ as large as possible (we may have several possible pairs with the right sum). Here is the invariant:

• At the start of the loop, $i\le x$ and $j\ge y$.

If $i=x$ and $j=y$, then the algorithm will stop and say YES. The loop invariant is trivial at the start, and also trivial when $i<x$ and $j>y$. But if $i=x$, and $j>y$, then, since the array is sorted $A[i]+A[j]>b$, because of how $y$ was selected. So $j$ decreases in all future iterations until it reaches $y$. The other case, where $j$ gets to $y$ first is symmetric.

As noted above, the algorithm always terminates, which implies the algorithm will actually say YES, so we are done.

Edit: Since this question is about proof writing, here is another option, which I think is more confusing and more gritty. I do not know if Tony Hoare would approve or not.

Here is the invariant: A the top of the loop,

• If $s<i$, then, for any $x\in [n]$, $A[s] + A[x] \neq b$
• If $t>j$, then, for any $x\in [n]$, $A[x] + A[t]\neq b$

Again, this holds vacuously at the beginning. Now we check some cases:

• If $i = j$, then in any pair of indices $x$ and $y$ at least one of $x$ or $y$ is smaller than $i$ or bigger than $j$. This rules out the input being a YES. The loop ends and says NO, so we are in good shape.
• Assume the loop did not end. If $A[i] + A[j] = b$, the answer is YES, and the algorithm works.
• Assume $A[i] + A[j] \neq b$.
• Subcase: If there is a $j'$, by hypothesis $j'<j$, such that $A[i] + A[j'] = b$, then $A[j'] < A[j]$ because the array was sorted, so $A[i] + A[j] > b$, which causes $j$ to decrease. This shows that the invariant is maintained for $i$. To see it for $j$, just note that if there is an $x$ such that $A[x] + A[j] = b$, then $x < i$, which is ruled out by the inductive hypothesis.
• Subcase: If there is a $i'$, by hypothesis $i'>i$, such that $A[i'] + A[j] = b$, then $A[i'] > A[i]$ because the array was sorted, so $A[i] + A[j] < b$, which causes $i$ to increase. This shows that the invariant is maintained for $j$. To see it for $i$, just note that if there is an $x$ such that $A[i] + A[x] = b$, then $x > j$, which is ruled out by the inductive hypothesis.
• Subcase: If neither of the other two cases holds, then the invariant is maintained trivially.

Finally, we note that the gap between $i$ and $j$ always gets smaller, so they must eventually become equal, and the algorithm will stop.

Remarks: This is the exact same argument, but more difficult to follow. You too can write proofs like this using some expert techniques:

• Don't say what the algorithm does. Here, if the input is a YES, the algorithm ALWAYS gives you certifying indices that are as close to the ends as possible. The 2nd proof cleverly hides this in a case analysis.
• Don't give names to things. Having hidden what the algorithm does, also don't name the stopping point.
• Don't factor out easy cases. This algorithm clearly works for NO instances. By not noting that up front, we get a more complicated invariant.

Answer 2

Perhaps something like this?

After k iterations of the loop, A[i...j] contains a sorted subarray of size n - k, with k of the original elements, none of which summing to b with any other element of A, having been removed.

Perhaps a clearer way of stating this is simply:

After k iterations of the loop body, for 0 <= k < n, A[i...j] is a sorted (contiguous) subarray of A[1...n] (whose elements are in the same order and have the same value as before the first iteration) of the loop body containing k elements (i.e., i + j = k + 1) such that A[1...n] contains a desired pair of elements if and only if A[i...j] does, as well.

This loop invariant is useful because, if the loop finishes (i.e., reaches the termination condition), then A is the sorted array with one element, and we can conclude that there is no pair of elements in A.

Here is a proof sketch/idea for this invariant:

• Before the loop, A[1...n] is a sorted array and i = 1, j = n. Therefore, the loop invariant is guaranteed to after k = 0 iterations of the loop body.
• Assume that the loop invariant holds true for k up to and including k'.
• We now show that the loop invariant holds for k' + 1. There are three cases for the behavior of the loop body during the iteration corresponding to k = k' + 1:
  • A[i] + A[j] = b, in which case the loop correctly returns YES and there is no iteration after this iteration of the loop;
  • A[i] + A[j] < b, in which case we can safely discard the smallest element of A, A[i]. To see this, note that since A[j] is the largest element in A, if the sum of it and another element in A is smaller than b, then sum of that other element and any element of A is also guaranteed to be less than b.
  • A[i] + A[j] > b, in which case we can safely discard the largest element of A, A[j]. The reasoning is similar to that for the case A[i] + A[j] < b.
• After termination of the loop body, i = j and so A contains only one element. Since A now contains only one element, it is trivially the case that A does not contain two elements summing to b.

Demonstrating the sufficiency of the loop invariant to show that there is no solution after termination of the loop

This addresses a question raised in the comments by Raphael, here is some clarification on why this loop invariant should be sufficient.

For the loop to terminate, we must have i = j. Notice also that this loop always terminates, either by correctly emitting YES if a match is found, or by removing array elements until only one remains (by either incrementing i or decrementing j). This termination argument is not given in the sketch above, but should be straightforward.

Since i = j, A is a sorted subarray of size one. Because no array of size 1 satisfies the requirement that there exist $x, y$ (note that I am interpreting this to mean unique $x, y$, since otherwise the algorithm provided is incorrect; consider A = [1] and b = 2) where $A[x] + A[y] = b$, and since by the loop invariant we know that no element A[k], where k != i = j, could be added to any element A[k'], where k' != k, to achieve sum b, this completes the proof idea.

Assumptions/facts used for termination condition:

• The question was interpreted correctly, i.e, $x$ and $y$ are distinct; you have to add elements at different positions in the original array.
• i = j after the (normal) termination of the loop body, and the loop always terminates;
• There are not two distinct $x$ and $y$ between i and j if i = j; there aren't two indices in a subarray of size 1.
• By the loop invariant, for k != i = j, there is no way to add A[k] to any A[k'], k != k', to get b; we have only thrown out, by incrementing i and decrementing j, elements which couldn't possibly sum to b with any element of the original array.

Please feel free to help out if I continue to be missing something subtle.

Answer 3

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}$$

Answer 4

There is no foolproof way to derive a helpful invariant; note that the problem is not computable (otherwise we could solve the halting problem). Therefore, your are back to trial and error with heuristics trained by experience. See Gilles' answer for an exemplary thought process. In general, you need the desired post condition (i.e. output specification) first and find an invariant that implies it (together with the negated loop condition).

Here is what I think works:

$\qquad \begin{align} I = &\phantom{\land}\ A \text{ is sorted and has not been changed} \\ &\land\ 1 \leq i,j \leq n \\ &\land\ j \geq i \\ &\land\ \forall i' \lt i.\ \forall j' \gt j.\ A[i'] + A[j'] \neq b \\ &\land\ \forall i' \lt i.\ b > A[i'] + A[j] \\ &\land\ \forall j' \gt j.\ b < A[i] + A[j'] \end{align}$

That the latter three clauses are actually maintained by the loop -- assuming you do not terminate with YES which is trivially correct -- is tedious to show because they are heavily interdependent and $i,j$ can switch roles.

In the end, you get $i=j$ which allows to combine the last two clauses to the fact that the last element $A[i]$ does not sum up to $b$ with any other element. Combination between elements from left and right are excluded by clause three. Finally, two elements left of $i$ can not sum up to $b$ because of clause four and one, and similarly for two elements right of $i$.

If you do the proofs, make sure to follow the rules of Hoare logic closely.