loops - 次のコードのループ不変条件とは何ですか

Question

このサンプルコードのループ不変条件とは何ですか。
これは、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

これらは私の最初の答えです（ループ不変条件）：

私はまだこれについて確信が持てません。ありがとう。

score 2 · Accepted Answer

あなたの答えは確かに不変ですが、ループの条件についてはほとんど言いません。常に特定の不変条件を探す必要があります。この場合、ループ内に (排他的な) 操作が 2 つしかないため、非常に簡単です。

最初x' = x/2; y' = 2*y;のものはの下で不変であるように見えますx*y。

2番目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ため、ループ不変が見つかりました。

1 に答える 1