= Solution
Let `point` be the known point index. Work backwards so that each step uses just one division, rather than separately computing positional weights:
``
var j = bin.length - 1
var fractionalPart = 0.0
while (j > point) {
fractionalPart = (fractionalPart + (bin(j) - '0')) / 2.0
j -= 1
}
``
The <loop invariant>, under exact arithmetic, is
$$
fractionalPart=\sum_{t=j+1}^{bin.length-1}(bin(t)-\mathtt{'0'})2^{j-t}.
$$
Initially the suffix is empty. Incorporating digit $j$ and dividing by two gives exactly the same formula with $j$ replaced by $j-1$. At exit $j=point$, \b[the result is $\sum_{t>point}(bin(t)-\mathtt{'0'})2^{point-t}$]. The <loop variant> is $j-point$ when a point exists. If a no-point input is handled by setting `point=bin.length`, the loop is skipped and the fractional contribution is zero; $\max(0,j-point)$ is a <loop variant> covering that convention too. Trailing zeroes and an empty fractional suffix require no special arithmetic. <Floating-point rounding> qualifies the exact formula for long inputs.
Back to article page
