java - 如何找到循环不变的java

Question

我试图找到循环的不变量（例如在下面的代码中）我真的不知道如何找到一般的不变量。任何人都可以帮助我如何找到一个不变量，并帮助我找到它的以下代码？谢谢

public static int div(int a, int b)
{
   int q = 0;
   while(a >= b)
   {
      a -= b;
      q++;
   }

   return q;
}

score 4 · Accepted Answer

关于循环不变量，首先要注意的是它们有很多。其中一些更有用，而另一些则不太有用。由于不变量用于证明程序的正确性，因此选择不变量取决于您要证明的内容。

例如，q >= 0是循环的不变量。如果你想证明函数返回一个正数，这就是你所需要的。如果你想证明更复杂的东西，你需要一个不同的不变量。

由于 Java 中的参数是按值传递的，而且由于程序会修改参数的值，所以a我们用a0来表示参数的初始值a。现在您可以编写以下不变量表达式：

a == a0 - (b * q)

您通过观察每次q增加，a也减少了来得出这个不变量b。在循环的每次迭代中， Soa0减少了b精确q的次数。

这个不变量可以用来证明循环产生q == a0 / b，并且的结束值a等于a0 % b。

score 1 · Accepted Answer

循环不变量是对循环的每次迭代都成立的某些条件。

在您的循环中，谓词q >= 0是循环不变量，因为它始终为真。分析循环不变量的需要是，当你退出循环时，循环不变量和循环终止条件都可以得到保证。因此，在您退出循环时，我们可以确定q >= 0and a < b。

score 0 · Accepted Answer

循环不变量是对循环的每次迭代都成立的某些条件。

在您的情况下，一个不变量是：

q >= 0

3 回答 3