论文部分内容阅读
Lustre是一种广泛应用于工业界核心安全级控制系统的同步数据流语言，采用形式化验证的方法实现Lustre到C的编译器可以有效地提高编译器的可信度．基于这种方法，开展了从Lustre^＊（一种类Lustre语言）到C子集Clight的可信编译器的研究．由于Lustre^＊与Clight之间巨大的语言差异，整个编译过程划分为多个层次，每个层次完成特定的翻译工作．阐述了其中高阶运算消去的翻译算法，翻译过程采用辅助定理证明工具Coq实现，并进行严格的正确性证明．