期刊导航
期刊开放获取
河南省图书馆
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
1
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式:
文摘
详细
列表
相关度排序
被引量排序
时效性排序
模型驱动的Dafny程序形式化生成与自动验证
被引量:
1
1
作者
王昌晶
贺江飞
+2 位作者
罗海梅
左正康
许帆
《江西师范大学学报(自然科学版)》
CAS
北大核心
2020年第4期378-384,共7页
Dafny是一种内置规范结构的编程语言和静态程序证明器,它能验证程序的功能正确性以及将证明过程自动化,这既提高了软件开发的效率,又极大增强了软件开发的可靠性.该文探索了一种模型驱动的Dafny程序形式化生成的方法.首先,从问题的Radl...
Dafny是一种内置规范结构的编程语言和静态程序证明器,它能验证程序的功能正确性以及将证明过程自动化,这既提高了软件开发的效率,又极大增强了软件开发的可靠性.该文探索了一种模型驱动的Dafny程序形式化生成的方法.首先,从问题的Radl规约出发,根据规约变换技术得到其Radl算法;然后,根据PAR方法中循环不变式开发新策略得到问题的循环不变式;最后,在Radl算法和循环不变式基础上利用模型等价转换规则生成Dafny程序,并由Dafny证明器自动验证其功能正确性.用该方法解决了2个典型问题的算法程序开发与验证,证实了该方法能够有效地提高Dafny程序的生成效率和可靠性.
展开更多
关键词
模型驱动
Dafny程序
循环不变式
形式化生成
自动验证
下载PDF
职称材料
题名
模型驱动的Dafny程序形式化生成与自动验证
被引量:
1
1
作者
王昌晶
贺江飞
罗海梅
左正康
许帆
机构
江西师范大学计算机信息工程学院
江西师范大学物理与通信电子学院
江西师范大学江西省光电子与通信重点实验室
出处
《江西师范大学学报(自然科学版)》
CAS
北大核心
2020年第4期378-384,共7页
基金
国家自然科学基金(61762049,11804133,61862033)
江西省科技厅课题(2020BABL202025,2020BABL202026,2018BAB206034)资助项目.
文摘
Dafny是一种内置规范结构的编程语言和静态程序证明器,它能验证程序的功能正确性以及将证明过程自动化,这既提高了软件开发的效率,又极大增强了软件开发的可靠性.该文探索了一种模型驱动的Dafny程序形式化生成的方法.首先,从问题的Radl规约出发,根据规约变换技术得到其Radl算法;然后,根据PAR方法中循环不变式开发新策略得到问题的循环不变式;最后,在Radl算法和循环不变式基础上利用模型等价转换规则生成Dafny程序,并由Dafny证明器自动验证其功能正确性.用该方法解决了2个典型问题的算法程序开发与验证,证实了该方法能够有效地提高Dafny程序的生成效率和可靠性.
关键词
模型驱动
Dafny程序
循环不变式
形式化生成
自动验证
Keywords
model driven
Dafny program
loop invariant
formal generation
automatic verification
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
模型驱动的Dafny程序形式化生成与自动验证
王昌晶
贺江飞
罗海梅
左正康
许帆
《江西师范大学学报(自然科学版)》
CAS
北大核心
2020
1
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部