The intersection problem revisited

On the first attempt to solve the intersection problem and do the proof of correctness the class encountered a couple of problems:

• Using an algorithm that does not lend itself well to doing a proof of correctness.
• Using a more appropriate algorithm, but then having problems with the proof.

Given all of this, I am going to give everyone a second shot at this problem. The first pass through was worth 35 points, while this second round will be worth an additional 15 points. On this second pass through I am going to ask you to use my algorithm and my loop invariant. Your job will be to write the proof again using my algorithm and my invariant.

The algorithm to use

Intersection(A,B)
  // Count the number of elements in the intersection
  i = 1;
  j = 1;
  count = 0;
  while i <= A.length and j <= B.length
    if(A[i] == B[j])
      count++;
      i++;
      j++;
    else if(A[i] < B[j]
      i++;
    else
      j++;
  // Create a new array of the correct size
  let C[1..count] be a new array
  // Move the intersection elements into C
  k = 1;
  i = 1;
  j = 1;
  while i <= A.length and j <= B.length
    if(A[i] == B[j])
      C[k] = A[i];
      k++;
      i++;
      j++;
    else if(A[i] < B[j])
      i++;
    else
      j++;

The invariant to use

For your proof you should use the following loop invariant:

(C[1..k-1] = A[1..i-1] ∩ B[1..j-1]) and (A[i] > B[1..j-1]) and (B[j] > A[1..i-1])

Helpful hint There is a very specific reason that I added the extra conditions to my invariant. This information will prove helpful when it comes time to argue that when the algorithm skips over an item and does not put it in C it is doing it because that item can not possibly be in the intersection. The extra conditions will also help when it comes time to deal with the loop termination: you need to be able to argue that any elements still left in either A or B can not possibly be in the intersection.