Возможные инвариант цикла

Question

Рассмотрим следующий цикл:

y=1; 
x=a; 

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

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

Я хочу заключить у = Ь

Я размышлял некоторое время и не могу показаться, чтобы выяснить достаточно сильный контур инвариант позволяет сделать это. Кто-нибудь знает, как подойти к этому?

Любая помощь или понимание глубоко оценены.

Answer 1

Инвариант здесь: y = b ^a-x.

Вы начинаете с x = a, поэтому x-a равно нулю, и b = 1, которое является начальным значением y.

По мере прохождения цикла y умножается на b каждый раз, когда x уменьшается.

В конце цикла x равен нулю, поэтому y = b ^a.