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

【Abstract】 To solve the problem of the translation of temporal operation in implementing the trustworthy compiler which translates synchronous date-flow language Lustre to imperative serialization language C,a method defining all the translation of temporal operation into new layer and proving it independently is proposed.Based on the analyzing of property of synchronous dateflow language and C language,according to the neighbors layer in implementation of trustworthy compiler,the Coq proof assistant is used to formally define syntax and semantics of two intermediate languages,after analyzing the translation of temporal operation,the transitivity property of temporal variable is defined inductively,the translation is formally verified,the equivalence property of translation of temporal features eliminating is proved.更多还原