5.2.2　不可达路径判定问题的重定义

一条程序路径p由一系列节点n 1,n 2,…,n k以及节点之间的边组成,每一个节点对应程序中的一条语句,节点之间的边表示语句间的控制流关系,k是路径的长度。

定义5-4(可达路径) 路径p是可达的,当且仅当在程序的输入域D中存在至少一个输入v,利用v执行程序的执行轨迹与p一致。路径p的可达性等价于路径约束条件C p的可满足性[7]。约束是可满足的记为Cp⊨D v。

定义5-5(矛盾约束) 路径条件Cp是一系列逻辑谓词的合取φ1∧φ2∧…∧φk,其中φi是节点n i对应的条件表达式。若路径p是不可达路径,则在取值域D中所有值都无法满足C p,此时Cp是矛盾约束,记为Cp⊨DØ,在后续的讨论中会将符号D省略以节省篇幅。(https://www.daowen.com)

定义5-6(矛盾位置) 若路径p是不可达路径,其约束为Cp=φ1∧φ2∧…∧φk,则在Cp中存在约束φi∧…∧φj不可满足,其中i＜…＜j∈[1,k],记为(φi∧…∧φj)。称不可达路径p的矛盾位置是从1到j。

若k-j＜i-1,意味着从终点出发反向分析路径可达性能够比正向分析更早地判定矛盾约束。下一节通过对不可达路径的调研总结不可达路径上矛盾约束的位置特征。