Finding a good loop invariant for a powering procedure

Consider the following algorithm for computing integer powers:

Procedure power(integer x, integer n)  
    power := 1  
    for i := 1 to n  
        power := power * x
    return power

Can we say that the loop invariant is $power \leq x^n$ ?

Before the loop $power$ is initialized to $1$ so its equal to $1 \leq x^n$.

How do we prove maintenance of the invariant?

No, you can't say that $power \leq x^n$ is a loop invariant, since it is not maintained by the loop. For example, if $x > 1$ and at the current iteration $power = x^n$, then the invariant is satisfied at the beginning of the loop but not at the end of the loop.

Also, this loop invariant doesn't help you prove that at the end $power = x^n$, which is presumably your end goal.

Try to think of an invariant which describes the value of $power$ in terms of $x$ and $i$.

StackExchange Computer Science Q#54790, answer score: 6