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 から始めると、xa はゼロになり、b ⁰ = 1 になり、これが y の初期値になります。

ループが進行するにつれて、x が減少するたびに y に b が乗算されます。

ループの最後で x はゼロなので、y = b ^aです。