Loop invariant condition IsPrime program

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;
}
i+=1;
}
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)).

• Your second comment is wrong for n=4 or n=9, for example. – 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.