问题标签 [loop-invariant]

Hi我看到了一个计算数字不同素数的在线答案，它看起来不是最优的。所以我试图改进它，但在一个简单的基准测试中，我的变体比原来的要慢得多。

该算法计算一个数字的不同质因数。原始使用 HashSet 来收集因子，然后使用 size 来获取它们的数量。我的“改进”版本使用一个 int 计数器，并将 while 循环分解为 if/while 以避免不必要的调用。

更新：tl/dr（有关详细信息，请参阅接受的答案）

原始代码有一个性能错误调用 Math.sqrt 编译器修复了不必要的：

编译器优化了 sqrt 调用，使其仅在 n 更改时发生。但是通过使循环内容更复杂一些（虽然没有功能变化），编译器停止了优化，并且在每次迭代时都会调用 sqrt。

原始问题

原始版本的输出始终在 10 秒左右（在 java8 上），而“优化”版本接近 20 秒（都打印相同的结果）。实际上，只需将单个 while 循环更改为包含 while 循环的 if 块，就已经将原始方法的速度减慢了一半。

使用-Xint解释模式运行JVM，优化后的版本运行速度提高了3倍。Using-Xcomp使两个实现以相似的速度运行。因此，与具有简单 int 计数器的版本相比，JIT 似乎可以使用单个 while 循环和 HashSet 优化版本。

一个适当的微基准测试（如何在 Java 中编写一个正确的微基准测试？）会告诉我其他信息吗？有没有我忽略的性能优化原则（例如Java 性能提示）？

我试图证明一种方法的正确性，该方法确定大小序列是否n是. 我设法证明，只要方法返回，那么序列确实是有效的排列。尽管如此，证明相反的情况要困难得多（对我来说）。我认为我有正确的循环不变量和触发器，但是 Dafny 触发了一个我无法理解的断言错误。这是永久链接，这是完整的代码：0,1,...,n-1true

可能这是一个非常简单的解决方案，我只是愚蠢，但我找不到这个 while 循环的不变量。为了证明 (a+b) <= 2x，你可以取 (x+y>a+b)，所以这可能是不变量的第一部分，但对于第二部分，为了证明 2x<= (a+b +1）......你到底在做什么？我尝试了一切，但为此浪费了两个小时。

我觉得它应该很明显，我只是看不到它。

我理解关于证明部分正确性的理论。我只是找不到循环不变量，所以不变量将不胜感激，无需解释理论。

证明下列程序的部分正确性

我们知道不变量是表达式，在循环之前、每次迭代中和循环之后都是如此。所以我们应该找出下面的方阵螺旋遍历代码的所有不变量，从它的中心开始。

循环探索：

整个C++程序：

程序的输出和内部结构： 图片在这里

我向老师展示了我的想法 - 不变量是：

1. 我 < N+1
2. h < N
3. v < N

老师告诉我，它不是不变量。它应该是表达式，包含iInd和jInd。

我想为下面的一段代码找到一个循环不变量，我似乎无法弄清楚这段代码中呈现的任何类型的关系。

该算法的目标是找到二叉树中所有元素的总和。它将节点存储在一个名为 的堆栈中s。

我注意到这res是所有当前节点的父节点及其父节点左侧的总和，但我不知道如何将其表述为循环不变量。

Leetcode 描述

给定一个长度为的字符串n，您必须确定该字符串是否为回文，但您最多可以删除一个字符。

例如：“aba”是回文。
"abca" 也是有效的，因为我们可以删除 "b" 或 "c" 以获得回文。

我见过许多采用以下方法的解决方案。

用两个指针left分别right初始化为字符串的开始和结束字符，只要和所指向的两个字符相等，就保持同步递增和left递减。rightleftright

当我们第一次遇到 and 所指向的字符之间的不匹配时left，right并说这些是专门的索引iand j，我们只是检查string[i..j-1]or是否string[i+1..j]是回文。

我清楚地知道为什么会这样，但让我困扰的一件事是当我们第一次看到不匹配时我们采取的方法的方向。

假设我们不关心时间效率，只关注正确性，我看不出是什么阻止我们尝试删除一个字符，string[0..i-1]或者string[j+1..n-1]尝试查看整个结果字符串是否会变成回文？更具体地说，如果我们采用第一种方法并
看到两者都不是回文，那么是什么阻止我们回溯到我描述的第二种方法，看看是否删除一个字符或会产生一个回文？string[i..j-1]string[i+1..j]string[0..i-1]string[j+1..n-1]

我们能否在数学上证明为什么这种方法无用或根本不正确？

这是我的二分搜索实现，如果 x 在 arr[0:N-1] 中则返回 true，如果 x 不在 arr[0:N-1] 中则返回 false。
而且我想知道如何找出正确的循环不变量来证明这个实现是正确的。
我怎么解决这个问题？
非常感谢 :D

以下是我的算法和数据结构课程中的一个练习，旨在教授一些关于使用循环不变量分析算法的知识。

设置如下；我们有一个装有n 个弹珠的罐子。大理石要么是红色的，要么是蓝色的。我们还有无数的红色弹珠。我们的目标是通过使用这个算法来清空罐子

算法如下：

1）争辩说，在算法结束时，我们在罐子里留下了 1 个弹珠。我的想法是说我们有一个如下的循环不变式

在 while 循环的迭代开始时，还剩下 n-(ni) 个弹珠

然后证明在初始化、维护和终止期间不变量是正确的，但是我不确定我应该如何处理这个问题，有人可以帮忙吗？

例如，在初始化时，很明显循环不变量是因为我们在 jar 中有n 个弹珠，因此n-0 = n来自不变量，但是我应该如何处理其余的？

由于我正在使用 Frama-C 进行 C 形式验证的第一步，我正在尝试正式验证一个整数二进制对数函数，如下所示：

我正在使用带有命令的 Frama-C 20.0 (Calcium) frama-c-gui -rte -wp file.c（由于某种原因我没有 Jessie 插件）。我已经检查了后置条件以保持最多 n = 100,000,000（使用标准库断言），但是尽管我尽了最大努力，但此函数无法正式验证，并且 Frama-C 教程通常涉及递减的琐碎循环变体（而不是减半）每次迭代，因此与我想要做的不太接近。

我尝试了以下代码注释，其中一些可能是不必要的：

无法验证的注释是循环不变量 2 和 5（Alt-Ergo 2.3.0 和 Z3 4.8.7 都超时）。就不变量 2 而言，难度似乎与整数除法有关，但我不确定要添加什么以使 WP 能够证明它。至于不变量5，WP可以证明它成立，但不能证明它被保留。它可能需要一个能够捕获当 n 变为 1 时发生的情况的属性，但我不确定什么会起作用。

我如何指定缺少的信息来验证这些循环不变量，是否还有另一个 Frama-C 分析可以让我更轻松地找到循环不变量？

谢谢您的考虑。

这是数组问题中一个简单的分隔 0 和 1 的问题。我无法理解为什么循环不变量不成立。