问题标签 [dafny]

在尝试验证由数组支持的通用 FIFO 队列时，我遇到了一个令人困惑的错误。该队列是在这篇论文中找到的，由 Dafny 的创建者撰写。

有问题的错误是：

除非为数组元素提供了初始化程序，否则新的“数据”数组必须为空大小

new Data[whatever]这与在构造函数和 enqueue 方法中分配数组的两条线有关。

Dafny 版本：Dafny 2.0.0.00922 技术预览版 0

完整代码供参考。

我一直在建模任务中使用抽象引理和函数（没有主体）。在这个例子中，

在 main 中调用 py 可确保后置条件为真，而不管 py 是如何实现的。我有两个问题：

1. 在 Dafny 中使用抽象引理/函数是否安全？对上述代码的以下修改由 Dafny 验证：

   虽然我认为这可能是 Dafny 应该抛出一个错误。

2. 我应该说lemma {:axiom} py(...)吗？我没有观察到包括{:axiom}or的区别{:imported}。

在进行基本线性搜索时，我的 Valid() 谓词出现错误。它似乎仅在我取消注释构造函数和数据方法上的附加确保语句时才有效。也就是说，当我对内容非常明确时。

当找不到该项目时，我的搜索后置条件也有问题。

关于如何解决这些问题的任何建议？

我正在尝试验证一个哈希集，但我的插入方法遇到了问题。

我不明白为什么我在取消注释 main 中的插入时收到“调用可能违反上下文的修改子句”错误。我相信这与使用新鲜有关，但我不清楚如何/在哪里这样做。

代码可在以下网址找到：https ://rise4fun.com/Dafny/9UDG

在这段代码中

https://rise4fun.com/Dafny/DmBh

断言 forall x:: x in multisetOfTree(t.right) ==> t.root <= x;

在第 36 行没有证明，但是它是不变量的一部分。实际上，您可以取消注释第 31 行中的不变量并注释第 36 行并且它可以工作。

所以我试图从一组集合中获取所有元素，但出现错误：

“集合理解必须产生一个有限集合，但 Dafny 的启发式无法弄清楚如何为 'x' 产生一组有界值”

我认为这可能与您无法获得集合的基数有关。

感谢所有帮助。

我如何声明（在 Dafny 中）“确保”保证方法返回的对象将是“新的”，即与其他任何地方使用的对象不同（还）？

以下代码显示了一个最小示例：

“ dowork ”函数编译（和验证）正确，但另一个没有，因为 Dafny 编译器无法知道“ newArray ”函数返回的对象是新的，即不需要在“ doesnotwork ”函数的“require”语句，以便该函数满足它只修改“ this ”的要求。在“ doswork ”函数中，我只是简单地插入了“ newArray ”函数的定义，然后它就可以工作了。

您可以在https://rise4fun.com/Dafny/hHWwr下找到上面的示例，它也可以在线运行。

谢谢！

我正在尝试学习 dafny，但遇到了一个我不明白的问题。我需要检查用户是否存在于数组中，并且我想为此使用谓词。我有一组用户，每个用户都有一个 ID。所以我想检查属于 User 类的 id。

我收到这个错误Test.dfy(57,24): Error: member id does not exist in array type array

其他一切都很好（我认为）。

那么当我有一个对象数组（用户）时，如何读取/访问谓词中另一个类的成员？

谢谢您的帮助。`

我在 Dafny 中遇到了这种简单方法的问题，我不知道为什么它不起作用。由于没有调试器，而且我是这种语言的新手，我希望有人能提供帮助。我认为规范不完整..

当我在 microsoft dafny 编译器中运行它时，我得到以下信息：

后置条件可能不会在此返回路径上成立。（第 8 行）这是可能不成立的后置条件。（第 2 行）

我正在尝试覆盖方法内的数组。编译器给我错误“错误：赋值的 LHS 必须表示一个可变变量”。

我是在盯着自己瞎看，错过了什么，还是达夫尼不允许这样做？