Struggling to find loop invariant in power function

I am struggling to find a good loop invariant for the following function, which returns a^b where a is a real number and b is a natural number:

power <- function(a, b){
c <- 1
while(b > 0){
if(b %% 2 == 1){
c <- c * a
}
b <- floor(b / 2)
a <- a * a
}
return c
}


I've ran through the loop with a couple of examples, and I see that it has 2 kinds of cases; when b is even or odd. I also understand that on the kth iteration, a = a_0^(2^k), but I am struggling to find a proper invariant as there is no real iterating variable to use.

• Sorry, that was two typos. Fixed now. Oct 8, 2022 at 23:29

It may clarify things to use different variable names. Let's call $$x$$ the desired result of $$a^b$$ where $$a$$ and $$b$$ are the inputs. With variables $$c', a', b'$$ initialized to $$c' = 1, a'=a, b'=b$$, you are basically maintaining that $$x = c'(a')^{b'}$$. At the end you have $$x = c'$$ because $$b' = 0$$. Each step "transfers" half of the exponent to the base of the exponentiation, or in the odd case, the coefficient.