如何找到循环不变量

Question

我知道循环不变量旨在证明问题的正确性，但我不太明白如何提出一个问题，无论问题多么微不足道。这是一个例子，有人可以指出我应该考虑采取什么步骤。我知道循环中发生变化的所有值都必须包含在我的不变量中。请指导我解决这个问题，我还必须找到后置条件。一个解释比一个答案更有价值；请帮忙。

{M > 0 and N >= 0 }

a = M;
b = N;
k = 1;

while (b > 0) {
    if (b % 2 == 0) {
        a = a * a;
        b = b / 2
    } else {
        b = b – 1;
        k = k * a;
    }
}

{ ? ? }

Answer 1

关于循环不变量的棘手部分是没有算法（我知道）可以始终保证“正确”答案。

首先，对于您问题中的算法，尝试跟踪程序并找出算法的目标（提示：指数很有趣）。在跟踪时跟踪变量 a、b 和 k。

例如，使用M = 2 和N = 1,2,3,...。在 N 的几个值之后，您会注意到变量 a、b 和 k 之间的关系将开始发展。

一旦你弄清楚循环不变量，后置条件应该很容易想出。

希望这会为您带来成功！

Answer 2

嗯，你在这方面有点倒退了。正如您所说，循环不变量的目的是帮助您证明程序的正确性。我猜你没有写这个程序——否则你会知道它的用途，并且你会在编写循环之前想出循环不变量，因为它是理解循环正确的关键。

那么...这个程序是干什么用的？你怎么知道它是正确的？循环不变量将成为您对第二个问题的答案的一部分。

听起来像这样：在每次迭代的开始和结束时，k=...b....。循环之后，b==0，所以....，所以程序是正确的。

我不想把答案拼出来，因为这可能是家庭作业，只有你自己弄清楚才能学会。