如何找到循环不变的java答案

【问题标题】：how to find loop invariant java如何找到循环不变的java
【发布时间】：2013-06-05 04:25:25
【问题描述】：

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

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

   return q;
}

【问题讨论】：

家庭作业？搜索这个网站，关于什么是循环不变量有很多解释。一个例子：stackoverflow.com/questions/3221577/what-is-a-loop-invariant
这可能对你有帮助，对我也有帮助。 stackoverflow.com/questions/2935295/…

【解决方案1】：

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

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

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

a == a0 - (b * q)

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

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

【讨论】：

非常感谢，我现在很清楚了。 a0 的表达式正是我想要的。我不明白的是，为什么我们确实用“a”而不是“b”编写了一个函数。
@NavidKoochooloo 通过将表达式的一部分移动到== 的不同侧，有很多方法可以编写相同的不变量。例如，您可以将其写为(b*q) == (a0-a)，但这是完全相同的表达式。
提取表达式有点困难，不看你的表达，我想了很多，但无法达到这样的表达，也不知道我应该使用“a0”例如： /无论如何谢谢:)你解释的真的很有帮助

【解决方案2】：

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

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

【讨论】：

【解决方案3】：

循环不变量是对于循环的每次迭代都保持 true 的条件。

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

q >= 0

【讨论】：