CODEWITHSUNDEEP
loopsconditional-statementsinvariantsloop-invariant
kia
kia

Reputation: 1

What is the Loop Invariant in the following code

What is the Loop Invariant(s) in this sample code.
This is an excerpt code implemented in C programming language:

//pre-condition m,n >= 0
x=m;
y=n;
z=0;
while(x!=0){
  if(x%2==0){
    x=x/2;
    y=2*y;
  }
  else{
    x=x-1;
    z=z+y;
  }
}//post-condition z=mn

These are my initial answers (Loop Invariant):

  1. y>=n
  2. x<=m
  3. z>=0

I am still unsure about this. Thanks.

Upvotes: 0

Views: 499

Answers (1)

Howard
Howard

Reputation: 39217

Your answers are indeed invariant but say little about the conditions of your loop. You always have to look for specific invariants. In this case it is quite easy since there are only two (exclusive) operations inside your loop.

The first x' = x/2; y' = 2*y; looks like it is invariant under x*y.

The second x' = x-1; z' = z+y; is not: x'*y' = x*y - y. But if you add z again it will be invariant. z'+x'*y' = z + y + x*y - y = z+x*y.

Fortunately also the first condition is invariant under z+x*y and thus we have found a loop invariant.

  • pre-condition: z+x*y = m*n
  • post-condition: x=0 (loop condition) and therefore we can deduce from our invariant: z = m*n

Upvotes: 2

Related Questions