下面代码中的循环不变式是什么
此示例代码中的循环不变式是什么。
这是用 C 编程语言实现的摘录代码：
//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
这些是我最初的答案（循环不变）：
y>=nx<=mz>=0
我对此仍然不确定。谢谢。
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):
y>=nx<=mz>=0
I am still unsure about this. Thanks.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（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*nx=0（循环条件），因此我们可以从不变量中推出：z = m*nYour 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 underx*y.The second
x' = x-1; z' = z+y;is not:x'*y' = x*y - y. But if you addzagain 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*yand thus we have found a loop invariant.z+x*y = m*nx=0(loop condition) and therefore we can deduce from our invariant:z = m*n