= Solution
Test each positive candidate <divisor> and count the successful remainder tests:
``
def divisors(n: Int): Int = {
require(n >= 1)
var candidate = 1L
var count = 0
while (candidate <= n.toLong) {
if (n.toLong % candidate == 0L) count += 1
candidate += 1L
}
count
}
``
The <loop invariant> is $1\leq d\leq n+1$ and $count=|\{j:1\leq j<d,\ j\mid n\}|$, where $d$ denotes `candidate`. A successful test adds exactly the new <divisor>; an unsuccessful test leaves the count unchanged. The <loop variant> is $n+1-d$, which decreases by one. At termination $d=n+1$, so \b[the returned value is $\tau(n)$]. A `Long` loop counter prevents the increment after the last positive `Int` candidate from wrapping around.
Back to article page