Finding loop invariant

Question

I am really new concerning loop invariants and I am currently trying to figure out a loop invariant of an algorithm for prime numbers. I tried a lot of ideas, but I still have problems since there are two nested loops. I am also really grateful if someone have any tips regarding finding a loop invariant. My idea is that all $i$ which are primes are set on true and all $i$ which are not primes are set on false.. but I don't think that this is the loop invariant.

PRIME_FILTER(n)
1  P = INIT(n) // Initialize array P[1::n] with True
2  P[1] = False
3  i = 2
4  while i * i <_ n
5     if P[i] == True
6       j = i * i
7       while j <_ n
8          P[j] = False // Not prime
9          j = j + i
10    i = i + 1
11 return P

Answer 1

Let's see what the algorithm does in its first few iterations:

• Mark all elements other than 1 as "potentially prime".
• Mark all multiples of 2, starting at 4, as "not prime".
• Mark all multiples of 3, starting at 9, as "not prime".
• Skip 4, since it is known to be not prime.
• Mark all multiples of 5, starting at 25, as "not prime".
• Skip 6, since it is known to be not prime.
• Mark all multiples of 7, starting at 49, as "not prime".

So it continues, until the next element is already larger than $\sqrt{n}$.

Here is how we can describe the contents of the array:

• All elements other than 1 are "potentially prime".
• All elements not divisible by 2 are "potentially prime", except for 2.
• All elements not divisible by 2,3 are "potentially prime", except for 2,3.
• All elements not divisible by 2,3,4 (equivalently, by 2,3) are "potentially prime", except for 2,3.

And so on.

Hopefully this gives you some ideas on the loop invariant.

Answer 2

The inner loop is a "for" loop in disguise, from j to n in steps i. The invariant can only express that all values in the array P from the initial value of j until the current value of j have been set to False. It is worth to note that the initial value of j is i², hence all the indexes set to False are multiples of i.

The outer loop tries all increasing values of i from 2 on until i² exceeds n. The invariant of this loop expresses that for all i from 2 to the current value, the multiples of i such that P[i] is True, from i² to n have been struck out.

---

In fact, these invariants are not very informative, as they essentially repeat what the statements do. Things get more interesting if you establish, by a theorem, that all P[i] until the current i are True for primes and False otherwise. Hence the outer invariant can be rephrased as "the values in P up to i indicate primality of the corresponding index".