问题标签 [loop-invariant]

第 1 部分
我知道 QuickSort 可以“就地”使用，但有人可以向我解释插入排序算法如何使用“就地”来做到这一点。

据我了解：

插入排序从第一个值开始并将其与下一个值进行比较，如果该值小于我们的值，它们会切换位置。我们递归地继续这个。（简短说明）

所以你会说这是“就地”，因为我们没有创建一个新数组来执行此操作，而只是比较数组中的两个元素？

如果我的理解是错误的，有人可以解释一下插入排序的算法。

第 2 部分
另外，我将如何使用插入排序来说明循环不变量的概念？

我知道循环不变量是在循环的每次迭代之前和之后立即为真的条件，但我不确定这与插入排序有何关系。

数组包含首先增加值然后减少值的整数。目前尚不清楚数字何时开始减少。编写高效的代码将第一个数组中的数字复制到另一个数组，以便第二个数组按升序排序。

代码如下：

这里的循环不变量是什么？

我正在学习循环不变量，我一直在用越来越难的问题挑战自己。今天我解决了一个问题，但我不确定我的解决方案是否正确。任何人都可以验证我的答案，并请解释而不是仅仅给出解决方案吗？

代码：

循环不变量：c.size() == i

问题：

简要解释谓词c.size()==i是否是循环不变量。如果它是循环不变量，请解释是否足以验证该方法在其规范方面是部分正确的。如果谓词不是循环不变量，或者不足以验证方法 pairwiseMin 的部分正确性，则定义一个循环不变量，可用于显示该方法部分正确。

我的解决方案：

是的，它是循环不变量，因为在执行循环之前和之后满足前置条件后置条件。

第一次迭代：

检查 c.size()

因此，证明部分正确性就足够了。

因此，如果我有以下代码：

我现在必须找到一个循环不变量。有人告诉我，对于这样的循环，Y = i^2 的不变量被认为是循环不变量，但是我不知道我是否知道如何证明它是循环不变量。因为 Y 只是某物，所以在循环之前、期间和之后它总是正确的，因为它是 i*i 是什么......这是它是不变量的有效证明吗？

此外，在用不变量证明算法时，是否正确说 sum = i*i 的从 1 到 n 的总和（或 Y，循环不变量）= n(n+1)(2n+1 )/6

然后用归纳法证明那是正确的？是否正确使用循环不变量来证明算法？

希望得到一些帮助:)

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

这个证明在 Dafnys 的验证器中给出了一个无限循环：

这指向某种不确定性问题还是它？有没有更好的方法来呈现这个问题以避免无限循环？

以前的版本：

我决定使用 g++ 检查循环不变代码运动优化的结果。但是，当我编译下面的代码-fmove-loop-invariants并分析它的程序集时，我看到k + 17计算仍然在循环体中执行。

什么会阻止编译器对其进行优化？

可能是编译器得出的结论是重新计算更有效k + 17？

尝试过g++ -O0 -fmove-loop-invariants，g++ -O3并g++ -O3 -fmove-loop-invariants同时使用 g++ 4.6.3 和 g++ 4.8.3。

这是数组中线性搜索的伪代码，如果找到数组中i的所需元素，则返回索引，否则（来自 CLRS 书，第 3 版，练习 2.1-3）：eANIL

我试图从中推断出一个不变量的循环，所以根据我的理解，我认为一个由以下事实表示，即在循环中的任何给定时刻子数组A[1..i-1]仅包含相等性测试证明为假的值。

具体来说，在第一次迭代之前，i-1 == 0这意味着子数组的长度为空，因此不能存在v属于它的元素，使得v == e. 在任何下一次迭代之前，作为等式测试也是退出条件，假定的不变属性必须仍然成立，否则循环将已经结束。在终止时，要么是函数即将返回一个索引（在这种情况下，循环不变量是平凡的），要么是返回 NIL（在这种情况下i == A.length + 1，所以循环不变量对任何1 < j < i）。

以上是正确的吗？如果不是，您能否提供一个正确的循环不变量？

感谢您的关注。

为了证明这个有效三元组的有效性：

什么是循环不变量？

Eiffel 中的循环遵循以下格式：

您如何将上述 Eiffel 伪代码翻译成不支持循环不变量/变量的语言？让我们假设这样的目标语言有一个assert检查不变量/变量的指令。