问题标签 [dafny]

我试图在 dafny 中证明这个程序，但我仍然得到最后一个不变量的错误，我不明白为什么它不起作用。

该程序包含一个将 int 插入排序数组的方法。int 将插入正确的位置，即：将 5 插入 1,2,3,4,5,6,7 将返回：1,2,3,4,5,5,6,7

谢谢

这个证明在 Dafnys 的验证器中给出了一个无限循环：

这指向某种不确定性问题还是它？有没有更好的方法来呈现这个问题以避免无限循环？

以前的版本：

谁能帮我解决这里的问题。验证此程序时出现以下错误。

我尝试了各种方法，但它从未通过验证。请帮忙。

......

我一直在研究 Dafny 中引理的使用，但发现很难理解，显然下面的示例无法验证，很可能是因为 Dafny 没有看到归纳法或类似引理的东西来证明计数的某些属性? 基本上，我不知道我需要如何定义或定义什么来帮助说服 Dafny 计数是归纳性的等等。一些确保和不变量规范不是必需的，但这不是重点。顺便说一句，这在 Spec# 中更容易。

来自办公室的问题 - 树的边界是从左到右顺序的提示值序列。我需要开发迭代代码，使用以下 IO 类的 OUTPUT 方法打印给定树的边界

我有一个数组line，其中包含一个长度为 的字符串l， pat是另一个数组，其中包含一个长度为 的字符串p。注意：pandl不是数组的长度

目的是查看 中包含的字符串是否pat存在于 中line。如果是这样，这个方法应该返回line单词第一个字母的索引，如果不是，它应该返回-1。

给我们“没有发现触发”错误的不变量是ensures exists j :: ( 0<= j < l) && j == pos;和invariant forall j :: 0 <= j < iline ==> j != pos;

我对循环的逻辑是，当它们在循环中时，找不到索引。并且确保它遇到索引时。

有什么可能是错的？

这是代码：

我收到以下错误： Dafny 输出的屏幕截图

这是rise4fun 上的代码。

我有一个数组“line”，其中包含一个长度为“l”的字符串，还有一个数组“nl”，其中包含一个长度为“p”的字符串。注意：“l”和“p”不一定是每个对应数组的长度。参数“at”将是在“line”内进行插入的位置。恢复：长度为“p”的数组将插入“line”，将“line”的所有字符在位置（at，i，at+p），'p'位置之间向右移动以进行插入。

我的确保逻辑是检查插入“line”中的元素是否具有相同的顺序并且是否与“nl”中包含的字符相同。

这是代码：

这是 我收到的错误。

谢谢。

我想查询一个特定的 Dafny 程序是否验证。Dafny 通常用于在 Visual Studio IDE 中以交互方式开发程序。

但是，我需要以非交互方式执行查询。特别是我需要从 python 程序中查询 Dafny。这可能吗？

我正在使用 Dafny 制作一个删除方法，您会收到：

• 字符数组line

• 数组的长度l

• 一个位置at

• 要删除的字符数p

首先从 at to 删除 line 的字符at + p，然后必须移动at + pto右边的所有字符at。

例如，如果您有[e][s][p][e][r][m][a], and at = 3, and p = 3, 那么最终结果应该是[e][s][p][a]

我试图证明一个有意义的后置条件，例如：

ensures forall j :: (at<=j<l) ==> line[j] == old(line[j+p]);

确保 at + p 右侧的所有字符都在新位置。

但是 Dafny 输出两个错误：

索引超出范围 7 53

后置条件可能不会在此返回路径上成立。19 2

这是rise4fun上的程序

我想知道为什么我收到以下程序的错误：

我得到了：invalid UnaryExpression当我运行这个时。