Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Imperative programming (resit) / 1 / b / Solution

Keep both the exponent and its power. This Oberon procedure uses only the permitted arithmetic:The loop invariant is $i\ge 0$ and $p=b^i\le n$. It holds initially because $n>0$. A successful guard permits the next power, and the two assignments preserve the relation between $p$ and $i$. At exit, $p\le n<pb$, which is exactly part (a). Each iteration increases $i$, and only finitely many powers of $b\ge 2$ are at most $n$, proving algorithm termination. The returned value is $\lfloor {\log }_{b}n\rfloor$. Its running time is $\Theta (1+{\log }_{b}n)$ arithmetic operations; integer overflow is deferred to part (e).