5期 高鹰等：基于抽象解释的代码迷惑有效性比较框架 811 SQ],可以保证结论成立. 代码迷惑有效性定理。 传递定理也可以表述为抽象α是保偏序的. 4.1定义实例语言 推论.HP,Q∈P,SaIP]ESu IQ]→S,IP] 首先在流图语言[]（如图2）的基础上定义离散 E+S,IQ1. 转移系统T=〈∑，：，〉定义如下： 传递定律及其推论的含义在于：抽象解释将程 ∑表示状态集合，Σ三3×C,其中3是环境集 序分析看成是语义的近似，分析算法即是建立对语 合，环境是变量到值的映射，C是命令集合.状态s= 义的抽象：而且程序分析算法之间可以建立相互之 (p,C)中，p表示下一条命令C的执行环境. 间的抽象.所以可以根据传递定理，只要对于某一种 ,二Σ表示程序的初始状态 抽象的程序分析算法满足偏序，那么这样的偏序关 程序 P:PP△(C) 系是可以传递到其它由该抽象构造的其它程序分析 命令 C:CC::=LI:A-L2 算法上的， 程序动作A:AA:=V:=EV:=?引hpB 算术表达式E:EE:=nlxlEiop.E: 因此，如果在收集语义上可以比较迷惑有效性， 布尔表达式B:BB:=true|falsel Biops B2|-E:|Biop.Bz 能得到更强的结论，因为此时还不涉及到分析语义 变量 V:V标签L:L整数n:Z 的实例化，迷惑算法在收集语义上的有效性，对于所 图2流图语言的语法（其中op.是二元算术算子，0p是 有分析算法来说都是有效的. 二元逻辑算子，0p.是二元逻辑比较算子) 所以，迷惑的有效性比较是能够基于不可计算 图3是对流图语言语义的定义，转移关系S∈ 的语义上的. C→（∑和(）)可以定义为 命题2（迷惑的有效性）.VP∈P,如果关系 S((p,C))=(p,C')lp'ES lact [C]]pA Sa[P]Ecol Sco ITob[P]成立，则称变换t针对任意 suc [C]=labIC']). 分析算法都是有效的. 定义程序P∈P的转移语义S∈P→（Σ→和(）) 命题1和命题2为比较迷惑前后的程序的语义 为：SPs={(p,C)∈S(p,C)|s=〈p,C)p, 提供了理论基础.命题2要求的是对通常是不可计 p'∈3∧C∈P. 算的收集语义上的比较，通常无法直接计算得到二 二∑XΣ，表示状态s∈Σ与其可能后继s'∈ 者间的关系，但是可以得到比较强的结论，是通过语 的二元传递关系，(s,s)∈t当且仅当s'∈S(s),简记 义信息的变化来定义有效性的，与具体的分析算法 为s￥s',‘是转移关系S的另一种表达.如果命令 无关；而命题1是建立在分析语义基础上的，是基于 A,K∈C,且有suc[A]=lab[K],K是A的后继，为 分析得到的语义信息来定义有效性，可以直接计算 统一标记，也记为A￥K. 得到二者间的关系，不过有效性只是适用于这个具 体的分析算法. 程序动作：S[A]e:A→(3→3) SIskip le=p SIV :=El=[VA[El] 4 实例化有效性比较框架 s[V=l,=p[V一n],其中n∈z S[B]==p,其中B[Ble=true 布尔表达式：B[Elp:B→(3→3) 本节主要内容是根据上节提出的代码迷惑有效 B[ELOP6 E2le=A[E:leOpA [E:le 性比较框架，针对一个具体的迷惑算法，使用例子说 B[B1oP.B:le=B[B:lop.B [B:le 明有效性比较框架证明迷惑算法有效性的过程.为 算术表达式：A[E]:B→(3→3) A[rle=p(r) 证明迷惑算法的有效性，首先需要证明所比较的变 AIn le=p(n) 换算法是属于迷惑空间的，然后需要证明算法的有 A[E1op.E:le=A[E leop.A [E2le 效性满足有效性命题.为此，需要实例化的部分有实 图3流图语言的语义 例语言和迷惑算法，通过定义实例语言，就能够得到 标准语义.由抽象解释框架理论，实例化框架所需要 几个使用到的基本语义函数： 的其它语义，包括可观察语义、收集语义、分析语义， lab[L1:A→Lzl=L1 act IL1:A→Lz=A 都能通过对标准语义的定义抽象得到.在实例化这 sc[L1:A→L2l=L:war IL1:A→L2l=wr【A] 些部分后，就可以严格证明保证代码迷惑正确性的 迹是指状态转移序列，迹语义使用有限或是无 可观察语义等价性定理以及说明代码迷惑有效性的 限的状态序列来模型化计算过程，反映了程序最精#!犙"，可以保证结论成立． 传递定理也可以表述为抽象α是保偏序的． 推论． 犘，犙∈#，#犮狅犾!犘"!#犮狅犾!犙"#φ!犘" !φ#φ!犙"． 传递定律及其推论的含义在于：抽象解释将程 序分析看成是语义的近似，分析算法即是建立对语 义的抽象；而且程序分析算法之间可以建立相互之 间的抽象．所以可以根据传递定理，只要对于某一种 抽象的程序分析算法满足偏序，那么这样的偏序关 系是可以传递到其它由该抽象构造的其它程序分析 算法上的． 因此，如果在收集语义上可以比较迷惑有效性， 能得到更强的结论，因为此时还不涉及到分析语义 的实例化，迷惑算法在收集语义上的有效性，对于所 有分析算法来说都是有效的． 所以，迷惑的有效性比较是能够基于不可计算 的语义上的． 命题２（迷惑的有效性）． 犘∈#，如果关系 #犮狅犾!犘"!犮狅犾#犮狅犾! τ狅犫!犘""成立，则称变换τ狅犫针对任意 分析算法都是有效的． 命题１和命题２为比较迷惑前后的程序的语义 提供了理论基础．命题２要求的是对通常是不可计 算的收集语义上的比较，通常无法直接计算得到二 者间的关系，但是可以得到比较强的结论，是通过语 义信息的变化来定义有效性的，与具体的分析算法 无关；而命题１是建立在分析语义基础上的，是基于 分析得到的语义信息来定义有效性，可以直接计算 得到二者间的关系，不过有效性只是适用于这个具 体的分析算法． ４ 实例化有效性比较框架 本节主要内容是根据上节提出的代码迷惑有效 性比较框架，针对一个具体的迷惑算法，使用例子说 明有效性比较框架证明迷惑算法有效性的过程．为 证明迷惑算法的有效性，首先需要证明所比较的变 换算法是属于迷惑空间的，然后需要证明算法的有 效性满足有效性命题．为此，需要实例化的部分有实 例语言和迷惑算法．通过定义实例语言，就能够得到 标准语义．由抽象解释框架理论，实例化框架所需要 的其它语义，包括可观察语义、收集语义、分析语义， 都能通过对标准语义的定义抽象得到．在实例化这 些部分后，就可以严格证明保证代码迷惑正确性的 可观察语义等价性定理以及说明代码迷惑有效性的 代码迷惑有效性定理． ４１ 定义实例语言 首先在流图语言［８］（如图２）的基础上定义离散 转移系统 %＝〈Σ，Σ犻，ι〉定义如下： Σ 表示状态集合，Σ "× &，其中 "是 环 境 集 合，环境是变量到值的映射，&是命令集合．状态狊＝ 〈ρ，犆〉中，ρ表示下一条命令犆 的执行环境． Σ犻Σ 表示程序的初始状态． 程序 犘：# 犘!（犆） 命令 犆：& 犆∷＝犔１：犃→犔２； 程序动作 犃：' 犃∷＝犞··＝ 犈｜犞··＝？｜狊犽犻狆｜犅 算术表达式 犈：( 犈∷＝狀｜狓｜犈１狅狆犪犈２ 布尔表达式 犅：) 犅∷＝ｔｒｕｅ｜ｆａｌｓｅ｜犅１狅狆犫犅２｜!犈２｜犅１狅狆犮犅２ 变量 犞：* 标签犔：" 整数狀：+ 图 ２ 流图语言的语法（其中狅狆犪是二元算术算子，狅狆犫是 二元逻辑算子，狅狆犮是二元逻辑比较算子） 图３是对流图语言语义的定义，转移关系犛∈ & →（Σ→ !（Σ））可以定义为 犛（〈ρ，犆〉）＝｛〈ρ′，犆′〉｜ρ′∈犛! 犪犮狋!犆"" ρ∧ 狊狌犮!犆"＝犾犪犫!犆′"｝． 定义程序犘∈#的转移语义犛∈#→（Σ→!（Σ）） 为：犛!犘狊" ＝｛〈ρ′，犆′〉∈犛（〈ρ，犆〉）｜狊＝〈ρ，犆〉∧ρ， ρ′∈"∧犆′∈犘｝． ιΣ×Σ，表示状态狊∈Σ 与其可能后继狊′∈Σ 的二元传递关系，〈狊，狊′〉∈ι当且仅当狊′∈犛（狊），简记 为狊↓狊′，ι是转移关系犛 的另一种表达．如果命令 Λ，Κ∈&，且有狊狌犮! Λ"＝犾犪犫! Κ"，Κ 是Λ 的后继，为 统一标记，也记为Λ↓Κ． 程序动作：犛!犃" ρ：'→ （" → "） 犛! 狊犽犻狆" ρ＝ρ 犛!犞··＝犈" ρ＝ρ［犞 #犃!犈" ρ］ 犛!犞··＝？" ρ＝ρ［犞 #狀］，其中狀∈+ 犛!犅" ρ＝ρ，其中犅!犅" ρ＝ｔｒｕｅ 布尔表达式：犅!犈" ρ：( → （" → "） 犅!犈１狅狆犫犈２" ρ＝犃!犈１" ρ狅狆犫犃!犈２" ρ 犅!犅１狅狆犮犅２" ρ＝犅!犅１" ρ狅狆犮犅!犅２" ρ 算术表达式：犃!犈" ρ：( → （" → "） 犃!狓" ρ＝ρ（狓） 犃! 狀" ρ＝ρ（狀） 犃!犈１狅狆犪犈２" ρ＝犃!犈１" ρ狅狆犪犃!犈２" ρ 图 ３ 流图语言的语义 几个使用到的基本语义函数： 犾犪犫!犔１：犃→犔２；"＝犔１ 犪犮狋!犔１：犃→犔２；"＝犃 狊狌犮!犔１：犃→犔２；"＝犔２ 狏犪狉!犔１：犃→犔２；"＝狏犪狉!犃" 迹是指状态转移序列，迹语义使用有限或是无 限的状态序列来模型化计算过程，反映了程序最精 ５ 期 高 鹰等：基于抽象解释的代码迷惑有效性比较框架 ８１１