一个支持位运算形式化推理的抽象机

• 作者: 林春晓 陈意云 项森
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: 形式化方法 程序验证 Hoare逻辑 程序设计中的逻辑
• 年，卷（期）: 2007,（1）
• 所属期刊栏目: 软件技术
• 页码范围: 88-92
• 页数: 5页
• 分类号: TP301.2
• 字数: 6449字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-1220.2007.01.019

摘要

程序推理使用的抽象机器与物理机器的差距降低了推理的精确度,为了缩小这个差距,本文提出了一个带位级别抽象的新抽象机, 在这个机器里,二进制整数以纯语法的方式被表示成位矢量而不是非负整数.使用这个抽象机器,可以在其上进行许多带位操作指令的程序,特别是系统级代码的Hoare逻辑风格推理. 本文中,二进制整数及其上的算术逻辑运算使用Coq的归纳结构演算来形式化,并且一些常见的重要性质也都使用Coq证明助理进行了严格的形式化证明.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈意云	中国科学技术大学计算机系	83	854	16.0	26.0
2	项森	中国科学技术大学计算机系	4	13	2.0	3.0
3	林春晓	中国科学技术大学计算机系	5	20	2.0	4.0