基于Coq的命令式语言编译器机械验证的研究与实现

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