Remove each prime power as soon as it is found, and stop trial division once the remaining value has no possible smaller factor:At an outer-loop boundary, write , where is the product of the prime powers already removed. The invariant states that
def divisors(n: Int): Int = {
require(n >= 1)
var remaining = n
var factor = 2
var result = 1
while (factor.toLong * factor.toLong <= remaining.toLong) {
var exponent = 0
while (remaining % factor == 0) {
remaining /= factor
exponent += 1
}
result *= exponent + 1
factor += 1
}
if (remaining > 1) result *= 2
result
}result is , every prime divisor of is smaller than factor, and remaining has no prime divisor smaller than factor. Thus if factor divides remaining, it is prime; a composite factor would have a smaller prime divisor, contrary to the invariant.During the inner loop, with fixed, . Each division removes one copy, so the positive remainder strictly decreases and supplies an inner-loop variant. On leaving the inner loop the complete power has been removed; multiplying the result by
exponent + 1 uses part (d) and reestablishes the outer invariant after advancing factor. The outer factor increases and can never exceed the original while its guard holds, proving termination.At exit, a remainder greater than one must be prime: a composite remainder would have a prime factor no larger than its square root, which would still be smaller than
factor. It therefore contributes one final factor of two. A remainder of one contributes nothing. The algorithm returns using constant auxiliary space and no array. The widened multiplication in the loop guard prevents an Int overflow in the square test. Articles by others on the same topic
There are currently no matching articles.