腾讯云
开发者社区
文档
建议反馈
控制台
首页
学习
活动
专区
工具
TVP
最新优惠活动
文章/答案/技术大牛
搜索
搜索
关闭
发布
登录/注册
精选内容/技术社群/优惠产品,
尽在小程序
立即前往
文章
问答
(24)
视频
沙龙
1
回答
Z3
中
的
Horn
子句
z3
如果要分析
的
程序
的
语义以
Horn
子句
的
形式给出,则
Z3
现在支持求解
归纳
不变量(暗示所需
的
属性)。 但是,
上
Z3
源代码
的
master分支中
的
版本不支持此功能。由于
Z3
通过使用插值
的
PDR算法解决了这些
Horn
子句
问题,因此我转而编译了支持(set-logic
HORN
)
的
int
浏览 2
提问于2013-07-06
得票数 3
1
回答
z3
:
归纳
数据类型
上
的
Horn
子句
/固
定点
z3
、
z3py
、
z3-fixedpoint
我试图使用
z3
的
固
定点
来断言程序
的
等价性,我发现任何类型
的
递归,即使是微不足道
的
可判定
的
递归,都会使
z3
完全卡住。This z3py tutorial特别将程序模拟作为Fixedpoints
的
一个用例,程序由递归
数据类型
表示。我觉得我一定是做错了什么。下面是一个简单
的
例子: from
z3
import * Li
浏览 31
提问于2020-09-18
得票数 0
1
回答
muZ中
的
可解查询
z3
我想通过muZ为BMC使用
z3
。也许我遗漏了一些关于查询可满足性
的
定义。然而,在下面的例子中,我有一个无法满足
的
查询示例(即,返回"false"),但是当添加额外
的
约束(有效地给出令人满意
的
赋值)时,将返回一个有效
的
赋值。是否有任何文档可以帮助理解
z3
的
muZ语言扩展的确切语义?formula undete
浏览 1
提问于2013-09-16
得票数 0
1
回答
支持
定点
SMT工具
z3
、
smt
您知道除了
Z3
之外,还有其他支持固
定点
的
工具吗?
浏览 0
提问于2012-08-25
得票数 1
回答已采纳
3
回答
可以使用LLVM字节码作为
Z3
输入吗?
llvm
、
z3
我有一个LLVM字节码
的
描述,我需要作为
Z3
输入传递。如果可以做到,那该怎么做呢?如果没有,有什么工具可以做到吗??
浏览 0
提问于2014-02-12
得票数 1
1
回答
基于
Z3
的
程序可满足性
z3
如何使用
Z3
检查程序
的
可满足性?例如:while(x is False) { y = x & yy = x or y
浏览 0
提问于2013-09-24
得票数 2
1
回答
用Z3py实现
horn
-
子句
上
的
不变
归纳
logic
、
z3
、
z3py
、
logic-programming
我目前正在使用Z3py来推导出一些不变量,这些不变量被编码为
horn
-
子句
的
连接词,同时也为不变量提供了一个模板。如果您看到下面的代码片段,我将首先从一个简单
的
示例开始。x = 0; x += 1assert(x == 5)X=0 => Inv(x) X<5 /\ Inv(x) => Inv(x +1)我已经为形式a*x +b <= c
的
不变量提供了一个模板,这样求
浏览 21
提问于2016-08-07
得票数 3
回答已采纳
1
回答
Z3
在(大概)可判定逻辑上超时
z3
我们正在试验一种用于功能程序验证
的
关系逻辑。我们
的
逻辑具有代数
数据类型
上
的
关系,以及关系上
的
等式和子集包含谓词。我们
的
验证程序执行
归纳
程序分析(结构
归纳
),并生成足够强
的
归纳
假设
的
验证条件(VC)。上述编码结果(想必)是有效命题(EPR)一阶逻辑中
的
一个公式.借助
Z3
,我们能够断言许多风险投资
的
有效性(不可满足
的</em
浏览 0
提问于2013-11-12
得票数 0
回答已采纳
2
回答
为了使
Z3
能够验证具有递归
的
程序
的
可满足性,我们还需要添加哪些附加公理?
z3
、
smt
、
z3py
就像我们一样,
Z3
有递归
的
局限性。有没有办法得到以下程序
的
结果?什么额外
的
方程式将帮助
z3
得到结果?from
z3
import * m=Int('m')
浏览 0
提问于2017-07-10
得票数 3
回答已采纳
2
回答
如果
Z3
不支持诱导,Dafny是如何支持
的
?
z3
、
proof
、
dafny
、
formal-verification
、
induction
而且,据我所知,每当我们在Dafny中使用断言时,在它下面发生了什么,它构造了证明义务,然后使用
Z3
对它们进行计算。然而,我读到
Z3
不支持
归纳
:例如.然而,任何非平凡
的
属性都需要通过
归纳
法来证明.
Z3
目前不支持
归纳
证明.() 因此,我
的
问题是:每当我们设置{:induction true}时,如果不使用
Z3
,在Dafny中如何执行这种
归纳
?有不同
的
潜在求解者吗?有什么启发法吗?最后一个建议是在这里(
浏览 39
提问于2022-09-26
得票数 1
回答已采纳
1
回答
在
z3
中实现GDL
的
尝试
c#
、
z3
我正在尝试使用中
的
z3
实现一些GDL c#,而且我几乎被困在了起始块中。基本
上
,我想从下面的gdl开始非常简单(init (state 0)) (true (state 0))) (does you proceed)) (true (state 1))) 然后询问哪一个“法律”是可满足
的
(在这个设计
的</e
浏览 2
提问于2013-08-01
得票数 1
回答已采纳
2
回答
如何在
z3
中定义代数
数据类型
上
的
z3py函数(即递归函数)?
z3
、
z3py
、
algebraic-data-types
我
的
目标是将队列定义为
z3
数据类型
(在z3py中),这样我就可以将队列上
的
操作作为约束来执行。有没有办法这样做,如果有,那又是什么呢?我
的
第一本能是使用代数
数据类型
(ADT),比如在OCaml或Haskell中经常使用
的
递归函数定义。我发现了一些不久前在
z3
中讨论ADT
的
文章,比如。其他帖子
上
的
一些答案声称
z3
不支持递归,但是对这个问题
的
公认答案定义了一个非常类似
浏览 0
提问于2019-08-01
得票数 0
回答已采纳
2
回答
Z3
中带有量词
的
函数
z3
设a(0) = 0,根据x(n)
的
值,a(n)+1或a(n)+2。我们可以预期,对于任何类型
的
x(.)对于所有n,a(n) <= n*2。下面是
Z3
的
代码:(declare-fun x (Int) Int)(assert (forall) )(assert (= (a 0) 0))(get-mo
浏览 1
提问于2017-10-27
得票数 3
回答已采纳
1
回答
如何在
Z3
中进行增量解决?
z3
、
smt
关于
Z3
如何增量地解决问题,我有一个问题。在阅读了这里
的
一些答案后,我发现如下: 在假设模式(我不知道名称,也就是我想到
的
名称)中,
z3
不会简化某些公式,例如值传播。我做了一些比较(欢迎您询问公式,它们太大,不能放在rise4fun
上</e
浏览 2
提问于2013-05-07
得票数 54
回答已采纳
1
回答
z3
中
的
最大递归界
z3
、
smt
我在下面写了一个基准测试来生成两个列表
的
叉积。
z3
是否有某种最大递归界?出于某种原因,它可以推断出大小为1
的
列表,而不是大小为2
的
列表,或者可能我在形式化中
的
某个地方出错了?
浏览 18
提问于2019-02-10
得票数 0
2
回答
对Coq中记录构造中
的
模式匹配感到困惑
coq
我使用Coq
的
时间很短,但我仍然会遇到一些问题。我已经定义了一个带有记录构造
的
集合。现在我需要做一些模式匹配才能使用它,但我在正确使用它时遇到了问题。首先,这些是我
的
元素。现在,我需要在“特殊”元素
上
使用定义和固
定点
,只需要我选择
的
两个元素。当然,这告诉我,我错过了元素
的
归纳
部分
的
所有内容,所以我添加了{|E := _ |}=> 0,或者其他任何东西,只是为了让
归纳
变得完整。我一直无法解决
的
是
浏览 1
提问于2016-03-28
得票数 0
2
回答
我们如何知道所有Coq构造函数都是内射
的
和不相交
的
?
constructor
、
coq
、
injective-function
根据,所有构造函数(对于
归纳
类型)都是内射
的
和不相交
的
: 我只是想知道我们怎么知道这个假设成立?和 ( 2)一些plus函数,通过构造函数
的</
浏览 5
提问于2015-09-19
得票数 5
回答已采纳
1
回答
如何在Haskell中使用快速排序按accountID对列表进行排序
sorting
、
haskell
、
functional-programming
我是一个对函数式编程非常陌生
的
学生。我正在开发一个银行应用程序,其中
的
数据已经定义为data Accounttype = Saving | Current | FixedDeposit derivingsortByID exampleBase mapM_ putStrLn viewRecord 但是我没有得到预期
的
结果因为它给了我一个错误,告诉我“viewSortedDetails定义所需
的</em
浏览 0
提问于2010-10-24
得票数 1
回答已采纳
2
回答
如何随着天数
的
递增来获得每天
的
输出
java
、
spring-boot
test date incrementation** dDate.plusDays(1));} 我想要实现
的
是在每天凌晨1点获得输出(已经完成),但随着天数
的
增加而递增。
浏览 0
提问于2019-08-07
得票数 2
7
回答
协助Agda
的
终止检查程序
functional-programming
、
termination
、
agda
Agda将在鲑鱼中画f,因为它不能判断n/2是否小于n,我不知道如何告诉Agda
的
终止检查器。我在标准库中看到,它们
的
除法是2,证明了n/2 < n。但是,我仍然不知道如何使终止检查器实现对较小
的
子问题
的
递归。
浏览 5
提问于2013-10-28
得票数 21
回答已采纳
点击加载更多
扫码
添加站长 进交流群
领取专属
10元无门槛券
手把手带您无忧上云
相关
资讯
这38个小技巧告诉你如何快速学习MySQL数据库
告诉你38个MySQL数据库的小技巧!
数据库优化建表优化
Protobuf编码原理及优化技巧探讨
Apache Calcite:异质数据源优化查询框架
热门
标签
更多标签
云服务器
即时通信 IM
ICP备案
对象存储
实时音视频
活动推荐
运营活动
广告
关闭
领券