问题标签 [dafny]

下面的函数 seqToSet 接受一个元素序列并返回一个包含给定序列中所有（且仅）元素的集合。它通过调用具有相同序列和空集的递归辅助函数 addSeqToSet 来实现这一点。辅助函数将序列中的每个元素添加到给定的集合中并返回结果。它通过对序列的头/尾结构进行递归来做到这一点。它在序列为空时完成，否则使用序列的尾部以及集合与包含序列头部的单例集合的并集递归调用自身。

Dafny 无法自行验证表明结果集包含原始序列中所有元素的后置条件。

帮助它看到这种情况的正确策略是什么？

这是一个简单的 Dafny 程序：两行代码和三个断言。

S 的基数是 50，但 Dafny 无法验证此声明，如所写。同样，T 显然是 S 的一个子集，而 Dafny 可以验证这一说法；但 T 也是 S 的真子集，Dafny 无法验证这一说法。

导致这些困难的“幕后”发生了什么？学习和使用 Dafny 的人是否可以预见并避免或处理这些困难？

我正在尝试在 dafny 中编写一个程序，以查找给定整数集的所有子集，其乘积是给定数字。

我所做的是实现 ComputeSubProduct、FindProductSets 和 GenerateAllIndexSubsets 方法。

这是我到目前为止得到的：

我在“A”方法中遇到断言违规：

1. 断言 {} == AllIndexSubsets([])
2. 断言 res1 == AllIndexSubsets(q) - AllIndexSubsets(q[1..])

我正在尝试用 Dafny 编写一个程序，这是程序的一部分：

在线var index : nat := q[0]我遇到以下问题：

类型与元素类型 seq 不一致（得到 int）

为什么我会得到这个，我怎么能现在解决它而不是将来再次得到它？

某些在 Dafny 类之外进行验证的代码在封装时无法验证。我想知道（1）为什么，以及（2）如何两全其美：封装/抽象和验证。该代码将“关系”建模为一对：一个域集和域集上的一组对。下面介绍两个版本。第一个验证，第二个没有。

该代码定义了一个有效性条件，该条件要求对集中的对实际上在域上。它定义了一个谓词 isFunction，如果如此建模的“关系”是单值的，则返回 true。这是在一种情况下验证但在另一种情况下不验证的谓词。然后，在 Main 例程中的代码验证 ( dom = {1,2,3,4}, pairs = { (1,1), (2,2), (3,3), (4,4 ) } ) 是单值的（一个函数）。但是，当我将域和对集合封装在一个类中，并将谓词制作成成员函数时，Main 中的相同代码不再验证。

未封装版本：

封装版本（抱歉标识符略有不同）

我编写了一个类，它表示集合 S 上的二元关系，具有两个字段：该集合 S 和从 S 中提取的第二组值对。该类定义了一系列关系属性，例如是单值的（即，是一个函数，在“isFunction()”谓词中定义）。在类定义之后，我尝试定义一些子集类型。一个旨在定义这些关系的子类型，这些关系实际上也是“函数”。它不工作，解码产生的错误代码有点困难。请注意，Valid() 和 isFunction() 谓词确实声明了“读取此内容；”。关于我应该在哪里寻找的任何想法？是不是 Dafny 看不出子集类型有人居住？有没有办法说服它是这样的？

[Dafny VSCode] 尝试见证 null：操作结果可能违反 'binRelOnS' 的子集类型约束

所以我在尝试完成的 Dijkstra 算法的实现中有一个 Vertex 类和 Edge 类。它看起来像这样：

和一个看起来像这样的 Graph 类：

有一堆关于在算法运行中假设的图的谓词。我正在尝试编写一个将顶点作为输入的方法，然后从源中输出该顶点的当前最短路径，该路径存储在 d 中，其中 d 的索引是顶点的“id”。该方法如下所示：

涉及的谓词是：

和

违反了 getVertexwfs() 方法的后置条件，尽管我坚持函数 v 存在于图中的先决条件，并且这意味着 v 的 ID 是 d 范围内的索引。

我是否错过了 Dafny 发现未分配返回整数的情况？

为什么违反前提条件？

任何帮助表示赞赏。

我在 Dafny 中定义了一个多态二元关系类型（一个类）：

实际的声明是：

我想添加一个新的类型约束：类型 S 和 T 应该实现“显示”操作（返回字符串）。

我对 Dafny 参考手册的阅读表明，Dafny 仅支持一些内置类型约束：==，并且显然是 !new，并且没有办法要求该类型支持，例如某些特定的 trait。

也许我错了，比参考手册更新的更新提供了这样的功能。我走运了吗？如果没有，是否有解决方法？

Dafny 对集合交集函数的定义没有问题。

但是当谈到联合时，Dafny 抱怨道，“集合推导必须产生一个有限集合，但 Dafny 的启发式算法无法弄清楚如何为 'x' 产生一组有界值”。A 和 B 是有限的，因此显然联合也是。

是什么解释了这种对初学者来说看似不一致的行为？

这是我要证明的代码：

但我收到一个后置条件错误：

stdin.dfy(13,0)：错误 BP5003：后置条件可能不会在此返回路径上成立。stdin.dfy(12,14)：相关位置：这是可能不成立的后置条件。

如果有任何方法可以证明均匀性的循环版本（while 循环或递归），我将不胜感激！

编辑：从代码中可能并不明显，但我正在寻找关于 n 的归纳证明，至少对于方法案例，dafny 应该能够弄清楚。

我见过一些类似的证明，其中递归函数用于方法函数的循环不变量，只是不知道为什么它不适用于这种特殊情况。

你可以在这里尝试rise4fun上的代码： https ://rise4fun.com/Dafny/wos9