I'm new to the concept of loop invariant and I'm trying to figure out the loop invariant for a program that returns if an integer is prime and, if not, one possible factorization. My intuition is that as a loop invariant condition we need i in the range [2,floor(sqrt(n))] and then n mod i !=0 implies n is prime

bool IsPrime(int n)
    if (n == 1) return false;
    if (n == 2) return true;

    //if n (>2) is prime, it's prime factor is just n
    //if n (>2) is not prime, n=a*b, where both a,b<n and we have either a<sqrt(n) or b<sqrt(n)
    var bound = (int)Math.Floor(Math.Sqrt(n));

    //invariant: 2<=i<=bound and n mod i=0
    int i = 2;
    while (i<=bound) 
        //if n is divisible by some integer smaller than the upper bound it is not prime
        if (n % i == 0)
            Console.WriteLine(" " + n/i);
            Console.WriteLine("x" + i);
            return false;
    return true;        

Could you please tell me if that is enough? I already made many attempts and that's the only statement that holds true for the whole loop until i=floor(sqrt(n)).

  • $\begingroup$ Your second comment is wrong for n=4 or n=9, for example. $\endgroup$ – gnasher729 Mar 5 '18 at 8:12

The condition $2 \leq i \leq \lfloor \sqrt{n} \rfloor$ is a reasonable part of the invariant you seek. As I think you realize, this is not enough.

You proposed to also require $n \!\!\!\mod i \neq 0 \implies n$ prime, but this can not realistically hold. For instance, take $n=3^2=9$: running the loop we would start from $i=2$ and have $n \!\!\!\mod i = 1 \neq 0$ but clearly $n=9$ is not prime, which makes the condition false. Hence, that is not really an invariant.

What we need is something expressing "we checked all the numbers from $2$ to $i-1$, and we did not find any divisors". This can be written as "for all the numbers $k$ such that $2\leq k < i$, we have $k\!\! \mod n \neq 0$".

That might be enough, but the loop seems to have a bug to me: for e.g. $n=5^2$ we never try to divide for $i=5$, consequently returning that $25$ is prime. Perhaps you should fix the bug first, and then adapt the first "range" invariant accordingly.

| cite | improve this answer | |
  • $\begingroup$ I corrected the bug, indeed unlike my proof, it didn't include the write range. $\endgroup$ – FunnyBuzer Mar 4 '18 at 21:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.