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

Generate the fractional bits by repeated doubling, keeping only the unconverted residual:Let $f_0=dec-int\_part$ and $k=out-digits-1$. The loop invariant is $0\le fraction<1$, the first $k$ fractional digits have been written, and, in exact arithmetic,Doubling exposes the next digit, and subtracting that digit leaves the next residual in $[0,1)$. This proves preservation. The loop variant is $res.length-out$. The loop fills the whole suffix, even when the residual has become zero; subsequent bits are zero. There is one multiplication per output bit. With $F=res.length-digits-1$ fractional positions, the result is truncated, with exact-arithmetic error $0\le dec-value(res)<2^{-F}$. An integer has an all-zero suffix. No rounding-up step is performed.