摘要
程序推理使用的抽象机器与物理机器的差距降低了推理的精确度,为了缩小这个差距,本文提出了一个带位级别抽象的新抽象机,在这个机器里,二进制整数以纯语法的方式被表示成位矢量而不是非负整数.使用这个抽象机器,可以在其上进行许多带位操作指令的程序,特别是系统级代码的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.
作者
项森
陈意云
林春晓
XIANG Sen;CHEN Yi-yun;LIN Chun-xiao(Department of Computer Science,University of Science and Technology of China,Hefei 230026.China)
出处
《小型微型计算机系统》
CSCD
北大核心
2007年第1期88-92,共5页
Journal of Chinese Computer Systems
基金
国家自然科学基金项目(60473068)资助.
