一种适用于可信编译器的源语言转换与检查框架  

A source language transformation and inspection framework for trusted compilers

作　　者：张晓曈 何炎祥[1,2] 

机构地区：[1]武汉大学计算机学院,武汉430072 [2]武汉大学软件工程国家重点实验室,武汉430072

出　　处：《中国科技论文》2017年第14期1646-1650,共5页China Sciencepaper

基　　金：国家自然科学基金资助项目(91118003;61373039);高等学校博士学科点专项科研基金资助项目(20130141110025)

摘　　要：针对当前可信编译器对源语言处理能力的局限,提出了1个适于可信编译器的源语言转换与检查框架,将命令式源语言程序转换为可信编译器可接受的等价的函数式语言程序,通过语法支持、良构性和异常发生三方面的检查,保证了可信编译器对转换后的代码的可接受性以及代码本身较高的可信性。Aiming at the limitation of processing capacity on source language,a trusted compiler-oriented framework is proposedfor source code transformation and inspection.It can convert an imperative programming language program to the equivalent functional programming language program that is acceptable to trusted compiler.Through three verifications,including syntax support check,well-formedness check and exception,this frame can ensure the acceptability and the comparatively high credibility of the source code.

关 键 词：编译验证 可信编译器 代码转换 操作语义 

分 类 号：TP314[自动化与计算机技术—计算机软件与理论]