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