What's the loop invariant for this code?

Question

I need to come up with a loop invariant for a given piece of code:

//pre: x & y >= 0
//post: z = x^y
//computes pow(x, y), x^y
int pow(int x, int y){
    int z = 1;
    while(y > 0){
        if(y%2==0){
            y /= 2;
            x = x*x;
        }else{
            z = z*x;
            y -= 1;
        }
    }
    return z;
}

My invariant is:

{(ypre - 0 = 0 & x = x^(ypre  -y)) OR (ypre - y != 0 & x^(n + m) = x^(ypre - y), where (n=ypre-y) and (m=integer value of z/x))}

This is a messy invariant, and I'm not 100% sure it's correct. Is there a better invariant that would cover the post condition of z = x^y

Answer 1

I would suggest one loop variant is

• that x' ^ y' == (x ^ y)/z (where x' and y' are the modified inputs after any iteration)
• that x' >= x and 0 <= y' < y (this proves that the algorithm will finish)