Past exam of the year 1 of the computer science course of the University of Oxford / 2003 / Functional programming, data structures and algorithms, procedural programming, and digital hardware / 6 / a / Solution

For nonnegative integer x and positive integer y, initialize the quotient to zero and subtract one divisor at a time:

q := 0; r := x;
WHILE r >= y DO
  r := r-y;
  q := q+1
END

The loop invariant is $x=qy+r$, $q\ge 0$, $r\ge 0$, with x and y unchanged. It is true initially. A body execution changes $qy+r$ to $(q+1)y+(r-y)=qy+r$ and keeps $r$ nonnegative because of the guard. The nonnegative integer loop variant $r$ strictly decreases by $y>0$, so termination follows. At exit the guard supplies $r<y$; henceThere are exactly $\lfloor x/y\rfloor$ body executions. Under the unit-cost model, the time complexity including initialization and the final test is $\Theta (1+\lfloor x/y\rfloor )$, which is $O(x)$ for integer $y\ge 1$. This is a bound in the value of x, rather than in its encoded bit length.