Any hints about loop invariant of weird loop?

Question

I have this tiny program for finding largest prime divisor (taken from Code Review Stackexchange and written by user Altinak: https://codereview.stackexchange.com/a/74792):

Here is my try to write it in pseudocode:

GLOBAL VARIABLE highest;

// This function takes parameters n and f with 1 <= n and 2 <= f.
// It returns n with f factored out of it.
// Also, if f divides n and if f > h then it replaces h with f

factorize(n, f) {
    if (n < f)
        return n
    while (n mod f == 0) {
        n = n / f
        if (f > highest)
            highest = f
    }
    return n
}

find(n) {
    highest = 1

    n = factorize(n, 2)
    n = factorize(n, 3)

    if (n >= 5) {
        i = 5
        while (i * i <= n) {
            n = factorize(n, i)
            n = factorize(n, i + 2)
            i = i + 6
        }
    }
    if (n == 1)
        return highest
    else
        return n
}

But the while loop in the function find is harder than ones I have seen before - its number of iterations aren't easy to calculate before the loop, as the variable n from the condition i * i <= n changes in the loop body.

Right now I feel like I'm stuck and have no idea how to write the loop invariant for this loop, but I will try to think of something. Meanwhile, big thanks in advance for any hints!

Answer 1

The invariant says that the current value of n is the initial value of n divided by all its factors in the trial sequence 2, 3, 5, 7, 11, 13, 17, 19, 23, 25, 29, 31... until i. Some of the numbers in this sequence are not primes, but their factors have been previously processed and simplified, so equivalently, we have n divided by all its prime factors until i.

The number of iterations of the while loop equals the number of elements of the sequence 5², 7², 11², 13², 17², 19²... that do not exceed n[5], n[7], n[11]... respectively, where n[m] denotes the value of n after all factors until m have been removed. So the number of iterations is also the number of elements of the sequence until the highest prime factor.

In addition, the function factorize executes a number of divisions equal to the multiplicity of the prime factor f in the number n. When f is not a prime, the function returns immediately because its factors have already been consumed; the iteration count is the same for the initial and current n.

Hence, the total complexity will be like the sum of the multiplicities of the prime factors of n, plus the highest prime factor.