Bug验证软件的安魂曲:测试和静态分析

2014年11月4日,

本文提供了两种方法来解决日益复杂的软件验证问题。

约翰内斯Kanig

相关: AdaCore

这篇文章是嵌入式软件系列:使用Ada契约强制编码

下载本文的。pdf格式

怎样做才能使代码按照预期的方式运行?你选择的方法在发现问题时是否像你想象的那样有效?本文是由两部分组成的系列文章的第一篇，我将用Ada编写一段代码，然后用两种不同的方法来寻找bug:

•通过编写简单的单元测试进行测试

•使用CodePeer工具进行静态分析

这些方法在日益复杂的水平上处理软件验证的问题。尽管所选择的示例很小，但它将展示各种验证技术可以实现什么，不能实现什么。

演示这两种方法的示例程序是在一个已排序的数组中对特定值进行二进制搜索;搜索函数返回值的索引(如果存在)，否则返回0。相同的值可以在数组中出现多次;在这种情况下，搜索函数将返回一个匹配项的索引。

二分搜索是一种在排序数组中定位给定值的著名算法。二进制搜索不是一开始就搜索整个数组，而是将数组中间的数组值与给定值进行比较。如果前者更大，搜索将继续到中间值的左边;否则，它将继续向右。以这种方式，二分搜索将在每次迭代时将搜索空间分成两半，直到它找到值或得出它不可能在数组中。一个标准的线性搜索O(n)执行时间，而二分搜索为O(日志₂(n))

二分搜索是一种非常基本的算法，但令人惊讶的是，它在编程时很容易出错。唐纳德·克努特(Donald Knuth)等伟大的思想家已经指出了这一点¹和乔恩•宾利²．如果您对进一步的信息感兴趣，我邀请您阅读最近的“堆栈溢出”讨论^3.，但得先看完我的文章。

这是我第一次尝试实现二分搜索算法:

类型Integer_Array是数组(正范围<>)的整数;——正的是整数的子集在范围1 ..Integer'Last——一个Integer_Array类型的对象有一个正的下界和任何上界函数取值:Integer) return Natural is——Natural是整数值的子集，取值范围为0 ..整数'最后左边:正面:= A'第一;右:正:= A 'Last;——上界分裂指数:正;Split:= (Left + Right) / 2;如果A (Split) = Value则返回Split;elsif A (Split) < Value then Left:= Split + 1; else Right := Split - 1; end if; end loop; return 0; end Search;

这个实现假设数组的下标是正数(但不一定从1开始)。然而，函数的结果是一个Natural值，其中包括0。这允许函数返回特殊值0(它在数组中不是有效的索引)，以表明没有找到该值。

该算法维护两个索引——左索引和右索引。这些表示算法当前正在搜索的区域。超出这个范围的都被排除了。在每一步中，该算法计算左和右之间的中间点，将该索引处的值与给定值进行比较，然后返回结果或从要搜索的区域中排除左或右区域。一旦要搜索的区域变为空(循环的退出条件)，算法就可以返回零，表明该值不存在。

这看起来很合理，对吧?我们将先进行测试，看看是否有问题。我用下面的方法测试了这个函数，看起来非常详尽:

我创建了一个10个随机整数的数组，从1到100，按升序排序。然后，我使用上面的Search函数，这个数组作为第一个参数，所有1到100之间的整数作为第二个参数。对于每一个值，我都检查结果是否为预期值:如果值不在数组中，则为0;否则，它返回一个索引，使A (I) = Value．

事实上，我的函数在第一次测试时崩溃了，搜索值为1!这是为什么呢?我忘了考虑Value已经小于数组的第一个元素的情况。在本例中，算法将把变量“Right”的值设置得越来越小，直到它尝试将其设置为零。这最终会在运行时检查中失败，因为Right被限制为正，这排除了零。

解决方案是通过在while循环之前添加以下检查来防止这种情况:

如果A(左)>值然后返回0;如果;

我看似详尽的测试没有发现更多的问题。

显示的是带有CodePeer消息和计算的先决条件的CodePeer会话的截图。

然后，我运行了静态分析工具CodePeer，它检查Ada代码中潜在的运行时错误和逻辑错误。CodePeer报告源代码中有问题的构造，并计算函数的先决条件，即调用者需要满足的条件。图中显示了我们示例的CodePeer报告的屏幕截图。在这种情况下，看看搜索函数的计算先决条件是非常有趣的:

——A(A' first)')被初始化——A' last ' >= 1——A' first <= A' last

它似乎要求数组应该是非空的。实际上，当传递给它一个空数组时，我的代码将会失败(例如，当下界为1，上界为0时)。我头脑简单的测试策略没有涵盖这种情况，因为它只测试一个大小为10的固定数组。修正很容易;我们只需在函数的开头添加一个适当的测试。此外，由于Right可能不是正的(即，当数组为空时)，要么它的声明需要更改，要么它的初始化需要移动。我们选择了后者，为了一致性，我们还移动了Left的初始化。

以下是该程序的修改版本，包括对我们发现的两个错误的修正:

函数搜索(A: Integer_Array;取值:Integer) return Natural is——Natural是整数值的子集，取值范围为0 ..整数'最后的左，右，分裂:正;如果A'Length = 0，则返回0;如果;左:= 'First;右:= 'Last;如果A(左)>值然后返回0;如果;Split:= (Left + Right) / 2; if A (Split) = Value then return Split; elsif A (Split) < Value then Left := Split + 1; else Right := Split - 1; end if; end loop; return 0; end Search;

使用其默认设置，CodePeer不会在此代码中识别任何其他错误。程序现在是否正确?我们将在本系列的第2部分中回答这个问题，届时我们将使用SPARK 2014和形式化方法来扩充我们的验证方法。

更多信息请参阅嵌入式软件系列:使用Ada契约强制编码

下载本文的。pdf格式