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

Research and Implementation of the Mechanization Verification of a Coq-based Imperative Language Compiler

作　　者：盛枫[1] 窦亮[1] 杨宗源[1] 

机构地区：[1]华东师范大学计算机科学与技术系,上海200241

出　　处：《小型微型计算机系统》2015年第9期1927-1931,共5页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(61070226)资助

摘　　要：软件的可靠性和可信性越来越受到人们的关注,而编译器作为软件开发的基础,其正确性的验证一直都是个重要且迫切的问题.设计和实现一个小型命令式语言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.

关 键 词：定理证明器Coq 机械验证 堆栈 函数式语言 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]