loops - 这段代码的循环不变量是什么？

Question

我需要为给定的一段代码想出一个循环不变量：

//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;
}

我的不变量是：

{(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))}

这是一个混乱的不变量，我不能 100% 确定它是正确的。是否有更好的不变量可以覆盖 z = x^y 的后置条件

Answer 1

我建议一种循环变体是

• 那x' ^ y' == (x ^ y)/z（在任何迭代后修改输入的位置x'和位置）y'
• 那x' >= x和0 <= y' < y（这证明算法将完成）