问题标签 [dafny]

我正在尝试使用 Dafny 来验证一些非常简单的代码。第一块是普通版本。而且我只是找不到将后置条件设置为的方法

“存在我forall j ~~~~~~”

我不知道如何在 Dafny 中一起使用 2 个量词，请帮助。谢谢。

我目前正在学习达夫尼。我完全被引理弄糊涂了，我不知道如何使用它。该教程没有那么有用。如果我想证明 count(a) <= |a| 我应该怎么做。感谢您的帮助。

我的问题是关于 Boogie，但由于没有可用的 Boogie 标签，我使用 dafny 标签作为与 Boogie 密切相关的标签。

我按照文档中的说明在 Visual Studio 上构建了 Boogie。接下来我应该做什么来编写 Boogie 代码或等效地如何运行 Test 文件夹中的 .bpl 文件？据我了解，Boogie 虽然是一种中间验证语言，但也可以独立使用。

谢谢你。

I followed the instructions in the documentation to install Dafny on Linux, but when I use xbuild dafny/Source/Dafny.sln I get the following trace:

I used the 64-bit version of Linux Mint 18.1. I get the same error in other Linux distributions as well (Fedora and Ubuntu).

The previous step (xbuild Source/Boogie.sln works fine)

Any help would be appreciated.

Thanks.

我正在与 Boogie 合作，我遇到了一些我不理解的行为。

我一直在用assert(false)它来检查前面的assume陈述是否荒谬。

例如在以下情况下，程序被验证没有错误......

......这t1 == t2 && t1 != t2是一个荒谬的说法。

另一方面，如果我有类似的东西

唯一在assert(false)注释行未注释时失败。为什么评论断言改变了结果assert(false)？

教程集合包含以下代码

但是，目前无法在rise4fun 提供的Dafny 系统中进行验证：

这个更简单的例子

也不验证：

我认为这两个例子都应该验证；我错过了什么吗？

LetRectangle和PairBe Dafny 数据类型定义如下：

这个矩形的一个数学抽象/表示，我想用 Dafny 编码，是这个矩形包含的所有点 (i,j) 的集合。例如矩形 rect(pos:(5,5), width=2, height=3) 表示点的集合：{(5,5), (6,5), (7,5), (5, 6), (6,6), (7,6)}

假设abs是一个函数方法（单行方法），它以 a 的形式返回这个抽象set<Pair>，给定一个类型的变量Rectangle

有谁知道如何在 Dafny 中用一行来表达这个集合？

我很难摆脱 Dafny 程序中的最后一个错误。有人可以指出我正确的方向吗？这是代码：http ://rise4fun.com/Dafny/2FPo

我收到此错误：赋值可能会更新不在封闭上下文的修改子句中的数组元素

我尝试在合并方法中添加修改矩形（即使我很确定它已经包含在修改此中）但这只会在合并方法调用中产生类似的错误。

我真的迷失了这个。谢谢您的帮助

我想知道为什么 Dafny 需要http://rise4fun.com/Dafny/8sl7中的注释提示 来验证断言？
有人可以解释一下吗？

这是dafny代码，第二个断言永远不会通过，任何人都可以帮助我吗？在此处输入链接描述