5.2.5 对于代码片段性值的有效性验证
本节利用统计数据来对上一节所猜想的性质进行验证。首先统计了在一个广泛使用的开源工程Coreutils-8.24中LDc2的出现情况。Coreutils工程为GNU系列的操作系统提供了核心功能,其代码行数超过6万,具体信息和统计数据如表5-2所示,可以看到在Coreutils中此代码片段出现的频率为每千行代码4.4个。
表5-2 依赖循环的等值模式在Coreutils的出现情况
本节使用二项分布检验(binomial testing)来验证猜想的性质。首先将性质拆分成为两个假设。
①R 1:程序中若包含LDc2,则等式判定条件n的约束可能导致路径条件发生矛盾。
②R 2:由LDc2导致的矛盾约束位置相比于程序入口,更接近n。
为了验证此假设,本书对Coreutils中满足LDc2的程序中的不可达路径数量进行了统计,由于对于不可达路径的统计是保守的近似分析,所以将R 1成立的概率设置为0.7,R 2是在R 1成立的基础之上做出的假设,因此将假设R 2成立的概率设置为0.93。(https://www.daowen.com)
显著性水平设置为a=0.05,拒绝域的临界值是满足式(5-4)的最小整数。
其中,u 1-a是正态分布的中位数,经过计算,c的值分别是169和163。样本的统计数据如表5-3所示,具有R 1和R 2特性的样本数量x的值分别是170和163。在5%的显著水平下,假设R 1和R 1成立。
表5-3 假设检验的统计数据
