关键词：定理证明器Coq;机械验证;堆栈;函数式语言
摘 要：软件的可靠性和可信性越来越受到人们的关注,而编译器作为软件开发的基础,其正确性的验证一直都是个重要且迫切的问题.设计和实现一个小型命令式语言IMP的编译器,该编译器将IMP源代码转换成定理证明器Coq接受的函数式语言表示形式的代码,通过语义分析得到IMP目标代码,在堆栈中执行得到结果.本文的重点是使用交互式定理证明器Coq机械验证函数式语言表示形式的源代码编译执行前后的属性和行为均保持一致.本文的工作为使用堆栈的编译器和其他软件系统的机械化形式验证提供了一种新的思路和方法.
内 容：原文可通过湖北省科技信息共享服务平台（http://www.hbstl.org.cn)获取