Search code examples
loopsinvariantsloop-invariant

Possible loop invariant

Consider the following loop:

y=1;
x=a;

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

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

I wanna conclude y = ba

I been pondering for a while and cant seem to figure out a strong enough loop invariant that allows me to conclude that. Does anyone have any idea how to approach this ?

Any help or insight is deeply appreciated.

Solution

  • The invariant here is y = ba-x.

    You start off with x=a, so x-a is zero, and b0 = 1, which is the initial value of y.

    As the loop progresses, y gets multiplied by b each time x decreases.

    At the end of the loop x is zero, so y = ba.