中文摘要：

软件的可靠性和可信性越来越受到人们的关注,而编译器作为软件开发的基础,其正确性的验证一直都是个重要且迫切的问题.设计和实现一个小型命令式语言IMP的编译器,该编译器将IMP源代码转换成定理证明器Coq接受的函数式语言表示形式的代码,通过语义分析得到IMP目标代码,在堆栈中执行得到结果.本文的重点是使用交互式定理证明器Coq机械验证函数式语言表示形式的源代码编译执行前后的属性和行为均保持一致.本文的工作为使用堆栈的编译器和其他软件系统的机械化形式验证提供了一种新的思路和方法.

英文摘要：

The reliability and credibility of softw are is getting more and more attention. As the basis for softw are development,the compiler＇s verification has alw ays been an important and urgent issue. In this paper,w e design and implement a small imperative language IM P compiler,w hich translates source code into the code in the form of functional language that the theorem prover Coq is acceptable to. The code represented by functional language is translated into the IM P object code by using semantic analysis and gets results in a stack. The focus of this paper is to use the interactive theorem prover Coq mechanically verifying properties and behavior of the source code,w hich is represented by functional language,are consistent before and after the execution. This paper provides a new method for mechanization validation of compiler and other softw are systems using stack.