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

Abstract Machine Supporting Bit Arithmetic Reasoning

作　　者：项森[1] 陈意云[1] 林春晓[1] 

机构地区：[1]中国科学技术大学计算机系,安徽合肥230026

出　　处：《小型微型计算机系统》2007年第1期88-92,共5页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(60473068)资助.

摘　　要：程序推理使用的抽象机器与物理机器的差距降低了推理的精确度,为了缩小这个差距,本文提出了一个带位级别抽象的新抽象机,在这个机器里,二进制整数以纯语法的方式被表示成位矢量而不是非负整数.使用这个抽象机器,可以在其上进行许多带位操作指令的程序,特别是系统级代码的Hoare逻辑风格推理.本文中,二进制整数及其上的算术逻辑运算使用Coq的归纳结构演算来形式化,并且一些常见的重要性质也都使用Coq证明助理进行了严格的形式化证明.The gap between the physical machine and the abstract machine used in program reasoning reduces the accuracy of reasoning. In order to shorten this gap, a new abstract machine with blt-level abstraction is proposed, in which the binary integers are represented as bit vector in syntactic approach instead of non-negative integer number. With this new abstract machine, many programs with bit operation instructions, especially system-level codes, can be reasoned using Hoare Logic. In this paper, the binary integer along with its arithmetic and logic operations are formalized in Coq＇s Calculus of Inductive Construction, and many important properties are also formally proved in Coq proof assistant.

关 键 词：形式化方法 程序验证 HOARE逻辑 程序设计中的逻辑 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]