loops - What is the Loop Invariant in the following code

Question

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.

Answer 1

您的答案确实是不变的，但对循环的条件几乎没有说明。您总是需要寻找特定的不变量。在这种情况下，这很容易，因为循环中只有两个（独占）操作。

第一个x' = x/2; y' = 2*y;看起来在 下是不变的x*y。

第二个x' = x-1; z' = z+y;不是：x'*y' = x*y - y。但是，如果您z再次添加，它将是不变的。z'+x'*y' = z + y + x*y - y = z+x*y.

幸运的是，第一个条件在下是不变的z+x*y，因此我们找到了循环不变量。

• 前提：z+x*y = m*n
• 后置条件：（x=0循环条件），因此我们可以从不变量中推导出：z = m*n