Loop invariant for an algorithm

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;

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 $iy$. 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

• 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' 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

• 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] 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.

StackExchange Computer Science Q#1157, answer score: 5