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

    //invariant: 2&lt;=i&lt;=bound and n mod i=0
    int i = 2;
    while (i&lt;=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)).
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 &lt; 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.