一种基于形式化验证的同步数据流程序的可信排序方法

摘要

本发明公开一种基于形式化验证的同步数据流程序的可信排序方法，包括Lustre并行程序和由Lustre并行程序排序后得到的串行C程序，通过对任意两个满足拓扑排序的Lustre程序，证明其拓扑排序前的Lustre程序和拓扑排序后的Lustre程序执行语义等价，得到排序后的C程序与排序前的Lustre程序在语义上执行等价。本发明以“入度为零的顶点拓扑排序算法”为理论基础，基于形式化语言进行开发实现，通过对任意两个满足拓扑排序性质的程序在串行语义中执行是等价的证明，在形式化验证时考虑了并行语言在转化成串行语言过程中的所有情况，并分别对每种情况都做了证明，得到排序后的程序满足拓扑排序的性质，从而保证方案的正确性，提高整个软件系统的安全性和可靠性。

说明书

技术领域

本发明涉及计算机安全领域，具体涉及针对编译器的安全性而利用形式化验证的同步数据流程序的可信排序方法。 

背景技术

随着计算机技术越来越多地应用于航空航天、核电、高速铁路等安全关键系统(SCS，Safety-Critical System)，对其系统中核心软件的安全性要求也越来越高。安全关键系统中的丝毫错误都可能引发巨大的灾难，如何为安全关键系统构造一个基础的安全软件环境是需要面对的首要问题，尤其是对操作系统、编译器等基础核心软件。 

编译器的可信性很早就受到学术界和工业界的重视，从McCarthy和Painter的开创性工作开始，如何提高编译器正确性和可靠性一直是计算机科学研究领域的热点；但一致进展缓慢，在工业界的应用有限。最有突破性进展的是Xavier Leroy等人基于Coq辅助定理证明工具研究开发的Compcert编译器，它是一个完整的使用形式化方法证明了产生的可执行代码的行为与源程序的语义完全保持的C编译器，得到了业界的广泛认可。 

我国经济高速发展，对能源的需要日益高涨，尤其是对新能源的需求。因此核电站在我国将迎来快速发展。Lustre是一种同步数据流语言，主要用于核电、航空航天等高可信要求的工业自动化领域中。 

需要将Lustre程序转换成相应环境下的语言，如将Lustre转换为C代码。这个转换目前大多使用国际著名工具SCADE来将Lustre编译成C代码。Scade是目前为止最成熟的Lustre编译器，它已通过了多个工业标准的安全级认证，其代码生成器KCG获得了民用航空软件生产许可。在因果分析时它只在静态语义层面进行检查，通过模块化和独立编译以及更严格地定义依赖关系来解决因果分析的问题。它禁止node的输入依赖于node的输出，从而使每个node能够单独编译。SCADE工具虽然已通过多个安全级工业标准的认证，但它是通过大规模测试来保证其安全性，未经过严格的形式化验证。由于测试无法做到完全覆盖，故未经验证的编译器中隐藏的误编译错误很难被发现。另一方面，SCADE是商业公司推出的软件产品，相关技术细节没有公开，很难了解到为提升软件的可靠性和可信性在哪些方面做了技术性工作。 

此外在对编译器的验证方面，目前还有如下一些方式：CompCert项目实现了C的子集Clight到汇编的翻译过程，并用交互式定理证明器证明每个步骤在对应的语义中执行等价。相比普通的验证技术，形式化验证能在数学的层面对软件的逻辑进行抽象和证明，因此具备更高的安全性，Compcert项目虽然利用形式化验证技术对部分子模块进行验证，但是其实现的是串行语言（C语言）到串行语言（汇编语言）的转换，并不适用于并行语言（Lustre语言）到串行语言（C语言）的转换。Mike Gemunde等通过模型检查的方式对Lustre程序进行因果分析。他建立了一个形式化的因果分析定义并能够保守迅速地检查系统中的因果循环。模型检查的方式相对于基于语义的形式化验证还是有局限性。A.Bertails等用形式化验证的方法完成了对Lustre程序的类型检查和时钟演算的验证，准备开始因果分析工作和后续的翻译工作，到目前为止还未完成。他们虽然准备通过形式化验证的方式来进行因果分析，但验证还是停留在语法层面，并未在语义执行的层面进行验证，而且后续到C的翻译工作也还没有完成。 

为有效提高编译器的可靠性，系统中每个环节的可靠性都不容忽视，将同步数据流语言的程序转换为串行C语言程序是L2C编译器的重要组成部分。这一功能是为了保证两个程序执行的功能是相同的，保证程序的正确逻辑。 

发明内容

为解决现有技术中在对Lustre程序转换为C语言程序时无法验证编译器安全性的问题，本发明提供一种形式化验证的同步数据流程序的可信排序方法。具体方案如下：一种基于形式化验证的同步数据流程序的可信排序方法，包括Lustre并行程序和由Lustre并行程序排序后得到的串行C程序，其特征在于，包括如下步骤： 

步骤1、将源Lustre程序利用词法语法分析工具进行分析，得到该Lustre程序的抽象语法树，利用基于形式化方法的验证工具Coq对所得抽象语法树进行类型分析和静态语义检查，得到符合well-typed条件的抽象语法树Lustre-W； 

步骤2、对Lustre-W中所有变量的时钟周期进行归一化处理，使所有变量的时钟周期统一于标准周期； 

步骤3、对归一化后的Lustre-W进行因果分析和拓扑排序、翻译后生成串行C程序； 

步骤4、对任意两个满足拓扑排序的Lustre程序，证明其拓扑排序前的Lustre程序和拓扑排序后的Lustre程序执行语义等价，验证过程如下： 

（1）首先建立Lustre并行程序中存储node名称的全局环境和存储各node函数执行周期 中变量的局部环境，同时确保全局环境中node的名称不重复和局部环境中等式左值ID不为空； 

（2）建立一个与验证程序A的全局环境相同且与验证程序B的局部环境相同的验证程序C； 

（3）利用验证程序A和验证程序C中node名一一对应的方式，可得到两者执行后语义等价的结果； 

（4）以验证程序C为基础，以仅有一步为区别的方式细化出中间验证程序C1、C2、C3……Cn，其中验证程序Cn与验证程序B仅有一步区别，对比两个程序执行后其局部环境的值可得到两者语义执行是否等价的结果，再依次反推直至得到验证程序C和验证程序B之间语义执行是否等价的结论； 

（5）结合（3）和（4）的结果，得到拓扑排序前的Lustre程序和拓扑排序后的Lustre程序执行语义等价的结论； 

步骤5、由此得到Lustre程序和其经过因果分析和拓扑排序后生成的C程序在执行语义上是等价的证明。 

优选的：在步骤1的Coq静态语义检查中，通过分析node列表中不存在依赖环能够证明node列表在拓扑排序前后相互是同一个排列，其证明过程包括如下步骤： 

（1）首先证明拓扑排序前后的Lustre程序中“入度为零”的node名都是同一个排列； 

（2）然后证明拓扑排序前后的Lustre程序中具有依赖关系的node名都是同一个排列； 

（3）最后证明将上述两种结构合并到一起后的node列表的全局环境和局部环境与拓扑排序前相互是一个排列。 

优选的：所述步骤2中的归一化处理是指，将所有不同长度的时钟周期按其中最快的时钟周期为单位进行拆分，然后按进行周期划分所有的变量。 

优选的：所述步骤4的（4）中，所述验证程序Cn与验证程序B仅有一步区别包括四种类型： 

（1）这个区别点是主node； 

（2）这个区别点不是主node； 

（3）区别点是主node时，执行的两个主node不相等，即两个主节点的等式列表互相是一个排序，但其他信息相同； 

（4）区别点是主node时，两个主node所处的主节点位置不同，且两个主节点的全局环境也不同； 

针对上述区别，再次对其化简，使最终的区别点统一为：不同主node下两个不相依赖的等式。 

优选的：中两个不依赖的等式根据其中是否有call表达式，分为下面三种情况分别进行证明： 

（1）两个等式中都没有call表达式； 

（2）两个等式中有一个有call表达式； 

（3）两个等式都有call表达式。 

本发明以“入度为零的顶点拓扑排序算法”为理论基础，基于形式化语言进行开发实现，最后用形式化验证的方法对系统设计模型进行验证。形式化验证能在数学的层面对软件的逻辑进行抽象和证明，因此具备更高的安全性。本发明通过对任意两个满足拓扑排序性质的程序在串行语义中执行是等价的证明，在形式化验证时考虑了并行语言在转化成串行语言过程中的所有情况，并分别对每种情况都做了证明，得到排序后的程序满足拓扑排序的性质，从而保证方案的正确性，提高整个软件系统的安全性和可靠性。 

附图说明

图1本发明的工作过程示意图； 

图2本发明的证明过程流程图； 

图3本发明中环境结构示意图； 

图4本发明中等式间依赖关系示意图； 

图5本发明中元素和集合的示意图； 

图6本发明中元素和集合的化简示意图； 

图7本发明中元素和集合的另一化简示意图； 

图8本发明中元素和集合的另一化简示意图； 

图9本发明中元素和集合的另一化简示意图； 

图10本发明中元素和集合的另一化简示意图； 

图11本发明中元素和集合的另一化简示意图； 

图12本发明的拓扑排序分解证明示意图； 

图13本发明的拓扑排序分解证明另一示意图； 

图14本发明的拓扑排序分解证明另一示意图； 

图15本发明的拓扑排序分解证明另一示意图； 

图16本发明的拓扑排序分解证明另一示意图。 

具体实施方式

由于Lustre是同步数据流语言，是在无限周期中进行计算，具有复杂多变的时钟演算和计算历史流数据的时态运算，其程序与C程序差异太大，直接将其翻译到C，转换过程十分复杂，验证起来也会非常困难，本发明将整个转换过程分为多步执行，每一步只做一个类型的化简，并将其化简的结果称之为中间语言，保持每步之间的相互独立，便于协作开发和提高效率，同时也简化了形式化验证的难度。 

如图1所示，101、本发明的基于形式化验证的同步数据流程序的可信排序方法，包括Lustre并行程序和由Lustre并行程序排序后得到的串行C程序； 

如图2所示，102、将源Lustre程序利用词法语法分析工具进行分析，得到该Lustre程序的抽象语法树，利用基于形式化方法的验证工具Coq对所得抽象语法树进行类型分析和静态语义检查，得到符合well-typed条件的抽象语法树Lustre-W； 

本发明中对于Lustre语言的词法语法分析采用行业认可的词法语法分析工具Flex和Bison对Lustre语言进行分析，得到Lustre语言的抽象语法树，由于该步骤相对简单且在现有技术中已经有严格的规则进行约束，故这里没有再进行形式化验证。 

Lustre程序的抽象语法树分为：programS、nodeS、equationS和exprS四个层次；分别对应程序、节点、等式和表达式；其中 

programS表示整个程序，由类型定义列表、nodeS列表和主node的id三部分组成。程序执行时会通过主node的id定位nodeS列表中的主node，并执行主node。 

nodeS为Lustre程序的程序执行节点，相当于C程序的函数。nodeS主要由node名、输入参数、输出参数、局部变量和equationS列表五部分构成。 

equationS为等式，由左值列表lhsl和表达式exprS两部分组成。每个等式都相当于是给一个或者多个左值赋值，每个变量最多被赋值一次。 

exprS为表达式，分为：表达式列表、call表达式、一元操作表达式、二元操作表达式、时态操作表达式、原子表达式和普通表达式。为简化排序的证明，做排序前已经对时态表达式进行了处理，使得时态表达式的子表达式只能是原子表达式。 

Lustre程序的抽象语法树构建在形式化验证和开发工具Coq中，现有技术中已经用形式化语言实现了对其形式化的描述，在此不再赘述。 

对生成的语法树，在Coq中进行静态检查，检查的内容分为两部分，一是检查语法树中 的类型，以得到Well-typed的抽象语法树Lustre-W，并证明整个过程；二是检查后续翻译证明中所需的性质是否得到满足，并证明这些性质。 

Coq静态语义检查中通过分析node列表中不存在依赖环，证明node列表在拓扑排序前后相互是同一个排列，其证明过程包括如下步骤： 

（1）首先证明拓扑排序前后的Lustre程序中“入度为零”的node名都是同一个排列； 

（2）然后证明拓扑排序前后的Lustre程序中具有依赖关系的node名都是同一个排列； 

（3）最后证明将上述两种结构合并到一起后的node列表的全局环境和局部环境与拓扑排序前相互是一个排列。 

具体的实例如下： 

这一部分主要利用Coq库中List数据结构有关Permutation和map的基本性质来证明，因为排序的过程是多个步骤的嵌套，直接进行归纳证明比较难，而利用List的性质可以化简排序的步骤，简化证明。证明过程惟一的难点在于证明对依赖关系的排序前后是个排列，因为不能直接对依赖关系列表作归纳来证明，需要先对辅助参数len做elim归纳，再对依赖关系列表l作归纳。 

Theorem toposort_depList_permutation:forall(len:nat)(l:list dependT), 

length l<=len→ 

Permutation l(toposort_depList len l). 

其中，Permutation l是Coq库中List数据库提供的相关定义。 

103、对Lustre-W中所有变量的时钟周期进行归一化处理，使所有变量的时钟周期统一于标准周期； 

由于Lustre语言是同步数据流语言，程序在无穷周期中执行。每个变量都有一个时钟，在无穷周期中为一个无限时钟流。时钟在每个周期中的值为VtrueL或VfalseL，变量在时钟的值为VtrueL时才有值。这种复杂的时钟如果带入后续验证步骤，不但使后续的语义变得非常复杂，还将使后续证明难度增大。本发明先将携带普通时钟的Lustre-W程序经过翻译转换成只携带全局基本时钟（每个周期时钟都为VtrueL）的Lustre-K程序，以有效简化后续的翻译和验证工作。其具体作法是，根据时钟的长度1秒、2秒、3秒……，最终以基本时钟为标 准，一般是最快的时钟作为标准，如以1秒为标准，而2秒、3秒……则被分成相应的多个1秒，经过化简后，全局时钟每个周期都是VtureL，程序中每个周期都进行运算，因此时钟归一化后的程序已不需要时钟的概念，可大大简化后续证明的难度。 

104、对归一化后的Lustre-W进行因果分析和拓扑排序、翻译后生成串行C程序； 

Lustre程序是并发执行的，所以将其翻译到C程序之前先要对well-typed Lustre-W进行因果分析和拓扑排序，以将其串行化，最后再对整个过程进行可信的形式化证明。拓扑排序的过程是指在任意两个满足拓扑排序的程序执行等价。而C语言需要的是一个经过分析变量之间的依赖关系的串行程序，通过对Lustre程序的中各node之间的依赖关系分析，根据设定的标准，按不同node之间依赖关系的大小进行排序，其中入度为零的无依赖关系的node放置在程序的前面。在符合拓扑排序关系定义的情况下，无依赖关系的node列表满足拓扑排序关系；如果一个node的依赖关系不依赖自身以及后续所有的依赖关系列表，且后续的依赖关系列表满足拓扑排序关系，那么这个node和具有依赖关系的node列表之间也满足拓扑排序的关系。 

在证明过程中，先证明经过因果分析检查的程序的依赖关系列表中不存在环，再证明无环的依赖关系列表满足拓扑排序的定义。如图4所示，如果依赖关系D1的右值的id列表存在于依赖关系D2的左值的id列表中，说明D1依赖D2，然后递归的定义拓扑排序的关系。图4中是否存在从依赖关系x到y的依赖路径，如果x依赖于l中的第一个元素，l中的每一个元素又依赖于其后续的元素，l的最后一个元素又依赖y，则存在依赖路径；只要整条路径中有一个元素不依赖于其后续的元素，则不存在依赖路径。依赖路径主要是用于表示拓扑关系图中的一条路径，存在路径，就是在图中从x到y有通路l。相应程序代码如下： 

无环的定义即对图4中的任意x和l的任意子集l'，都不存在一条x通过l'到x自身的依赖路径。即在拓扑关系图中，从任意点x出发，都不能回到原点x。 

Definition no_cycle(l:list dependT):= 

forall(x:dependT)(l':list dependT), 

In x l→incl l'l→is_path x x l'=false. 

直接证明无环的依赖关系列表满足拓扑排序的定义，难度比较大，因为这两个定义都比较抽象，且是对依赖关系图的性质的不同类型的定义。故需要将无环的性质进行一步转换，证明这一步转换，再将转换后的目标作为新的前提来证明最后的目标。下面的证明就是第一步转换所要证明的命题，即对任意无环且不为空的依赖关系列表l，必能将其分为l1和l2两部分，其中l1不为空且不依赖于l中的任意元素；在l2中，对于任意元素x，存在依赖关系l1中的依赖关系y和l2的子集依赖关系列表l'，x通过l'存在到y的依赖关系路径。简单来说就是任意无环的且不为空依赖关系列表总能分为两个集合，一个集合不为空且其元素都是不依赖所有元素的依赖关系图中的叶子节点；另一个集合中的所有元素都能找到一条到第一个集合的依赖路径。代码如下： 

虽然经过了分拆简化，nocycle_infer的证明依然比较复杂，需要先进行归纳证明，再进一步分情况讨论来证明。先对依赖关系列表l作归纳证明，当l为空时，前提矛盾可直接证明；当依赖关系列表为一个元素a和一个列表l的组合时，l可分为l1和l2两个子集，l1和l2满足要证的性质，l1中的元素不依赖于l1和l2中的任何元素，对于l2中的任意元素x，其存在到l1的依赖路径；下面就要证加上元素a，也满足性质。 

如图5所示，为了分情况讨论，可以根据集合l1中元素和a的关系，将l1分为三个子集。子集la中的所有元素依赖a，但a不依赖子集la中的元素；a依赖子集lb中的所有元素，但子集lb中的所有元素不依赖a；子集lc中的元素和a互相都不依赖。根据la，lb和lc是否为空可以分成7种情况来证明。 

(1)if la<>nil and lb=nil and lc=nil then exists(a::nil)(la++l2)。 

如图6所示，只有la不为空，lb和lc为空，则元素a组成新的l1，la和l2组成新的l2。 

(2)else if la=nil and lb<>nil and lc=nil then exists lb(a::l2)。 

如图7所示，只有lb不为空，则集合lb组成新的l1，a和l2组成新的l2。 

(3)else if la=nil and lb=nil and lc<>nil 

如图8所示，只有lc不为空，情况比较复杂。则需再判断元素a是否依赖集合l2，如果元素a不依赖集合l2，则元素a和集合lc组成新的l1，l2组成新的l2；如果元素a依赖集合l2，则集合lc组成新的l1，元素a和l2组成新的l2。 

(4)else if la<>nil and lb<>nil and lc=nil then exists lb(a::la++l2)。 

如图9所示，la和lb都不为空，则集合lb组成新的l1，a、la和l2组成新的l2。 

(5)else if la=nil and lb<>nil and lc<>nil then exists(lb++lc)(a::l2)。 

如图10所示，lb和lc都不为空，则集合lb和lc组成新的l1，a和l2组成新的l2。 

(6)else if la<>nil and lb=nil and lc<>nil then。 

如图11所示，la和lc都不为空，情况比较复杂，则需再判断元素a是否依赖集合l2，如果元素a不依赖集合l2，则元素a和集合lc组成新的l1，la和l2组成新的l2；如果元素a依赖集合l2，则集合lc组成新的l1，元素a、la和l2组成新的l2。 

(7)else if la<>nil and lb<>nil and lc<>nil then exists(lb++lc)(a::la++l2) 

当la、lb和lc都不为空的情况，如图5所示，则集合lb和lc组成新的l1，a、la和l2组成新的l2。 

通过归纳和分情况讨论证明分拆证明的第一步，就可以利用第一步的结论证明下面的定理。只要l是非空、不重复且无环的，那至少可以从l的拓扑关系图中找到一个不依赖任何元素的叶子节点。通过这个结论可以证明如果l是非空、不重复且无环的依赖关系列表，则“入度为零的顶点拓扑排序算法”的第一步肯定能够扫描出入度为零的元素，即肯定能将原有列表l分拆成l1和l2两个子集，l1子集不为空。 

再通过get_nodep_List_notnill的性质，就能证明无环且不重复的依赖关系列表l，经过大于其长度的len次的迭代排序后，得到的新的依赖关系列表是满足拓扑排序关系的。 

因为排序的过程不是随着依赖关系列表的长度线性下降的，一次扫描至少找到一个叶子节点，也可能找到多个，故最多经过列表长度的次数，就能完成拓扑排序。这时我们定义排序的次数len作为辅助参数，排序的过程是根据排序次数线性下降的，这个辅助参数为自然数，带入值为排序可能的最大次数。这种证明比较特殊，不能用一般的归纳方式进行证明。需要先用elim策略对辅助参数进行归纳，当辅助参数为0时，可直接证明；当辅助参数不为0时，就能利用归纳得到的条件。在第二种情况再对依赖关系列表l用induction策略作归纳，当l为空时，可以直接证明；当l为a和新的l的组合时，利用get_nodep_List_notnill的性质就能得到a和l的组合经get_nodep_List一步扫描后得到的l1不为空。 

(l1,l2)=get_nodep_List idll(a::l) 

然后就能利用对len归纳所得到的条件进行证明，并构造出该条件所需的前提，就能完成toposorted_depList的证明。 

最后一步还需证明分别对节点列表和节点内的等式列表进行排序后，其依赖关系列表满足拓扑排序性质。先证明抽取节点列表调用关系的依赖关系列表并对其进行排序，排序后的依赖关系列表满足拓扑排序的性质。 

Theorem nodes_toposorted: 

is_nodes_toposorted 

progT.(nodeBlockS)(toposort_nodes progT.(nodeBlockS))). 

再证明对程序中的任意节点，对其等式列表进行拓扑关系抽取后排序，排序后的依赖关系列表满足拓扑排序的性质。 

Theorem eqs_toposorted: 

forall node,In node progT.(nodeBlockS)→ 

is_eqs_toposorted(eqsOfNodeS node)(toposort_eqs(eqsOfNodeS node)). 

这两个定理的证明比较类似，因为默认的依赖关系抽取需要加入序号，故不能利用map来简化抽取的过程，但序号只是在排序过程中使用，而排完序后在证明其满足拓扑排序的性质时，并不需要序号。故可先证明经两种方式获取的依赖关系列表，如果其中一种满足拓扑排序的性质，那另一种也必满足。即可将抽取的过程转换为利用map的简单方式，就可以利用map的性质进行化简，从而最终证明上面的两个定理。 

105、对任意两个满足拓扑排序的Lustre程序，证明其拓扑排序前的Lustre程序和拓扑排序后的Lustre程序执行语义等价； 

由于Lustre是一种同步数据流语言，有复杂的时态运算，故普通的方法，难以保证排序的正确性，我们将用Coq定义拓扑排序的性质，证明排序后的C程序满足拓扑排序的性质，并证明任意两个满足拓扑排序性质的Lustre程序在串行语义中执行是等价的，从而可以证明经过排序的并行程序和串行程序之间在实际执行过程中语义的等价性。验证过程如下： 

501、首先建立Lustre并行程序中存储node名称的全局环境和存储各node函数执行周期中变量的局部环境，同时确保全局环境中node的名称不重复和局部环境中等式左值ID不为空；建立一个由左值ID构成的等式子环境； 

在进行环境的定义时，可以基于以下两条性质： 

性质1：node列表的标识id不重复，保证调用node时读取全局环境最多只能找到一个对应的node。这个性质既可以保证调用node时读取全局环境的唯一性，也可以简化全局环境的定义。 

性质2：对于任意node，其等式列表的左值id不为空且不重复。这个性质非常重要，它首先保证了Lustre程序的基本性质：对于node中的等式，每个左值id只被赋值一次，通过这个基本性质，排序和证明都得以大大简化；另一方面，在构造局部环境时，又大有用处，可以以每个等式左值的第一个id作为标识来定位等式环境，从而大大简化环境匹配的定义和证明。 

上述两条性质是Coq在步骤101中对语法树进行静态检查时要验证的，同时这两条性质也是Lustre程序在转化成语法时必须满足的两个条件。 

Lustre语言的运行环境分为两部分：全局环境和局部环境。全局环境用于存储node列表，在node调用时需要读取全局环境并根据node名调用对应node。局部环境用于存储每个周期的每个node中的每个变量的值。以下所提环境均是进行拓扑排序时运行的全局环境和局部环境。 

因为对全局环境的操作比较简单，一是初始化阶段读取整个node列表，二是执行node调用时读取对应node。因为Coq的静态检查保证了所有node的名字不重复，并且已经将全局常量代入语法树，这就能够以最简单的方式定义全局环境。本发明义全局环境为一个node的列表。初始化时，将要执行程序的node列表赋值给全局环境。在执行过程中，需要调用node时再根据node名在node列表中搜索对应的node并执行,因为在Coq库中已经有很多证明过的List的性质，所以直接采用List来描述全局环境能起到简化证明的作用。 

根据Lustre的语言特点以及要证明的目标来说。语义的局部环境定义比较困难，从语言特点上来说：一是因为Lustre是流语言，局部环境需要存储node中每个变量在每个周期的值，所以局部环境需要以周期为轴呈线性结构；二是因为node是call的存在，每个node在执行时又可能调用多个子node，所以每个周期的局部环境又呈树状结构。 

由于要证明的最终目标是任意两个满足拓扑排序的程序语义执行等价。如：对于任意两个满足拓扑排序的Lustre程序PorgA和PorgB，其每个对应的nodeX和nodeY的等式列表互相是一个排列但顺序不同。这就使得nodeX和nodeY要调用的子node的顺序是不同的。从而任意周期n的ProgA和ProgB的局部环境的语法树每一层的节点都互相是一个排列。这种情况下使得证明过程的环境匹配描述起来非常复杂，证明的复杂度也增加很多。由于对每个node的等式列表排序是以等式为单位的，且Coq的静态检查已经保证了node中每个等式的左值id是不重复的。因此本发明把每个node的环境构造成双层树结构，在node环境中增加等式环境，每个等式环境以等式对应的第一个左值id为标识，在执行每个等式中的Call时先搜索对应等式子环境，再按顺序找对应子node的环境，通过这样的构造使得PorgA和PorgB可以在相同的环境中运行，大大的降低了证明的复杂度。 

对于每个node中变量的存储，我们借鉴CompCert中的数据结构PTree，一是因为PTree满足局部变量存储的要求，保证不同变量之间互不干扰，且读取写入方便，能存储复杂的数据信息；二是因为CompCert中已经包含关于PTree的各种基本性质的证明，使用它可以减少很多重复性的工作。图3为LsemT局部环境示意图，node A中有两个等式eq1和eq2，eqid1为eq1的左值列表的第一个id，eqid2为eq2的左值列表的第一个id，等式eq1调用node B和node C，等式eq2调用node B两次。其中e表示局部环境，te为node对应的本地环境的列表（用list PTree表示），eqenv为等式环境。一个e分为te和eqenv列表两部分；一个eqenv由一个等式id标识和一个e的列表组成。上述内容在对应局部环境Coq中的定义，先用PTree定义一个局部环境的节点，用于保存一个周期里node运行期间所有变量的值； 

Definition localenvL:=PTree.t(valL*typeL). 

再用递归的方式按两层架构定义整个局部环境。 

502、建立一个与验证程序A的全局环境相同且验证程序B的局部环境相同的验证程序 C； 

证明过程中有两点需要重视：一是证明过程的拆解，两个满足拓扑排序的程序差异太大，无法直接证明，本发明将证明过程拆解为多步，每一步只对证明环节中的某一项做变化，其他不变，这样就把一个非线性的问题转化成多个线性的问题；二是每一步的环境匹配的定义，证明的核心就是比较两者在语义中执行的值，而这些值存储在局部环境中，所以最终是比较程序执行后局部环境的值，所以每一步的环境匹配定义直接关系到该部分的证明的难度。 

如图12所示，假设P1（验证程序A）和P3（验证程序B）是两个满足拓扑排序关系的程序，由于node列表的顺序不同且每个node中的等式的顺序也不同，无法直接证明P1和P3在语义中执行等价。本发明把证明过程先拆分为两步，增加一个P2（验证程序C），P2也满足拓扑排序关系，P2和P1的node列表是一个排序，P3和P2的node顺序相同，但每个node的等式列表相互是一个排列。从而将P1到P3的语义执行等价证明分解成P1到P2，再由P2到P3的等价性证明。由于P1到P2的只是node顺序不同，证明相对容易，难点在P2到P3的证明。 

503、利用验证程序A和验证程序C中node名一一对应的方式，可得到两者执行后语义等价的结果； 

根据语法树的性质，在P1中存在的node，在P2中也存在并且是同一个，因此可以证明两者是等价的。 

504、以验证程序C为基础，以仅有一步为区别的方式细化出中间验证程序C1、C2、C3……Cn，其中验证程序Cn与验证程序B仅有一步区别，对比两个程序执行后其局部环境的值可得到两者语义执行是否等价的结果，再依次反推直至得到验证程序C和验证程序B之间语义执行是否等价的结论； 

如图13所示，P2到P3由于每个node中的等式顺序都不同，直接证明难度较大，这也是证明过程中最重要的部分，需要联系语法和语义进行证明。本发明定义一个程序P(i)，P(i)是P2的前i个node加上P3去掉前i个的部分。从而将P2到P3的等价性证明转换到P(i)到P(i+1)的等价性证明。而P(i)到P(i+1)之间只有第（i+1）个node不同，其他node都相同。也就是将P2一步步细化，细化相邻的两个程序之间只有一步程序不同，这样最终细化的程序Cn与P3之间也只有一步不同，再对两者进行证明，然后反推依次证明每一步不同，即可最终得到P2和P3相同的结论。如图3所示，其中的N表示node名，eq表示等式。 

针对P(i)到P(i+1)之间不同的第（i+1）个node包括两种情况：1、这个不同的node是主node；2、这个不同的node不是主node。为简化证明，通过简化将第2种情况也转化为不同 的node是主node的证明情况。这虽然只是简单的分类，但却将node调用关系树中任意一个node不同化简为根节点的node不同的情况，从而使证明过程进一步化简。经过上一步的简化，所要证明的两个执行等价的程序还有两点不同，一是执行的主节点不相等，即执行的两个主节点的等式列表互相是一个排序，且节点的其他信息相同；二是两个程序执行的全局环境也不同，即由于主节点不同，故在全局环境中主节点对应位置的节点不相同。 

在两点不同的情况下，很难直接证明等价，因此需要先将其中一个不同的条件简化为相同的条件，如图14所示，简化的过程举例如下：程序执行过程中，全局环境gea和ged中的Nmain不同，其等式列表eql1和eql2互相是一个排序，执行的主节点Nmain也不同；且全局环境gea所对应的节点列表所抽取的依赖关系列表是满足拓扑排序性质的。现在无法一步直接将程序执行的全局环境gea化简到ged，但可先证明主节点Nmain1在gea和geb下执行等价，再证明Nmain2在gec和ged下执行等价。从而将证明简化为Nmain1在geb和Nmain2在gec下执行等价。其中第二步的简化相对简单，因为从一个少的环境gec到一个多的环境ged的证明过程中，如果程序能在环境gec中找到一个节点，那必能在ged中找到相同的节点。第一步的转换相对复杂，因为从一个多的环境gea到一个少的环境geb的证明过程中，如果能在gea中找到一个节点，则不一定能在少的环境geb中找到，在证明的过程中需要加入节点列表所抽取的依赖关系是满足拓扑排序性质的条件，这样主节点Nmain1以及ge1中的节点必不会调用ge2中的节点。第一步的证明过程中需要将该条件加入到互归纳中的每一层，并能使在各个层中的条件能够循环转化。 

经转换后的geb和gec的主节点仍然不同，需要进一步对证明进行化简，将其全局环境简化为相同的，使得在执行过程中只有要执行的主节点不同。如图15所示，可先证明主节点Nmain1在全局环境geb和ge1下执行等价，再证明主节点Nmain2在全局环境ge1和gec下执行等价。和前一步简化相似，也是简化的第二步相对简单，第一步较为复杂需要带入全局环境geb所抽取的节点依赖关系列表满足拓扑排序的性质。 

经过前面两次的化简，程序P(i)和P(i+1)执行的全局环境相同，只有主node不同。因为主node中的等式列表是一个排列，其顺序不同，直接证明难度依然很大，由于两个程序都满足拓扑排序的性质，同时利用排列的归纳性质可以将证明转化为主node中任意一个不依赖其他等式列表eql的等式eq，在eql中的任意位置，整个程序执行等价。如图16所示，即证明不依赖其他等式的eq在N1中插入等式列表的不同位置程序执行等价。 

对于主node不同的程序P(i)和P(i+1)，因为主node中的等式是一个排列，其顺序不同，直接证明难度依然很大。由于两个程序都满足拓扑排序的关系，因此同时利用排列的归纳性 质可以将证明转化为主node中任意一个不依赖其他等式列表eql的等式eq，在eql中的任意位置，整个程序执行等价，即证明不依赖其他等式的eq在N1中插入等式列表的不同位置程序执行等价。 

经过上述一系列的分解，最终需要证明的是两个互相不依赖的等式eq1和eq2，交换顺序执行等价，这也是整个证明过程的核心，这个证明的难点在于call表达式的存在，使得局部环境的子环境存在多种情况；还有Pre时态运算的存在。eq1的左值为lhs1，表达式为expr1；eq2的左值为lhs2，表达式为expr2。也就是要证明以下两种方式执行等价：先执行expr1将值赋给lhs1并写入环境，再执行expr2将值赋给lhs2并写入环境；先执行expr2将值赋给lhs2并写入环境，再执行expr1将值赋给lhs1并写入环境。即lhs1是否被赋值不影响expr2运算的值；lhs2是否被赋值不影响expr1运算的值。可以通过分情况讨论的方式来证明，首先根据两个表达式中是否有call表达式可以分成三种情况： 

(1)expr1和expr2中都没有call表达式； 

由于两个等式的表达式中都没有call，那么两个等式的子环境都为空。这种情况，比较容易证明，因为两种顺序的执行环境完全相同，且执行过程中都不改变子环境。 

(2)expr1中有call表达式，expr2中没有，或expr1中没有call表达式，expr2中有。 

由于expr1中有call表达式，所以expr1执行后会改变子环境。因为第一个周期和以后的周期执行过程中环境是不同的：第一个周期环境都是空的，执行过程也就是初始化环境树的过程，后面的周期因为环境树已经构造出来，每次执行只是给树的每个节点的列表增加一个，所以需要再分两种情况：第一个周期的证明；后续周期的证明。 

对于expr2中有的情况和expr1中有类似，只是顺序与前一种相反。也是需要根据周期分成两种情况继续讨论。 

(3)expr1和expr2中都有call表达式； 

在两个表达式中都有call的情况，两种执行顺序会造成子环境分多种情况。在执行call表达式时，会搜索等式子环境列表，如果能找到对应的等式子环境，则在前面加一个节点，如果找不到，则会新构造一个对应的等式子环境。所以根据两个等式对应的等式子环境是否能找到，可以再分成四种情况。其中前三种情况类似，第四种情况是两个等式对应的等式子环境都能找到，需要对其再次分类讨论。根据等式子环境列表的中eq1和eq2对应的等式子环境的顺序不同，分两种情况证明。 

本发明考虑到上述所有的情况后，得到证明结果。 

505、结合（3）和（4）的结果，得到拓扑排序前的Lustre程序和拓扑排序后的Lustre 程序执行语义等价的结论。 

106、由此得到Lustre程序和其经过因果分析和拓扑排序后生成的C程序在执行语义上是等价的证明。 

以上所述仅是本发明的较佳实施例而已，并非对本发明作任何形式上的限制，虽然本发明已以较佳实施例公开如上，然而并非用以限定本发明，任何熟悉本专利的技术人员在不脱离本发明技术方案范围内，当可利用上述提示的技术内容作出些许更动或修饰为等同变化的等效实施例，但凡是未脱离本发明技术方案的内容，依据本发明的技术实质对以上实施例所作的任何简单修改、等同变化与修饰，均仍属于本发明方案的范围内。