腾讯云
开发者社区
文档
建议反馈
控制台
首页
学习
活动
专区
工具
TVP
最新优惠活动
文章/答案/技术大牛
搜索
搜索
关闭
发布
登录/注册
精选内容/技术社群/优惠产品,
尽在小程序
立即前往
文章
问答
(9999+)
视频
沙龙
1
回答
Dafny
中
可以
存在
静态
变量
吗
?
但是,从编程的角度来看,
静态
字段也有其用途。 由于
Dafny
编译到.NET平台,因此
可以
合理地期待某种方式来公开
静态
变量
。
浏览 9
提问于2019-03-04
得票数 0
回答已采纳
1
回答
dafny
如何编码涉及数组的条件的验证?
、
与直接使用z3进行编码相比,我正在评估
Dafny
的使用情况,这是我们公司
存在
的一个问题。method Find(a: array<int>) returns (index: int) index := a.Length;现在
浏览 2
提问于2019-10-21
得票数 1
1
回答
Dafny
简单的断言不成立
在exercise_1a
中
,怎样才能使断言cnt > 0有效?
浏览 2
提问于2020-06-19
得票数 0
1
回答
函数将出现在注释之外。
在练习之后,它提到函数只能出现在注释
中
。因此,一个人不能写:本教程还提到,有时在实代码中使用函数很方便,因此
可以
定义函数方法,它
可以
从实代码
中
调用。因此,在练习5
中
,这就是我所写的:{} var b := 4; var c := max(a,b); /
浏览 5
提问于2021-12-14
得票数 1
回答已采纳
1
回答
理解循环不变式和断言在
dafny
中
的工作方式
我
可以
理解这是因为循环不
变量
,但是为什么
Dafny
要这样做呢?当我已经清楚地说明了循环条件是while I< n时,为什么它如此依赖于循环不
变量
?这是因为
Dafny
先看验证码
吗
?
浏览 7
提问于2020-09-02
得票数 0
1
回答
Dafny
未能证明整数数组
中
的max元素
、
、
我试图在
Dafny
中
证明一个简单的程序,它
可以
找到整数数组的最大元素。
Dafny
在几秒钟内取代了,证明了下面的程序。当我从最后两个ensures规范
中
删除注释时,
Dafny
会发出错误消息,指出这可能是由于index我尝试在if语句中编写一个嵌套的不
变量
,但是
Dafny
拒绝了这个语法。有什么解决办法
吗
?
浏览 2
提问于2019-06-02
得票数 2
回答已采纳
1
回答
我在达夫尼的代码有什么问题?
我试着使用
dafny
来验证我的qsort函数的正确性,但是我想知道为什么我的代码已经被验证失败了。storeIndex); } 这些错误是: 断言ai <= ai+1; 这个循环不
变量
可能不会由循环来维护left<=p<right &if;left<=p<right&if;var storeIndex : int :=左;var i: int :=左;i<右-1不变左<= sto
浏览 4
提问于2018-04-11
得票数 2
回答已采纳
1
回答
如何用
dafny
证明气泡排序的时间复杂性?
、
、
、
在
dafny
中
是否有一种方法
可以
创建一个特定于单个循环迭代的不
变量
?下面,我试图创建一个
dafny
程序,以上限的掉期数量的泡沫排序。这个值存储在
变量
n
中
,所以我想用(a.Length * (a.Length - 1))/2来确定n的上限。原因是,如果数组是相反的,那么在内部循环的第一次迭代
中
必须有n个交换,然后在内部循环的第二次迭代中进行n-1交换,等等,直到数组被排序。这相当于1+2+3+.我想知道,在
dafny
中
浏览 6
提问于2021-09-28
得票数 1
回答已采纳
1
回答
Dafny
中
的类型约束:为二元关系类型实现"Show“
我在
Dafny
中
定义了一个多态的二元关系类型(一个类):实际的声明是:也许我错了,比参考手册更新的更新提供了这样的功能。
浏览 69
提问于2018-03-05
得票数 1
回答已采纳
1
回答
如果我使用不同的Boogie后端来检查
Dafny
翻译的bpl文件,我能找到非伪反例
吗
?
、
正如在
Dafny
GitHub上的Wiki中提到的,当
Dafny
不能证明程序
中
的断言时,这可能是由于我的程序不正确或
Dafny
不完整所致。如果我设法使用另一个Boogie后端(如Corral )来检查使用/print从
Dafny
编译的Boogie程序,而Corral还返回一个模型来使Boogie程序失效,这能保证模型否定我的
Dafny
程序并且我
可以
使用它进行调试
吗
从他们的论文中,我认为Corral和Symbooglix应该保证提供的模型应该是
浏览 2
提问于2018-09-12
得票数 1
回答已采纳
1
回答
假设
静态
变量
总是
存在
的安全
吗
?
在Java
中
,我一直认为类
变量
(用关键字
静态
定义)等同于其他语言(如C )
中
的全局
变量
,它们是在类
中
定义的,以避免名称冲突。在C
中
,您
可以
引用任何函数的全局
变量
,它在程序运行时总是
存在
的。Java
中
的
静态
变量
呢?它们总是
存在
吗?他们被推荐的时候总是会上膛
吗
?当我使用另一个类的
静态
方法
中
的<em
浏览 5
提问于2015-05-31
得票数 1
回答已采纳
1
回答
尝试见证null:操作结果可能违反子集类型约束
你知道我应该去哪里看
吗
?是不是
Dafny
不知道子集类型是有人的?有没有办法让它相信它是这样的?type func<T> = f: binRelOnS<T> | f.Valid() && f.isFunction()
Dafny
VSCode尝试见证null:操作结果可能违反“”binRelOnS
浏览 14
提问于2018-03-01
得票数 1
1
回答
为什么达夫尼认为在使用鬼
变量
时,这个前提条件可能会出现问题?
但是,如果我使用t作为参数,而不是myGhostVar;
Dafny
没有抱怨。 两者都有相同的requires谓词,这使它有点混乱。这是我在使用鬼
变量
时缺少的东西
吗
?
浏览 0
提问于2019-12-18
得票数 0
回答已采纳
1
回答
Dafny
/Boogie
中
的触发器是什么?
、
、
我一直在
Dafny
蹒跚前行,并不了解触发器。也许结果是,我编写的程序似乎给验证器带来了很大的困难。有时我花费大量的时间摆弄我的证明,试图说服
Dafny
/Boogie它是有效的;当我得到一些工作,有时它是缓慢的验证(这严重降低了我继续的能力)。 很难问一个准确的问题,因为我不知道我不知道的是什么。
浏览 28
提问于2018-06-04
得票数 2
回答已采纳
1
回答
如何在
Dafny
中产生无效的LogicalExpression?
、
考虑下面的
dafny
函数: function method unpair(n: nat): (nat, nat) var x,y :| n == (x+y)*(x+y+1)/2 + y;这
可以
使用Cantor的配对函数,但不确定我是否有正确的语法,因为
dafny
在返回行上抛出错误:"invalid LogicalExpression“。如何解决此错误?
浏览 23
提问于2021-10-04
得票数 1
回答已采纳
1
回答
赋值
可以
更新不在封闭上下文的修改子句中的对象
false; requires 0<=p<N0ensures 0<=p<M
Dafny
告诉我"top.Sta.Dir.HomeShrSet := true;“语句赋值
可以
更新一个对象,而不是在封闭上下文的修改子句中。
浏览 2
提问于2020-06-20
得票数 0
1
回答
dafny
初始断言在循环中没有验证相同的最终断言验证
、
、
您好,我已经将问题简化为一种简单地将一个数组的元素复制到另一个数组的方法。我的问题是,最终的断言会验证,而初始的断言却无法验证,即使我有一个保护措施来确保初始断言只在第一次进入循环之后应用。因此,我认为最终的断言应该暗示初始的断言。method simpImp(a:array<int>) returns (r:array<int>) print "a ",a[..],"\n"; var i:nat := 0; while
浏览 0
提问于2020-09-11
得票数 1
1
回答
如何证明
Dafny
中
的通用介绍
我正在努力寻找策略来证明
Dafny
中
普遍量化的断言。我看到
Dafny
很容易证明了普遍的淘汰: predicate P<X>(k:X) ensures (forall a:X :: P(a)) ==
浏览 17
提问于2020-08-13
得票数 1
1
回答
在MacOS上验证时,运行
dafny
的VS代码挂起。我
可以
从VScode停止验证器
吗
?
、
使用
Dafny
插件运行VS代码,但检验器挂起function sumNum(l:List) :nat decreases
浏览 5
提问于2021-07-29
得票数 0
1
回答
简单while循环的循环不
变量
、
、
我看过一个示例程序,它将数组
中
的每个值都设置为0:while(i < n) { i++;它说循环不
变量
的一部分是0<我说这不是循环不
变量
的一部分,对
吗
?如果是这样,应该用什么来代替呢?完全不
变量
是For All j (0<= j < i --> a[i] = 0) & 0 <= i < n)
浏览 0
提问于2016-04-08
得票数 1
点击加载更多
扫码
添加站长 进交流群
领取专属
10元无门槛券
手把手带您无忧上云
相关
资讯
PHP实战技巧PHP中的静态知识:静态类属性、方法
我们高中class里有一个static女神
都说变量有七八种,到底谁是 Java 的亲儿子
从 static 关键字深入理解 java 对象初始化顺序
Android面试总结(一)
热门
标签
更多标签
云服务器
ICP备案
实时音视频
对象存储
即时通信 IM
活动推荐
运营活动
广告
关闭
领券