问题标签 [dafny]

我想在该方法中做的只是覆盖前一个数组并用排序的数字填充它，但是 dafny 说后置条件不成立，我终生无法弄清楚原因。我猜我需要在循环中添加一些不变量，但是由于在进入循环之前检查了它们，所以我不知道如何放置有效的不变量。

我之前的尝试只是重新初始化 a 但 dafny 显然不允许内部方法。

此Q3方法通过将 m0 添加到 res |n0| 来对 n0 * m0 进行通勤。次。如果 n0 为负数，我们将 n0 和 m0 反转，因为 n0*m0 = -n0* -m0 成立。

我遇到的问题是我不完全知道我的不变量应该是什么样子，因为不变量需要是布尔类型。谁能告诉我不变的布尔条件可能是什么样的？我想了想Abs((n0)-n)*m == res，但这行不通。

如果每次迭代后我的索引都不会减少，我如何避免减少错误？为什么我在一个对象和一个数组上得到一个修改子句，而我对它们使用修改子句？

我也在 Dafny 中上传了此代码，您可以在其中再次编译它：https ://rise4fun.com/Dafny/bYDH 。如您所见，由于其他修改违规问题，我修改了数组 m_owner 并将 ownerIndex 外包给另一个对象。但是在这里，dafnys 的语言似乎是有限的，不是吗？

如何在方法中覆盖标记为已修改的数组？或者在 Dafny 中有没有办法将数组的长度增加一倍？

正如您在这段代码中看到的那样。我试图在方法extendArrayByOne 中将数组的长度增加一。之后，我在方法 confirmAndCheck 中添加从 extendArrayByOne 返回的新数组末尾的元素操作。这是官方编译器的链接，可以编译此代码： https ://rise4fun.com/Dafny/WtjA

这是我之前关于extendArrayByOne的问题的链接：

修改已更改对象的子句错误

根据Automating Induction with a SMT Solver，以下内容应适用于 Dafny：

但 Dafny 拒绝它（至少在我的桌面和 Dafny 在线）。也许有些东西改变了。

问题：

Q1。为什么？

Q2。真的需要对 j 或 i 和 j 进行归纳吗？我认为对 seq 长度的归纳应该足够了。

无论如何，我对以下内容更感兴趣：我想通过手动归纳来证明这一点，以供学习。在纸上，我认为对 seq 长度的归纳就足够了。现在我试图在 Dafny 上这样做：

我坚持最后一个案例。我不知道如何将计算证明风格（如基本案例中的风格）与归纳炒作结合起来。

也许是棘手的暗示。在纸上（“非正式”证明），当我们需要p(n) ==> q(n)通过归纳证明一个蕴涵时，我们有类似的东西：

炒作： p(k-1) ==> q(k-1)

特西斯：p(k) ==> q(k)

但这证明：

(p(k-1) ==> q(k-1) && p(k)) ==> q(k)

Q3。我的方法有意义吗？我们如何在 dafny 中进行这种归纳？

因此，作为本科项目的一部分，我试图直接根据 CLRS 算法书中算法的描述，在 Dafny 中实现 Dijkstra 的单源最短路径算法。作为实现的一部分，我定义了一个“Vertex”对象，其中包含两个字段，分别表示来自源的最短路径和前一个顶点的当前长度：

以及包含“顶点”-es 数组的“图形”对象：

我正在尝试使用“图形”对象中的谓词来声明顶点数组的每个“顶点”中字段的一些属性：

据我了解，Dafny 中的“读取”和“修改”子句仅适用于一层，我必须向 Dafny 指定我将读取顶点数组中的每个条目（读取 this.vertices[x] ）。我尝试使用“forall”子句来做到这一点：

但这似乎不是 Dafny 的功能。有谁知道是否有办法在“读取”子句中使用量词，或者告诉 Dafny 读取包含对象的数组的每个条目中的字段？

谢谢您的帮助。

我知道一个 Dafny 源文件可以包含在另一个文件中，从而在验证之前导致文件的文本连接。但是对于包含、导入以及何时验证哪些文件之间的关系，我没有清晰的心智模型。也许专家可以详细说明。谢谢。

Dafny 中的实数是多少。它们是否表示为 IEEE 754-2008 浮点数？如果不是，那么它们是什么？即，Dafny 中真实类型的规范是什么？

我通过了一个有限的地图，米。有没有办法计算它的域？m.Domain、dom(m) 之类的东西。参考手册并没有说有这样的功能。

在 Dafny 中迭代有限集对象的元素的最佳方法是什么？一个工作代码的例子会很有趣。