论文部分内容阅读
为解决实现同步数据流语言Lustre到串行命令式语言c语言可信编译器过程中碰到的时态运算翻译的困难，提出了将所有的时态运算翻译单独分层定义和证明的方法。在同步数据流语言的时态特性和C语言的循环特性分析的基础上，结合可信编译器实现框架上下层的语言结构，使用Coq证明工具，形式化的定义了两种中间语言的语法和语义，经过分析时态翻译过程特点，归纳定义了时态变量传递性质，实现了翻译工作严格的形式化验证，最终完成了时态消去翻译的等价性证明。