| 一个支持位运算形式化推理的抽象机 |
| |
| 引用本文： | 项森,陈意云,林春晓.一个支持位运算形式化推理的抽象机[J].小型微型计算机系统,2007,28(1):88-92. |
| |
| 作者姓名： | 项森 陈意云 林春晓 |
| |
| 作者单位： | 中国科学技术大学,计算机系,安徽,合肥,230026 |
| |
| 摘 要： | 程序推理使用的抽象机器与物理机器的差距降低了推理的精确度,为了缩小这个差距,本文提出了一个带位级别抽象的新抽象机,在这个机器里,二进制整数以纯语法的方式被表示成位矢量而不是非负整数.使用这个抽象机器,可以在其上进行许多带位操作指令的程序,特别是系统级代码的Hoare逻辑风格推理.本文中,二进制整数及其上的算术逻辑运算使用Coq的归纳结构演算来形式化,并且一些常见的重要性质也都使用Coq证明助理进行了严格的形式化证明.
|
| 关 键 词： | 形式化方法 程序验证 Hoare逻辑 程序设计中的逻辑 |
| 文章编号： | 1000-1220（2007）01-0088-05 |
| 修稿时间： | 2005-10-10 |
Abstract Machine Supporting Bit Arithmetic Reasoning |
| |
| XIANG Sen,CHEN Yi-yun,LIN Chun-xiao.Abstract Machine Supporting Bit Arithmetic Reasoning[J].Mini-micro Systems,2007,28(1):88-92. |
| |
| Authors: | XIANG Sen CHEN Yi-yun LIN Chun-xiao |
| |
| Affiliation: | Department of Computer Science, University of Science and Technology of China, Hefei 230026, China |
| |
| Abstract: | |
| |
| Keywords: | formal method program verification hoare logic logic in programming |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
