Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Imperative programming / 1 / b / Solution

Let point be the known point index. Work backwards so that each step uses just one division, rather than separately computing positional weights:The loop invariant, under exact arithmetic, isInitially 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$, the result is ${\sum }_{t>point}(bin(t)-{}^{\prime }{0}^{\prime })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.