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

Question

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

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

   return q;
}

Answer 1

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

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

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

a == a0 - (b * q)

通过观察每次 q 增加，a 也减少 b，您得出了这个不变量。因此，a0 在循环的每次迭代中正好减少 b q 次。

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