我开始学习Dafny，我只学习了不变量。我有这样的代码：{ else if n==1 then m var i:=0; while i<=n { i:=i+1;}
给定的错误如下：“这个循环不变量可能<em
浏览 8提问于2017-08-18得票数 2
回答已采纳
我试图理解为什么我下面的断言是失败的。我可以理解这是因为循环不变量，但是为什么Dafny要这样做呢？当我已经清楚地说明了循环条件是while I< n时，为什么它如此依赖于循环不变量？这是因为Dafny先看验证码吗？也就是说，在查看实际代码之前，不变行？
浏览 7提问于2020-09-02得票数 0
1回答
下面是用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
回答已采纳
我试着使用dafny来验证我的qsort函数的正确性，但是我想知道为什么我的代码已经被验证失败了。storeIndex); } 这些错误是：
断言ai <= ai+1；
(a，左，storeIndex)；
由于@J
浏览 4提问于2018-04-11得票数 2
回答已采纳
1回答
如果我的索引在每次迭代后都不会减少，我如何避免减少错误？为什么我在对象和数组上使用modify子句时，却在它们上使用modify子句？frees]; //error 3 } boo := true;我还用Dafny正如您所看到的，由于其他修改违规问题，我修改了数组m_owner，并将ownerIndex外包给了另一个对象。但在这里，达夫尼的语言似乎是有限<
浏览 13提问于2017-12-30得票数 2
回答已采纳
嗨，为了教学，我准备了一大堆简单的愚蠢的问题。基本上一切都很好，但是...要么我错过了Dafny中关于循环不变量的一些细节，要么这是一个弱点/bug？invariant i<= a i:=i+1; } 该方法无法验证，并出现错误"invariant t hold on entry
浏览 47提问于2021-07-31得票数 0
我想要有一个分配两个迭代器的函数，然后进入一个循环，只要MoveNext()返回true，它就会重复调用迭代器上的MoveNext()。然而，在迭代器上调用MoveNext()会违反(或阻止Dafny验证)另一个迭代器所需的不变量：{ yield; }
{ yield{ iter1More := iter1.MoveNext(); }
浏览 13提问于2019-08-07得票数 1
回答已采纳
1回答
我的任务是初始化一个8x8矩阵，并确保矩阵中的所有元素都设置为零。我还需要使用while循环和循环不变量来实现。invariant forall i,j :: 0 <= i < row && 0 <= j < a.Length1 ==> a[i,j] == 0我首先怀疑我的执行中存在问题。因此，我首先在没有任何前后条件的情况下运行该方法，并打印数组<
浏览 2提问于2018-03-27得票数 1
1回答
while i < 10{ i := i+1;assert a[5] == 5;
到目前为止，非常简单:声明新数组a并用相应的索引位置初始化它的值因此，assert语句应该是正确的，但是dafny抱怨说“违反断言”。我试过将a5与其他数字进行比较，例如4和6，以及其他接近的数字，但是它没有起作用，我想知道为什么？与此相关，我想问一下在dafny (使用VSCode)中打印是如何工作<em
浏览 6提问于2020-12-14得票数 0
在下面的程序中，我创建了类似荷兰国旗问题的东西，并遵循同样的逻辑，这也提供了，程序以0、1s和2s的方式对0、1s和2s的数组进行排序，所有的1在开始的0，0在中间，2在末尾。但是在循环不变量处，我得到了误差This loop invariant might not be maintained by the loop.。
最初，i和j位于索引0，k在最后索引。逻辑是，如果看到2，则j会向上移动，如果看见0只是j向上移动，则使用k和k的交换减少，如果看到
浏览 1提问于2018-05-23得票数 1
回答已采纳
我是达夫尼的新手，我试图在不使用*的情况下为计算机5*m-3*n编写代码。
有人能告诉我我的密码出了什么问题吗？我认为它是不变的和减少的。
浏览 1提问于2019-07-22得票数 1
回答已采纳
0回答
我想在这个方法中做的只是简单地覆盖前面的数组，并用排序后的数字填充它，但是dafny说post-条件不成立，我永远也找不到原因。我猜我需要在循环中添加一些不变量，但是因为它们在进入循环之前被检查过，所以我不知道如何放置一个有效的不变量。i - 1;}
{
forall i :: 1 <= i < |s| ==> s[i] >= s[i-1
浏览 2提问于2017-12-06得票数 1
回答已采纳
1回答
我在为下面列出的插入排序算法编写适当的循环不变量时遇到了问题。我试图证明数组中的所有项在当前索引已经排序之前就已经按照插入排序进行排序了，但是Dafny没有正确地识别我的不变量。j + 1], a[j]; } }我尝试过在循环之外断言aj <= aj+1，但是Dafny当我尝试在循环之外使用数字(如<= a
浏览 4提问于2022-11-11得票数 1
回答已采纳
1回答
我试着用Dafny来验证一个算法。我正在努力修复错误消息“减少表达式可能不会减少(超时)”。我的算法的基本结构如下：
while (U !S在算法中根本没有被修改。我证明了B的基数小于或等于S的基数，所以减额子句是有界的。在分配给B或U(在内部while循环中)的每个赋值后，我可以证明_然而，这还不够，我需要一个循环不变量在内部while循环中声明这一点，但是我不知道如何用Dafny</em
浏览 2提问于2020-03-15得票数 0
回答已采纳
1回答
Dafny中的选择排序
、、、
我的sorted和FindMin函数确实有效，但是selectionsort本身包含达夫尼不会证明的断言，即使它们是正确的。这是我的节目： requires a !
浏览 3提问于2014-07-06得票数 4
回答已采纳
1回答
在dafny中是否有一种方法可以创建一个特定于单个循环迭代的不变量？下面，我试图创建一个dafny程序，以上限的掉期数量的泡沫排序。这个值存储在变量n中，所以我想用(a.Length * (a.Length - 1))/2来确定n的上限。原因是，如果数组是相反的，那么在内部循环的第一次迭代中必须有n个交换，然后在内部循环的第二次迭代中进
浏览 6提问于2021-09-28得票数 1
回答已采纳
1回答
我试图在Dafny中证明一个简单的程序，它可以找到整数数组的最大元素。Dafny在几秒钟内取代了，证明了下面的程序。当我从最后两个ensures规范中删除注释时，Dafny会发出错误消息，指出这可能是由于index然而，max_index < a.Length是正确的，我很难证明这一点。我尝试在if语句中编写一个嵌套的
浏览 2提问于2019-06-02得票数 2
回答已采纳
=0) decreases n1 res := res-3; }
} 我已经尝试增加循环中的不变性。在第一个循环中，我添加了条件res<=5*abs(m)，但是Dafny抱怨说“循环可能无法维护这个循环不变量”。我不明白为什么不是这样。 我能做错什么呢？
浏览 13提问于2020-03-26得票数 0
回答已采纳
我们正在尝试使用Dafny编写一个二进制搜索算法，但似乎Dafny并没有证明程序的正确性。在INV上:这个循环不变量可能不是由loop.Dafny VSCode维护的predicate
浏览 27提问于2018-12-17得票数 0
false; requires 0<=p<N0ensures 0<=p<MDafny告诉我"top.Sta.Dir.HomeShrSet := true；“语句赋值可以更新一个对象，而不是在封闭上下文的修改子句中。我猜我定义了修改top.Sta.Dir.InvSet的
修改to
浏览 2提问于2020-06-20得票数 0
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
云直播活动推荐
腾讯云开发者
