问题标签 [dafny]

哪些版本的 Visual Studio 可以支持 Dafny 1.9.7 IDE 插件？

特别是我对 VS 2015 社区版很感兴趣，因为我希望我的学生能够免费使用它。

一个非常简单的乘法代码：

当我用 dafny 验证它时，它说：

我明白它在某些条件下会说 res != m*n，但我无法弄清楚。

一个非常简单的乘法代码：

当我用 dafny 验证它时，它说：

我明白它在某些条件下会说 res != m*n，但我无法弄清楚。

我正在尝试使用 Dafny 证明以下程序的正确性/不正确性。

Dafny 成功地证明了断言是不正确的。然而，它没有给出断言失败的例子。Dafny 可以自己举一个这样的例子吗？

当我验证以下程序片段时，其中有一个错误，

我从 BVD 得到以下结果，我不明白。

令我困惑的是，第二个不变量似乎在生成反例时被忽略了。如果两个不变量是 I0 和 I1 并且保护是 G，那么验证条件肯定是 I0 && I1 && !G ==> qy > x 并且反例应该满足这个否定。我误解了什么？

为了方便任何想要它的人，下面复制了代码。

对于正确的方法，Z3能否找到该方法验证条件的模型？

我没想到，但这是一个方法正确的例子

然而验证找到了一个模型。

这是 Dafny 1.9.7。

这是一个例子，它接受一个整数lim并返回一个严格小于lim偶数的所有整数的序列。

只有第二个不变量中的向后方向... <==> ...不验证。我已经尝试过一段时间了，但我无法弄清楚。

任何帮助深表感谢！

我正在尝试编写子字符串方法的简单验证实现。我的方法接受 2 个字符串并检查 str2 是否在 str1 中。我首先试图弄清楚为什么我的不变量不成立 - Dafny 标记该不变量可能在输入时不成立，而我的前置/后置条件失败。我对不变量的想法是有 3 个主要场景： 1. 循环未能找到索引 i 处的子字符串，并且有更多索引要探索 2. 循环未能找到索引 i 处的子字符串 - 没有更多索引可探索 3 . 循环在索引 i 处找到子字符串

代码：

链接：http ://rise4fun.com/Dafny/QaAbU 任何帮助将不胜感激。

我正在尝试在 Dafny 中验证我的代码，但遇到了一个问题：我有一个方法正在迭代一个序列并对其进行更改。该方法根据序列中的元素改变序列。我想添加这样的后置条件：“如果序列中的元素是 X，那么应该发生一些事情”。问题是该方法更改了集合（添加元素等），我想检查原始序列的条件。在 Dafny 中是否有一种优雅的方式来做到这一点？（我现在能想到的唯一方法是保持序列原始条件的全局变量，但我正在寻找正确的方法）。

代码示例：

在代码中，我希望 post 条件检查原始 s stat，而不是我们更改后的 stat。

我在 Dafny 尝试一些东西。我想编写一个简单的数据结构，在内存中保存未压缩的图像：

实际使用它：

导致达芙妮抱怨：

stdin.dfy(3,24)：错误：数据类型构造函数参数的类型不正确（找到 seq，预期数组）在 stdin.dfy 中检测到 1 个分辨率/类型错误

我可能还想要求字节数组不为空，并且字节数组的大小等于宽度 * 高度 * 3（以存储表示该像素的 RGB 值的三个字节）。

我应该以什么方式执行此操作？我研究了 newtype，它可以让您对具有某种类型的变量施加一些约束，但这仅适用于数字类型。