问题标签 [dafny]

我想在多个程序中重用相同的 Dafny 代码。是否可以将一个 Dafny 文件包含在另一个文件中？该手册没有描述任何方法。

我正在尝试在 Dafny 中实现选择排序。

我的sorted和FindMin函数确实有效，但selectionsort它本身包含了 Dafny 不会证明的断言，即使它们是正确的。

这是我的程序：

为什么这是错误的？“后条件可能不成立”是什么意思？达夫尼能举个反例吗？

我有以下 zaMap（在此处查看完整代码：http ://rise4fun.com/Dafny/LCaM ）：

现在我想为该put方法添加更多规范。例如，我想ensure，如果返回值为success == true，则映射!full()在函数调用之前，或者等效地，如果映射不是full()，则保证put存在。

问题是，在前置条件“需要”中我还不知道它会返回什么，而在后置条件中“确保”我不再有原始地图。人们对此怎么办？

i am new in Dafny and i have problems verifying my insertionSort-implementation. Dafny tells me the the multiset invariants are not holding, anything else is working fine. After Hours of searching the mistake i could need some help :) Would be nice if somebody could tell me the trick!

My Code:

It produces

Link: http://rise4fun.com/Dafny/3R5

我正在研究经过验证的高斯消除实现，并且在验证这种将数组 b 的内容添加到数组 a 的内容的超级简单方法时遇到问题。这是代码。

就像标题说的那样，我想调用一个方法来修改另一个方法的 if 语句中的一些变量，例如：

这不起作用，因为 Dafny 不允许以这种方式调用非幽灵方法。这个问题的解决方法是什么？

我正在对在考虑到验证的情况下创建的几种语言（Whiley、Dafny 和 Frama-C 等）进行语言比较大批。我想出的规范在 Dafny 中是这样的：

在上面的第二个 while 循环中，可能有一些不需要的不变量，因为我试图涵盖我能想到的所有内容。但是，是的，这并不能验证，我很困惑为什么......

我尝试在 dafny 中编写一个递归求和函数并证明其正确性。我已经写了：

这是我写的证明：

总和1：

总和2：

我得到的错误：

请帮我理解为什么？

我遇到的问题是两个不同类中的两种不同方法不合作，设置如下：

一个主要的称它们如下：

为什么方法d不承认方法b确保了它的前提条件？如果这是对 Dafny 证明者的限制，我将如何解决这个问题？

编辑： 当我创建这个例子时弄乱了语法，所以测试程序可以工作。然而，真正的仍然有问题。我正在努力解决的具体课程如下所述：

主要它被称为如下：

我在下面的链接中为代码编写了以下证明。我想在证明 count2 方法方面获得一些帮助。交替证明对我来说不是很清楚，谢谢

http://rise4fun.com/Dafny/ueBY