验证循环修改子句

文章/答案/技术大牛

发布

1回答

dafny、formal-verification

对，所以我正在尝试验证下面的fill()方法。目前第一个和第三个invariant子句失败了，我不能完全确定原因。任何想法都很感谢！

浏览 22提问于2021-04-09得票数 1

1回答

将修改添加到方法中断循环不变量

dafny

最重要的问题是，当我向一个方法添加修改时，我的一些循环不变量突然不再正确检查了。 } }} 具体来说，当我将modifies arr添加到Merge签名时，第4和第5循环不变量就会失败我可以理解，我可能需要在循环中添加一个不变量，说它不编辑arr，但是我无法找到如何做到这一点？

浏览 3提问于2021-01-18得票数 0

回答已采纳

6回答

当循环中的if子句中断时，在函数中返回false

javascript、function、for-loop、return、break

我有一个函数，它运行抛出一个输入值数组(for循环)。在这个循环中，我使用if子句检查验证是否返回true或false (调用其他函数)。当验证返回false时，我希望在函数中中断for循环并返回false，然后跳出它。validateForm(values[i]) { }} 使用if子句中的break语句，我可以跳出for

浏览 2提问于2018-02-15得票数 1

回答已采纳

1回答

Frama-C阶函数

c、frama-c

我试图用Frama和ACSL语言证明我的排序函数'order‘的正确性。我有一个额外的“交换”函数来改变数组t的两个值。/*@ requires l > 0; assigns t[i], t[j]; ensures t[i] == \old

浏览 1提问于2018-11-10得票数 1

1回答

dafny非别名记忆怪异行为

alias、memory-model、dafny

为了完整起见，我再次将一个dafny定义的图ADT (来自)带到这里：{ constructor (adjListInput : seq<seq<int>>) { }function ValidGraph(G : Graph) : bool{ (fo

浏览 1提问于2020-08-06得票数 1

回答已采纳

3回答

For循环应该是格式良好的。

c、loops、for-loop、while-loop、misra

MISRA C-2012控制流表达式(MISRA C-2012规则14.2) { {modify_expr:修改表达式

浏览 0提问于2021-12-02得票数 2

回答已采纳

1回答

删除Dafny中特定索引失败处的元素

dafny、formal-verification、induction

我有以下问题:我必须在Dafny中实现一个优先级队列。我有以下界面：var capacity: int;var priorities: array<int>;reads this 0 <= nrOfElements <= capacity && capacity ==

浏览 7提问于2021-11-14得票数 1

1回答

Frama-C警告:缺失的赋值子句(指定“一切”代替)

automated-tests、frama-c、acsl

我正在用frama测试这个小程序，而且我一直收到同样的错误。我不知道这意味着什么。我特别搞不懂什么分配一切都意味着什么。// assuming n is nonnegative and even, f returns n */ int i=0; i+=2; //@ assert i==n;}[wp] warning: Missing RTE guards

浏览 0提问于2018-04-12得票数 0

回答已采纳

1回答

parsley.js -手动显示消息，而不必进行验证

javascript、parsley.js

我想在我的javascript代码的其他子句中显示一条欧芹消息： //do things //display parsleyerror我知道欧芹允许定制验证器，如下所示：$( '#myInput' ).parsley( { alwaysFalse: function (

浏览 2提问于2013-07-25得票数 2

回答已采纳

1回答

无法比较通过bat文件声明为成功/失败状态的变量

windows、batch-file、command-line、cmd、command

=ABC)ABCABC\DEFTEMPB\A我觉得这是因为if验证，在这里，我缺少一个单引号或双

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

回答已采纳

1回答

使用方法的结果时违反dafny断言

dafny

我编写了下面的程序来验证数组是否“干净”了任何特定的元素。我很难断言这种方法的结果。在试图断言该方法的结果时，我一直会得到一个断言冲突。

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

回答已采纳

1回答

Dafny中的并行循环终止

while-loop、termination、dafny

我试着用Dafny来验证一个算法。我正在努力修复错误消息“减少表达式可能不会减少(超时)”。我的算法的基本结构如下： while (U !S在算法中根本没有被修改。我证明了B的基数小于或等于S的基数，所以减额子句是有界的。在分配给B或U(在内部while循环中)的每个赋值后，我可以证明_然而，这还不够，我需要一个循环不变量在内部while循环中声明这一点，但是我不知道如何用Dafny来表示它。

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

回答已采纳

1回答

while循环中的动态‘Modifies`子句

loops、for-loop、dafny

while循环中的modifies子句在第一次进入循环时只计算一次。例如，如果我有一个对象序列，并且我增长了它，但也修改了我在以前的迭代中创建的新元素，Dafny不会接受它： var x: int; {var next := new Foo(); i := i + 1;} 我已经尝试过使用递归，它是有效的，但我想使用一个while循环来演示是否有某种“动态”modifies

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

1回答

if else在haml中循环

ruby-on-rails、haml

现在的问题是，这段代码只作为else循环的一部分被调用，而不是if循环的一部分，因为缩进是使用else循环的一部分。如何使用haml实现这一点，以便只使用if/else子句修改.active部分，而不是修改其他窗格。

浏览 3提问于2012-09-26得票数 0

回答已采纳

1回答

将主题筛选应用于邮件查询时Office 365初学者项目错误

c#、asp.net-mvc、office365api

我正在使用在上找到的初学者项目internal async Task<List<model.MailItem>> GetEmailMessages(int pageNo, int pageSize) 我已经开始并重新启动了这个项目好几次。如果删除where子句，它将再次工作。如果我将w

浏览 1提问于2016-05-04得票数 1

回答已采纳

2回答

有没有办法在调试JavaScript时更改变量值？

javascript、debugging、firebug

我在这段代码上有一个断点(使用Firebug)：即使我的dom.forumid无效，如何跳过此验证部分并进入if子句我在考虑修改JavaScript，但我不知道该怎么做。

浏览 1提问于2014-05-11得票数 20

回答已采纳

1回答

Dafny“调用可能违反上下文的修改条款”

dafny

我正在尝试验证一个哈希集，但我的插入方法遇到了问题。当我取消对main中的插入的注释时，我不明白为什么要得到“调用可能违反上下文的修改子句”错误。

浏览 1提问于2017-11-22得票数 2

回答已采纳

1回答

为同一个表创建多个游标，但不同的验证是一种很好的做法

oracle、plsql

我正在处理PL/SQL项目，我必须根据7个验证来执行某些操作。这是一个很好的实践吗？

浏览 2提问于2018-01-03得票数 0

2回答

不调用if-子句n次重用样板循环结构的pythonic方法

python

我继承了一个遗留代码库，其中有许多嵌套的for循环，如下所示： with为了加快速度(除了其他修改)，我想去掉所有if-子句被调用n*m次，测试表明这确实提供了大约10%的改进。有没有一种(公平

浏览 0提问于2019-04-05得票数 2

回答已采纳

4回答

在此示例中，break子句如何响应？

java、loops、break

break子句是如何工作的？我知道如果我在一个循环中有一个break，这个循环将会终止它的执行。例如： for (int i=0; i<10; i++) {} 但是，如果break子句既在循环中，又在if或else中，它会起作用吗？for (int i=0; i<10; i++) { //code //code} brea

浏览 63提问于2020-02-10得票数 3

回答已采纳

点击加载更多