algorithmnested-loopspseudocodediscrete-mathematicsloop-invariant

Find loop invariant of this simple algorithm

I'm sure this is a really simple question but I can't seem to crack it. Prove the correctness of your algorithm; i.e. state its loop invariant and prove it by induction.

Below is my algorithm. I know how to do the second part (prove by induction) but I just cant figure out the loop invariant for the life of me.

procedure intersection(A,B: list of integers)

  C= empty list
  for i:=1 to n:
    for j:= 1 to m:
      if Ai = Bj
        if Ai not in C
          C.append(Ai)
  return C
Solution

  • To get you started, I just state one of the loop invariants so that I don't give the solution completely away. The invariant for the outer loop is:

    C = intersection (B, {a1, ..., ai})

    You will also need an invariant for the inner loop.