问题标签 [loop-invariant]

我正在研究如何使用 dafny 来验证使用“交换”相邻元素的插入排序，但我找不到 while 循环的合理不变量，谁能帮我修复它？这是链接：http ://rise4fun.com/Dafny/wmYME

我有一个函数sum，它接受两个数组a并b作为输入并b修改b[i] = a[0] + a[1] + ... + a[i]. 我写了这个函数，想用 Dafny 验证它。但是，Dafny 告诉我，循环可能不会维护我的循环不变量。这是代码：

我该如何解决这个错误？

前置条件：len(list) >= 2 的整数列表

后置条件：返回第二小的值。如果列表中存在两个最小值，则返回最小值。

非常感谢。

这是一个用Dafny编写的简单排序算法：

代码没有错误。但是，如果我从forall m,n | 0 <= m < j < n <= i :: a[m] <= a[n]内部循环中删除不变量，Dafny 会告诉我循环sorted(a,j,i+1)可能不会维护不变量。

1. 这是为什么？

2. 怎么能猜到一 forall m,n | 0 <= m < j < n <= i :: a[m] <= a[n] 开始就需要不变量呢？

   我试图在纸上证明这个程序，但是在构造内部循环的不变量时我不需要这个不变量。

在函数执行过程中必须满足哪些条件？（断言）

我想确保我的断言能够在运行第 i 个循环后描述我所知道的真实情况。

这只是一个迭代线性搜索函数，如果找到目标，则返回目标的索引，否则返回 -1。

考虑解决100 名囚犯和一个灯泡问题的标准策略。这是我在 Dafny 中对其建模的尝试：

然而，它最终无法证明这一点I == P。为什么？我可能需要进一步加强循环不变量，但无法想象从哪里开始......

错误是：

ValueError：while_12/Merge:0 的形状不是循环的不变量。它以形状 (1, 6) 进入循环，但在一次迭代后具有形状 (?, ?)。shape_invariants在循环变量上使用 tf.while_loop 或 set_shape()的参数提供形状不 变量。

似乎变数

contigs_index

是负责任的，但我真的不知道为什么！我展开循环执行每个语句，但找不到任何形状不匹配！

我开始学习 Dafny，我刚刚学习了不变量。我有这个代码：

给定的错误如下：“这个循环不变量可能不会被循环维护。” 我想我可能需要另一个不变量，但我认为我的代码除此之外是正确的（我猜）。任何帮助表示赞赏。提前致谢。

我有我的测试代码（用于研究 WP 循环不变量），它在数组单元格中添加了两个长整数，每个数字的表示形式：

我只想指定最后一个循环不变量。我已经用 \at(a[i], LoopCurrent) 尝试了一些 ACSL 代码。我收到未知状态或超时。最后，我完成了一个公理递归解决方案，但没有任何成功。

我现在不知道我还应该尝试什么来验证这一点。帮助？

更新：为实际计算创建了一个函数。改进的公理。仍然有超时状态。使用来自 opam 的 Frama-C 最新版本以默认设置运行（超时 = 10，证明者 Alt-Ergo）。

我目前正在阅读 TCRC Introduction to Algorithms 3rd edition 教科书的第 2 章，并且正在阅读作者对该算法的循环不变量的解释。我理解作者的初始化和维护逻辑。然而，终止是我有点陷入困境的。作者声称在终止时，j = n + 1。然而，在算法的伪代码中，j 从 2 循环到 n。所以不应该 j = n - 1 吗？

编辑：这本书的插入排序伪代码是：

编辑：仔细阅读后，我终于明白了为什么 j = n + 1 在终止期间。这是因为 for 循环从 2 变为 n（包括），所以在 j 超过 n 之后，循环终止，因此在终止时 j = n + 1。我很感激帮助。