中文摘要：

与传统的高级语言程序验证相比，汇编代码验证中所需要的形式规范往往比较复杂，通常的做法是要求程序员手写形式规范，或是牺牲形式规范的表达能力以期能够自动生成规范．本文提出一种能够自动生成形式规范的方法，该方法依托一个出具证明的编译器自动生成汇编级形式规范，从而减轻程序员的负担．使用该方法生成的规范比现有的其他方法自动生成的规范具有更强的表达能力．文章主要描述该方法在出具证明编译器中的实现．

英文摘要：

The formal specifications in assembly code certification are usually complicated. Some specifications can be automatically generated, but usually lack for expressiveness. Others are too complex to be generated automatically. Such specifications are usually written by programmers and they are a big burden on programmers. This paper presents a method for generating formal specifications automatically. It uses a certifying compiler to generate formal specifications for assembly code, so that programmers are freed from writing specifications for assembly code. The generated specifications are more expressive than those generated automatically by other existent methods. This paper mainly describes the implementation of this method in a certifying compiler.