关于断言语言中引入逻辑变量的研究

• 作者: 李为胜 罗奇鸣 陈意云
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: Hoare逻辑 形式化验证 逻辑变量 断言语言
• 年，卷（期）: 2017,（5）
• 所属期刊栏目: 计算机软件与数据库研究
• 页码范围: 925-929
• 页数: 5页
• 分类号: TP311
• 字数: 6935字
• 语种: 中文

摘要

基于Hoare逻辑推理规则去验证程序安全性的研究是程序验证领域的重要发展方向.但是在Hoare逻辑中,仅依靠程序变量的断言语言无法表达程序上下文中不变性质.本文研究通过在断言语言中引入逻辑变量的方式来表达程序上下文不变性质,同时详细介绍了引入逻辑变量带来的问题以及给出解决问题的途径,最后以带逻辑变量的平衡二叉树插入程序为例展示了引入逻辑变量的作用.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈意云	中国科学技术大学计算机科学与技术学院	83	854	16.0	26.0
2	李为胜	中国科学技术大学计算机科学与技术学院	1	0	0.0	0.0