# What is the loop invariant of the following function?

x = n; y = 0

while x >= b:

x = x DIV b

y = y + 1

return y


This function takes in $n,b\in\mathbb{N}, n > 0, b > 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

• Why are you talking about 'the' loop invariant. Think about what statement you want to show true at the end of the program first. – Apiwat Chantawibul Jul 29 '17 at 22:09
• The statement that I wanna show true is $b^k \leq n \lt b^{k+1}$, but I need a proper LI in order to do this – K Split X Jul 29 '17 at 23:13

Try finding a loop invariant of the following form: $$f(x,y) \leq n < 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 < b^{y+1}$.
To get some intuition, note that if $n = b^k z + w$, where $0 \leq w < b^k$, then after $k$ iterations, we have $x = z$. This can help you formulate the loop invariant.
• What is $z,w$ in this case? – K Split X Jul 30 '17 at 14:29
• It's the result of dividing $n$ by $b^k$. – Yuval Filmus Jul 30 '17 at 15:42