loops - 可能的循环不变式

Question

考虑以下循环:

y=1;
x=a;

//with a>=0 , b>=0

while(x>0){
  y=y*b;
  x=x-1;  
} 

我想得出 y = b^a

我思考了一段时间，似乎无法找出一个足够强大的循环 不变式让我得出这样的结论。有谁知道如何解决这个问题？

非常感谢任何帮助或见解。

Answer 1

这里的不变量是 y = b^a-x。

从 x=a 开始，因此 x-a 为零，b⁰ = 1，这是 y 的初始值。

随着循环的进行，每次 x 减小时，y 都会乘以 b。

循环结束时 x 为零，因此 y = b^a。