Solution (source code)

= 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.