What is the loop invariant of the following function? x = n; y = 0

while x &gt;= b:

   x = x DIV b

   y = y + 1

return y


This function takes in $n,b\in\mathbb{N}, n &gt; 0, b &gt; 1$, and returns $k\in\mathbb{N}$ such that $b^k\leq n \lt b^{k+1}$

So far I think it is:

$b^y \leq n$

$x \leq n$

but now I'm stuck
Try finding a loop invariant of the following form:
$$
f(x,y) \leq n &lt; g(x,y).
$$

For example, when $y=0$ you could choose $f(x,y) = x$ and $g(x,y) = x+1$, and in the end you want this invariant to imply $b^y \leq n &lt; b^{y+1}$.

To get some intuition, note that if $n = b^k z + w$, where $0 \leq w &lt; b^k$, then after $k$ iterations, we have $x = z$. This can help you formulate the loop invariant.