嵌套循环的Dafny - Loop不变量 - 腾讯云开发者社区

文章/答案/技术大牛

发布

1回答

嵌套循环的Dafny - Loop不变量

dafny

我正在尝试创建一个Dafny程序，当且仅当A不包含重复项时才返回true。这就是我到目前为止所拥有的，但是不变量invariant r <==> (forall j :: 0 <= j < i && j != i ==> A[j] !

浏览 27提问于2020-04-22得票数 0

回答已采纳

1回答

理解循环不变式和断言在dafny中的工作方式

dafny

我试图理解为什么我下面的断言是失败的。我可以理解这是因为循环不变量，但是为什么Dafny要这样做呢？当我已经清楚地说明了循环条件是while I< n时，为什么它如此依赖于循环不变量？这是因为Dafny先看验证码吗？也就是说，在查看实际代码之前，不变行？

浏览 7提问于2020-09-02得票数 0

1回答

Dafny对带有break的循环了解多少？

iteration、break、dafny

Grd;} var x:int := tester([1,-9,0]);} 显然，Dafny明白不变量不再成立。

浏览 0提问于2020-09-09得票数 2

1回答

我在达夫尼的代码有什么问题？

dafny

我试着使用dafny来验证我的qsort函数的正确性，但是我想知道为什么我的代码已经被验证失败了。这是我的代码： requires a.Length > 0 {storeIndex); } 这些错误是：断言ai <= ai+1；这个

浏览 4提问于2018-04-11得票数 2

回答已采纳

1回答

不由循环维护的Dafny循环不变

formal-verification、dafny

我的任务是初始化一个8x8矩阵，并确保矩阵中的所有元素都设置为零。我还需要使用while循环和循环不变量来实现。然而，达夫尼认为，我的循环在外部时间循环中是不变的。invariant forall i,j :: 0 <= i < row && 0 <= j < a.Length1 ==> a[i,j] == 0我首先怀疑我的

浏览 2提问于2018-03-27得票数 1

1回答

在dafny断言中进行数组初始化后失败

computer-science、verification、dafny

while i < 10{ i := i+1;assert a[5] == 5;

浏览 6提问于2020-12-14得票数 0

2回答

标识循环-这个循环不变量可能不会由循环来维护。

arrays、while-loop、dafny

但是dafny返回BP5005: This loop invariant might not be maintained by the loop.作为forall条件。这对我来说没有多大意义，因为循环体确实完成了我们在不变量中定义的内容。 invariant for

浏览 1提问于2020-11-25得票数 0

回答已采纳

1回答

dafny初始断言在循环中没有验证相同的最终断言验证

iteration、assert、dafny

您好，我已经将问题简化为一种简单地将一个数组的元素复制到另一个数组的方法。我的问题是，最终的断言会验证，而初始的断言却无法验证，即使我有一个保护措施来确保初始断言只在第一次进入循环之后应用。因此，我认为最终的断言应该暗示初始的断言。任何帮助都非常感谢。

浏览 0提问于2020-09-11得票数 1

1回答

我的dafny方法怎么了。简单方法的后置条件可能不成立

dafny

我是达夫尼的新手，我试图在不使用*的情况下为计算机5*m-3*n编写代码。有人能告诉我我的密码出了什么问题吗？我认为它是不变的和减少的。

浏览 1提问于2019-07-22得票数 1

回答已采纳

2回答

Dafny循环不变量失败，即使不变量断言有效。这是一个小bug吗？

dafny、loop-invariant

嗨，为了教学，我准备了一大堆简单的愚蠢的问题。基本上一切都很好，但是...要么我错过了Dafny中关于循环不变量的一些细节，要么这是一个弱点/bug？

浏览 47提问于2021-07-31得票数 0

1回答

如何证明插入中的循环不变量？

dafny、formal-verification

我在为下面列出的插入排序算法编写适当的循环不变量时遇到了问题。我试图证明数组中的所有项在当前索引已经排序之前就已经按照插入排序进行排序了，但是Dafny没有正确地识别我的不变量。[j], a[j + 1] := a[j + 1], a[j]; } }我尝试过在循环之外断言aj <= aj+1，但是Dafn

浏览 4提问于2022-11-11得票数 1

回答已采纳

0回答

排序的后置条件不成立

dafny

我想在这个方法中做的只是简单地覆盖前面的数组，并用排序后的数字填充它，但是dafny说post-条件不成立，我永远也找不到原因。我猜我需要在循环中添加一些不变量，但是因为它们在进入循环之前被检查过，所以我不知道如何放置一个有效的不变量。i - 1;} { forall i :: 1 <= i < |s| ==> s[i] >= s[i-1

浏览 2提问于2017-12-06得票数 1

回答已采纳

1回答

Dafny使用交换验证插入排序。

swap、insertion-sort、loop-invariant、dafny

我正在研究如何使用dafny来使用“交换”相邻元素来验证插入排序，但是我无法为while循环找到一个合理的不变量，有人能帮我修复它吗？下面是链接：

浏览 10提问于2017-05-19得票数 0

回答已采纳

1回答

(Dafny)排序数组-循环不变量

sorting、verification、loop-invariant、dafny

下面是用Dafny编写的一个简单的排序算法： requires a != null && b !但是，如果我将不变量forall m,n | 0 <= m < j < n <= i :: a[m] <= a[n]从内循环中删除，则Dafny告诉我，不变量sorted(a,j,i+1)可能不是由循环</

浏览 3提问于2017-06-08得票数 2

回答已采纳

1回答

在Dafny中使用后置条件修改数组

dafny

尝试实现一个相当简单的方法，传递一个空数组并将值放入其中(自然数)。代码运行得很好，但是一个简单的后置条件会抛出错误，这个后置条件应该会在我脑海中传递。

浏览 7提问于2019-08-09得票数 1

回答已采纳

1回答

dafny中的指数方法:可能不会维护不变量

loop-invariant、dafny

我开始学习Dafny，我只学习了不变量。我有这样的代码：{ else if n==1 then m var i:=0; while i<=n { i:=i+1;} 给定的错误如下：“这个循环不变量可能不会被

浏览 8提问于2017-08-18得票数 2

回答已采纳

1回答

Dafny无法验证while循环中的多个迭代器

dafny

我想要有一个分配两个迭代器的函数，然后进入一个循环，只要MoveNext()返回true，它就会重复调用迭代器上的MoveNext()。然而，在迭代器上调用MoveNext()会违反(或阻止Dafny验证)另一个迭代器所需的不变量：{ yield; } { yield{ iter1More := iter1.MoveNext();

浏览 13提问于2019-08-07得票数 1

回答已采纳

1回答

涉及序列的dafny代码中缺少不变量

dafny

我想知道dafny无法验证我的程序是否有原因？ https://rise4fun.com/Dafny/Ip1s 我是不是遗漏了一些额外的不变量？

浏览 19提问于2019-01-19得票数 0

回答已采纳

1回答

如何用dafny证明气泡排序的时间复杂性？

time-complexity、bubble-sort、proof、dafny

在dafny中是否有一种方法可以创建一个特定于单个循环迭代的不变量？下面，我试图创建一个dafny程序，以上限的掉期数量的泡沫排序。这个值存储在变量n中，所以我想用(a.Length * (a.Length - 1))/2来确定n的上限。原因是，如果数组是相反的，那么在内部循环的第一次迭代中必须有n个交换，然后在内部循环的第二次迭代中进行n-1交换，等等

浏览 6提问于2021-09-28得票数 1

回答已采纳

1回答

Dafny未能证明整数数组中的max元素

specifications、dafny、loop-invariant

我试图在Dafny中证明一个简单的程序，它可以找到整数数组的最大元素。Dafny在几秒钟内取代了，证明了下面的程序。当我从最后两个ensures规范中删除注释时，Dafny会发出错误消息，指出这可能是由于index然而，max_index < a.Length是正确的，我很难证明这一点。我尝试在if语句中编写一个嵌套的不变量，

浏览 2提问于2019-06-02得票数 2

回答已采纳

点击加载更多