Что это за цикл для этого кода?

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% это верно. Есть ли лучший инвариант, который будет охватывать пост состояние г = х^у

Answer 1

Я хотел бы предложить один вариант петли

• что x'^y' == (x^y)/z (где x' и y' являются модифицированные входы после любой итерации)
• что x' >= x и 0 <= y' < y (это доказывает, что алгоритм завершится)