我想知道dafny无法验证我的程序是否有原因？ https://rise4fun.com/Dafny/Ip1s 我是不是遗漏了一些额外的不变量？
浏览 19提问于2019-01-19得票数 0
回答已采纳
我试着使用dafny来验证我的qsort函数的正确性，但是我想知道为什么我的代码已经被验证失败了。这是我的代码： requires a.Length > 0 {不变左<= storeIndex <右+1
(a，左，storeIndex)；
由于@James Wilcox的回答，
浏览 4提问于2018-04-11得票数 2
回答已采纳
我试图理解为什么我下面的断言是失败的。我可以理解这是因为循环不变量，但是为什么Dafny要这样做呢？当我已经清楚地说明了循环条件是while I< n时，为什么它如此依赖于循环不变量？这是因为Dafny先看验证码吗？也就是说，在查看实际代码之前，不变行？
浏览 7提问于2020-09-02得票数 0
我正在检查某个键是否只在数组中出现一次(其中b是返回值)，但是下面的不变量说明它不是由循环维护的： invariant b <==> exists j | 0 <= j < i :: a[j] ==if (keyCount == 1) else i := i + 1;
} 逻辑在我看来似乎是合理的-
浏览 19提问于2019-10-02得票数 2
回答已采纳
在阅读了Getting Started with Dafny: A Guide之后，我决定创建我的第一个程序:给定一个整数序列，计算其元素的和。然而，我很难让Dafny来验证这个程序。我怀疑Dafny需要一些“帮助”来验证程序(也许是引理？)但是我不知道从哪里开始。
浏览 5提问于2017-06-10得票数 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提问于2020-09-11得票数 1
1回答
下面是用Dafny编写的一个简单的排序算法： requires a != null && b !a[j], a[j-1] := a[j-1], a[j]; } }该代码没有错误但是，如果我将不变量forall m,n | 0 <= m < j <
浏览 3提问于2017-06-08得票数 2
回答已采纳
0回答
我想在这个方法中做的只是简单地覆盖前面的数组，并用排序后的数字填充它，但是dafny说post-条件不成立，我永远也找不到原因。我猜我需要在循环中添加一些不变量，但是因为它们在进入循环之前被检查过，所以我不知道如何放置一个有效的不变量。i - 1;}
{}
我之前<e
浏览 2提问于2017-12-06得票数 1
回答已采纳
我是达夫尼的新手，我试图在不使用*的情况下为计算机5*m-3*n编写代码。
有人能告诉我我的密码出了什么问题吗？我认为它是不变的和减少的。
浏览 1提问于2019-07-22得票数 1
回答已采纳
1回答
我的任务是初始化一个8x8矩阵，并确保矩阵中的所有元素都设置为零。我还需要使用while循环和循环不变量来实现。因此，我首先在没有任何前后条件的情况下运行该方法，并打印数组中的所有元素；输出是一个充满零的矩阵。为了确保是替换了所有元素，而不仅仅是使用从矩阵实例化时开始使用的零，我将矩阵中的所有元素初始化为1s，并打印出其中的所有值。结果是相同的-所有元素在矩阵<e
浏览 2提问于2018-03-27得票数 1
嗨，为了教学，我准备了一大堆简单的愚蠢的问题。基本上一切都很好，但是...要么我错过了Dafny中关于循环不变量的一些细节，要么这是一个弱点/bug？
浏览 47提问于2021-07-31得票数 0
我开始学习Dafny，我只学习了不变量。我有这样的代码：{ else if n==1 then m var i:=0; while i<=n { i:=i+1;}
给定的错误如下：“这个循环不变量可能不会被
浏览 8提问于2017-08-18得票数 2
回答已采纳
1回答
我试图在Dafny中证明一个简单的程序，它可以找到整数数组的最大元素。Dafny在几秒钟内取代了，证明了下面的程序。当我从最后两个ensures规范中删除注释时，Dafny会发出错误消息，指出这可能是由于index然而，max_index < a.Length是正确的，我很难证明这一点。我尝试在if语句中编写一个嵌套的
浏览 2提问于2019-06-02得票数 2
回答已采纳
1回答
如果我的索引在每次迭代后都不会减少，我如何避免减少错误？为什么我在对象和数组上使用modify子句时，却在它们上使用modify子句？frees]; //error 3 } boo := true;我还用Dafny上传了这段代码，您可以在那里重新编译它：。正如您所看到的，由于其他修改违规问题，我修改了数组m_owner，并将ownerIndex外包给了另一个对象。但在这里，
浏览 13提问于2017-12-30得票数 2
回答已采纳
1回答
我在为下面列出的插入排序算法编写适当的循环不变量时遇到了问题。我试图证明数组中的所有项在当前索引已经排序之前就已经按照插入排序进行排序了，但是Dafny没有正确地识别我的不变量。j + 1], a[j]; } }我尝试过在循环之外断言aj <= aj+1，但是Dafny
浏览 4提问于2022-11-11得票数 1
回答已采纳
1回答
Dafny中的序列是不可变的类型，因此从验证的角度来看，它们在运行时的表示方式并不重要。但正如函数式程序员所知道的那样，用函数式语言表示列表是正常的(在某种程度上程序员无法操作)为链表，因此取列表的尾部是常数时间(不涉及存储分配)，因此列表连接重新分配左参数的单元格，但只使用对右参数的引用是否记录了序列打算如何在Dafny实现中
浏览 0提问于2021-10-25得票数 2
1回答
在dafny中是否有一种方法可以创建一个特定于单个循环迭代的不变量？下面，我试图创建一个dafny程序，以上限的掉期数量的泡沫排序。这个值存储在变量n中，所以我想用(a.Length * (a.Length - 1))/2来确定n的上限。原因是，如果数组是相反的，那么在内部循环的第一次迭代中必须有n个交换，然后在内部循环的第二次迭代中进行n-1交换，等等
浏览 6提问于2021-09-28得票数 1
回答已采纳
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备案
腾讯会议
云直播
对象存储活动推荐
腾讯云开发者
