CODEWITHSUNDEEP
loopsinvariantsloop-invariant
some1fromhell
some1fromhell

Reputation: 135

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.

Upvotes: 2

Views: 48

Answers (1)

Sergey Kalinichenko
Sergey Kalinichenko

Reputation: 727047

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.

Upvotes: 2

Related Questions