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

【Abstract】 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 bit-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.更多还原