如今,形式化方法越来越多地被应用到与生命财产安全密切相关的计算机软件领域。其中,编程语言的形式化操作语义起着一个重要的作用,比起通常用自然语言描述的编程语言规范,形式化操作语义以数学的规范提供了一种更精确的描述方式。　　Lustre是一种并发的同步数据流语言,主要应用于嵌入式系统的软件开发。我们将形式化方法应用于Lustre到Clight的编译过程,Lustre-是由Lustre到Clight可信编译的一种中间语言,它是由Lustre语言的一个核心子集经过等式拓扑排序、对表达式列表的赋值进行拆分、等式化简、时态运算转化等变化后得到的顺序语言,它包括流、时钟、时态运算、node等核心概念。Lustre经过多步中间语言的转换翻译到Clight,并且通过定义每一步中间语言的形式语义,最终证明每一步翻译的语义保持性。其中,每一种中间语言的形式语义定义,直接关系到语义保持性的证明。　　本文主要研究Lustre-的形式化操作语义定义及其性质,以严格的数学规范定义了Lustre-的执行环境、格局和语义规则,讨论并证明了语义的确定性,并对于给定的程序,定义了由该程序确定的一个更为精确的格局集合,并在此基础上讨论并证明了语义的终止性。