Częściowa poprawność algorytmu

[drago77]

Prosiłbym o pomoc w rozwiązaniu zadania:

Udowodnij, że poniższy fragment programu jest częściowo poprawny.

Kod: Zaznacz cały

// b > 0, a > 0
x = 1;
y = b;
while (y!=0) // x= a^(b-y)
{
    x *= a;
    y--;
}
// x = a ^b