问题标签 [dafny]

我正在研究如何使用 dafny 来验证使用“交换”相邻元素的插入排序，但我找不到 while 循环的合理不变量，谁能帮我修复它？这是链接：http ://rise4fun.com/Dafny/wmYME

我想实现一个方法，它接受一个输入的字符数组并以相反的顺序输出另一个由输入数组组成的数组。但我收到错误“索引我们的范围”和“后置条件可能不成立”我不知道会发生什么

这是我的代码：

1. 错误 1 ​​索引超出范围 6 43
2. 错误 2 后置条件可能在此返回路径上不成立。21 2

3. 这是可能不成立的后置条件。13 26

   stdin.dfy(6,43)：错误：索引超出范围
   stdin.dfy(21,2)：错误 BP5003：后置条件可能不会在此返回路径上成立。
   stdin.dfy(13,26)：相关位置：这是可能不成立的后置条件。
   stdin.dfy(6,2)：相关位置
   stdin.dfy(6,47)：相关位置

很清楚输入是一个数组，但是为什么当它执行 flag[1..] 时，它说 flag 是一个序列？这是链接： http ://rise4fun.com/Dafny/fUgu

我有一个函数sum，它接受两个数组a并b作为输入并b修改b[i] = a[0] + a[1] + ... + a[i]. 我写了这个函数，想用 Dafny 验证它。但是，Dafny 告诉我，循环可能不会维护我的循环不变量。这是代码：

我该如何解决这个错误？

我是 dafny 的新手，正在尝试让这段简单的代码工作。我想计算字符串中 char 的出现次数。我在第 4 行收到了一个断言违规。我知道我的函数正在查找正确数量的字符，但显然这个断言中有一些漏洞。在开始使用前置条件和后置条件之前，我试图了解基础知识，而没有它们应该是可能的。该函数仅检查字符串中的最后一个字符并返回 1 或 0，然后再次调用该函数，该函数会切断字符串的尾部，直到它为空。

http://rise4fun.com/Dafny/2lvt 这是我的代码的链接。

这是一个用Dafny编写的简单排序算法：

代码没有错误。但是，如果我从forall m,n | 0 <= m < j < n <= i :: a[m] <= a[n]内部循环中删除不变量，Dafny 会告诉我循环sorted(a,j,i+1)可能不会维护不变量。

1. 这是为什么？

2. 怎么能猜到一 forall m,n | 0 <= m < j < n <= i :: a[m] <= a[n] 开始就需要不变量呢？

   我试图在纸上证明这个程序，但是在构造内部循环的不变量时我不需要这个不变量。

考虑以下尝试在数组a中查找元素e的Dafny代码：

验证工作正常，但有些东西我不确定：如果我没记错的话，循环的变体（如果它是整数）必须以零为界。然而，在最后一次迭代u-i时低于零。i = u+1为什么 Dafny 不抱怨u-i不受零约束？

在阅读了 Dafny 入门：指南之后，我决定创建我的第一个程序：给定一个整数序列，计算其元素的总和。但是，我很难让 Dafny 验证该程序。

我明白了

我怀疑 Dafny 需要一些“帮助”来验证程序（可能是引理？），但我不知道从哪里开始。

考虑解决100 名囚犯和一个灯泡问题的标准策略。这是我在 Dafny 中对其建模的尝试：

然而，它最终无法证明这一点I == P。为什么？我可能需要进一步加强循环不变量，但无法想象从哪里开始......

编译以下代码时：

我得到输出

鉴于Implementation精炼Interface，为什么编译器需要Interface.addSome有一个主体，尤其是当addSomeghost 无论如何不应该参与编译时？