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

Accumulate the prefix by Horner's method in base two. digit-'0' converts either permitted digit to its numerical value:The loop invariant, in exact arithmetic, is that i is the number of processed digits before the point andAppending a digit shifts the old positional value by one binary place and adds that digit, which proves preservation. The loop variant is $bin.length-i$. At exit, i is the binary-point index or the length if no point occurs, and integerPart is the value of the integer prefix. An empty prefix contributes zero. There is one multiplication per processed digit, with no separate powers or repeated divisions. Short-circuit evaluation prevents an out-of-range access when the point is absent.

For Double, this exact-arithmetic invariant describes the intended value; the operational value is the rounded Horner recurrence. Very long prefixes can lose precision or overflow, as discussed in part (g). A fixed-width return type cannot represent every finite binary digit string exactly.