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