问题标签 [loop-invariant]

我了解到循环不变量应该在循环之前、循环体的开头、循环体的结尾和循环之后为真。如果条件没有副作用，这 4 分可以减少到 2 分：循环之前和循环体结束。这是Java中的一个示例，我在其中检查不变量assert：

我认为不变量表达式的冗余非常糟糕。如果 Java 允许我这样做，则断言可以减少到条件之前的一个断言点。

所以我想出了另一个概念解决方案，并将条件拆分为另一种方法：

我认为可读性很差，并且代码不必要地臃肿。我的解决方案是否可以在不使用第三方库的情况下通过合同不变检查以某种方式实现设计？Java中还有另一种更优雅的方式吗？

我是Z3的初学者。如何在 Z3 中验证具有循环不变量的循环（C 代码）？

例如：

我有一个prob.h这样声明的类：

在A_c A;//A is an object of class A_c我的实现文件的其他地方.cpp，我有以下行：

for(int i = 0; i < A.vec_of_A_s_size(); i++) {...//do loop stuff}

我从我的程序设计中知道A.vec_of_A_s_size()是循环不变的。但是，我真的想避免以下情况（这很麻烦）：

我能否充分且始终如一地依赖一个编译器，即启用了优化 (-O2) 的发布版本不会vec_of_A_s.size()每次都进行评估？

这是我已经尝试过的问题：

(1)（请参阅下面的编辑更新）即使使用调试版本，使用 options -fPIC -fno-strict-aliasing -fexceptions -g -std=c++14，查看反汇编程序输出，vec_of_A_s.size()也只评估一次。但是，编译器会始终如一地可靠地进行这种优化吗？有任何已知的例外吗？我的怀疑和需要保证的部分原因源于下面的问题（2）。

（2）我查看了关于 SO：Performance issue for vector::size() in a loop的相关问题。那里的问题直接评估循环中向量的大小，如下所示：

for(int i = 0; i < vec_of_A_s.size(); i++) {...//do loop stuff}

就我而言，该向量不能直接访问。它是一个私有成员，A_c它的大小只能通过公共成员函数访问A.vec_of_A_s_size()。因此，在 for 循环中必须发生额外的间接/重定向层。该线程上的答案似乎表明编译器确实会优化循环不变量。但是在向量的大小不能直接和公开获得的情况下（如上），编译器会可靠地保证循环不变优化吗？

(3)在关于此类问题的其他相关问题中，一个常见的答案似乎是对程序进行剖析。如果以及当我进行分析时，我究竟应该寻找什么来验证这个特定的优化？该代码是更大的数值分析代码的一部分，这绝对不是当前的瓶颈。然而，很高兴知道如何在分析器中验证这一点。如果这个问题 (3) 太宽泛，我们深表歉意。我对分析比较陌生。但是分析器是否允许分析单个函数，比如包含上述for循环的函数？这样，我可以确定与此功能有关的瓶颈在哪里。

编辑更新：

在 (1) 上，使用所述编译器选项的调试构建优化循环不变量是不正确的。我错了。在更深入的挖掘中，事实证明该函数确实被调用了两次。

给定以下线性搜索算法（将索引 1 称为元素数组中第一个元素的索引）：

我想知道这个循环不变量是否正确：“在 for 循环的每次迭代开始时，found_idx 是数组中以 i-1 结尾的索引，如果该值存在，则该值存在”

这是我根据 CLRS 中的格式对这个循环不变量提出的非正式解释：

1. 初始化：在第一次迭代之前是这样，因为 i = 1 并且以 i-1 结尾的数组为空，因此 found_idx 为 nil。
2. 维护：在每次迭代之后都是如此，因为在 的每个值处i，A[i]都会检查然后 i递增，这意味着i-1在每次新迭代之前已经检查了所有元素。
3. Termination：这在 时终止i > A.length，这意味着所有元素A.length都已被检查。

我主要担心的是引用结束于的索引感觉不正确，i-1因为循环从i1 开始，这是数组的第一个元素。换句话说，引用数组的子数组感觉是错误的，其中子数组以小于数组的起始索引的索引结束，子数组首先应该是子数组。这似乎意味着上面给出的循环不变量在循环的第一次迭代之前实际上是错误的。

想法？

我对算法很陌生，虽然我理解它非常简单的代码，但我发现很难在下面的代码中找到循环不变量。有人可以明确告诉我以下代码的良好循环不变量是什么。任何帮助深表感谢

除了 sum 等于从 x 到 y 的所有整数之外，我想不出任何循环不变量，但在第一次迭代之前这是不正确的。是否存在覆盖后置条件的循环不变量？

我不知道如何找到循环不变量。我不知道从哪里开始。谁能找到给定程序的循环不变量并解释你的方法。

从下面的代码中，我需要推断/选择一个循环不变量。

给出的解决方案是

• s = (x-1)*x/2 ∧ (x ≤ n +1)

我不太明白它是如何达到上述解决方案的。

请帮助我了解如何从代码中得出这样的解决方案或其他循环不变量。

假设您有一个函数可以返回两个数组之间的长度差，但是，它不是使用常规方法来查找长度，而是使用递归函数。
你能帮我找到一个循环不变量吗？我理解循环不变量是在条件之前和条件之后必须为真的东西。但是，我真的无法理解它。这是代码：

第一个调用是 func(arr1.length, arr2.length);

冒泡排序算法（伪代码）：

我不确定，但我的证明似乎有效，但过于复杂。你能帮我清理一下吗？

循环不变：在每次迭代 i 之后，A 的 i - n + 1 个最大元素处于它们应该是 A 非降序排序的位置。在数组 A 包含多个最大值的情况下，令最大元素为所有可能最大值中索引最小的元素。

归纳法（i = n）：内部循环遍历 A 的每个元素。最终，j 指向最大的元素。这个值将被交换，直到它到达位置 i = n，这是数组 A 中的最高位置，因此是 A 中最大元素的最终位置。

归纳步骤：（i = m -> i = m - 1 for all m > 3）：内部循环遍历 A 的每个元素。最终，j 指向尚未排序的最大元素。这个值将被交换，直到它到达位置 i = m - 1，这是数组 A 中尚未排序的位置的最高位置，因此是 A 中最大的尚未排序元素的最终位置。

算法执行完毕后，位置1的剩余元素也处于其最终位置，因为如果不是，其右侧的元素将不会处于其最终位置，这是矛盾的。量子点

Godbolt 链接：https ://godbolt.org/g/Hv6MAL

期望编译器将上述代码优化为类似于以下内容的感觉是很自然的：

但是由 gcc 8.2 生成的带有-O3 -m32as 标志的程序集是：

为什么编译器不将subarrayandsubsubarray计算移到内部循环之外？

随机volatile会变魔术

我随机添加volatile以防止 DCE 摆脱所有代码，然后以某种方式将循环不变量从内部循环中提升出来。

这主要不是因为y它是一个局部变量，因为 usingstd::cout << subsubarray[k];阻止了优化。

gcc 8.2-O3 -m32为上述代码生成的带有 as 标志的程序集是：

循环不变量被推出内部循环。randomvolatile做了什么来让 GCC 优化不变量？clang 6.0.0时不会发生优化。