Requiem for a Bug – Verifying Software: Testing and Static Analysis

2014年11月4日

This article offers two approaches toward addressing the problem of software verification at increasing levels of sophistication.

Johannes Kanig

Related To: AdaCore

This article is part of the嵌入Software系列：Enforced Coding Using Ada Contracts

Download this article in .PDF format

您如何使您的代码按预期行事？您选择的方法在发现问题时是否有效？在本文中，我将在ADA中编写一个代码，然后尝试以两种不同的方法来编写一段代码：

• Testing by writing a simple unit test

• Static analysis using the CodePeer tool

这些方法以提高的复杂水平解决软件验证的问题。尽管所选的示例很小，但它将显示各种验证技术是无法实现的。

The sample program that will illustrate the different methods is a binary search for a particular value in a sorted array; the search function returns the index of the value (if present) and zero otherwise. The same value may occur more than once in the array; in such a situation, the search function is to return the index of one match.

二进制搜索是一种众所周知的算法，可以在排序的数组中找到给定值。二进制搜索不会从一开始搜索整个数组，而是将数组中间的数组值与给定值进行比较。如果前者更大，则搜索将继续在该中间价值的左边。否则，它将继续向右。通过这种方式，二进制搜索将在每次迭代时将搜索空间分成一半，直到它找到值或得出结论，它不能在数组中。标准线性搜索具有O(n) execution time, while a binary search isO（日志₂（n））

二进制搜索是一种非常基本的算法，但是编程时犯错误非常容易。唐纳德·努斯（Donald Knuth）等伟大的思想指出了这一点¹and Jon Bentley²。If you’re interested in further information, I invite you to read a recent “Stack Overflow” discussion³, but only after reading my articles.

Here’s my first try at implementing the binary search algorithm:

Integer_Array类型是数组(正面范围< >)Integer; -- Positive is the subset of Integer values in the range 1 .. Integer'Last -- An object of type Integer_Array has a Positive lower bound and any upper bound function Search (A : Integer_Array; Value : Integer) return Natural is -- Natural is the subset of Integer values in the range 0 .. Integer'Last Left : Positive := A'First; -- Index of lower bound Right : Positive := A’Last; -- Index of upper bound Split : Positive; begin while Left <= Right loop 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;

This implementation assumes that the array indices are positive numbers (but not necessarily starting at 1). However, the result of the function is a Natural value, which includes zero. This allows the function to return the special value zero, which cannot be a valid index in the array, to indicate that the value was not found.

该算法保持两个指数 - 左且正确。这些表示算法当前正在搜索的区域。该范围以外的任何东西都被排除在外。在每个步骤中，该算法都计算左右之间的中间点，将该索引的值与给定值进行比较，然后返回结果或排除从区域中搜索的区域或右侧区域。一旦要搜索的区域变为空（循环的退出条件），该算法就可以返回零，表明该值不存在。

看起来很合理，对吗？我们将首先尝试测试，以查看是否有任何问题。我通过以下方式测试了此功能，这对我来说看起来很详尽：

我创建了一个在1到100之间的10个随机整数的数组，并按顺序排序。然后，我将上面的搜索函数与此数组一起用作第一个参数，所有整数在1到100之间作为第二个参数。对于每个值，我检查结果是否为预期的一个：0，如果该值不在数组中；否则，它将返回索引，使得a（i）= value。

实际上，我的功能在第一个测试中崩溃，搜索值1！这是为什么？我忘了考虑到价值已经小于数组的第一个元素的情况。在这种情况下，该算法将将变量“右”设置为越来越小的值，直到它试图将其设置为零。最终将通过运行时检查失败，因为权利被限制为正，这不包括零。

解决方案是通过在WHIL循环之前添加以下检查来保护这种情况：

if A (Left) > Value then return 0; end if;

My seemingly exhaustive test found no more problems.

Shown is a screenshot of a CodePeer session with CodePeer messages and computed preconditions.

Then I ran the static analysis tool CodePeer, which examines Ada code for potential run-time errors and logic bugs. CodePeer reports problematic constructs in source code, and computes preconditions for functions, i.e., conditions that need to be met by the caller. A screenshot of the CodePeer report for our example appears in the figure. In this case, it is very interesting to look at the computed precondition for our Search function:

-- A(A'First)'Initialized -- A'Last >= 1 -- A'First <= A'Last

似乎要求阵列应该是非空的。实际上，在传递空数组时，我的代码将失败（例如，下限为1，上限为0）。我胸怀简单的测试策略并未涵盖这种情况，因为它仅以固定的尺寸为10。校正非常容易；我们只需在功能开头添加适当的测试即可。同样，由于权利可能不是积极的（即，当数组为空时），因此需要更改其声明，或者需要移动其初始化。我们选择了后者，为了保持一致性，我们还移动了左的初始化。

这是该程序的修改版本，包括对我们发现的两个错误的更正：

function Search (A : Integer_Array; Value : Integer) return Natural is -- Natural is the subset of Integer values in the range 0 .. Integer'Last Left, Right, Split : Positive; begin if A'Length = 0 then return 0; end if; Left := A'First; Right := A'Last; if A (Left) > Value then return 0; end if; while Left <= Right loop 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;

With its default settings, CodePeer did not identify any additional bugs in this code. Is the program now correct? We’ll answer this issue in Part 2 of this series, when we use SPARK 2014 and formal methods to augment our verification approach.

从嵌入Software系列：Enforced Coding Using Ada Contracts

Download this article in .PDF format