欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
程序推理使用的抽象机器与物理机器的差距降低了推理的精确度，为了缩小这个差距，本文提出了一个带位级别抽象的新抽象机，在这个机器里，二进制整数以纯语法的方式被表示成位矢量而不是非负整数．使用这个抽象机器，可以在其上进行许多带位操作指令的程序，特别是系统级代码的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.
同期刊论文项目
同项目期刊论文
期刊信息
位置：