這段代碼的循環不變量是什麼？

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（這證明，該算法將完成）