本文是其中的一部分嵌入式软件系列:使用ADA合同强制编码
在我们之前的文章中（bug验证软件的安魂曲:测试与静态分析），我们介绍了一个样本ADA程序，用于执行排序阵列的二进制搜索，我们使用传统测试和代码仪静态分析工具来定位错误。这是我们提出的代码：
类型Integer_Array是数组(正范围<>)的整数;——正的是整数的子集在范围1 ..Integer'Last——一个Integer_Array类型的对象有一个正的下界和任何上界函数取值:Integer) return Natural is——Natural是整数值的子集，取值范围为0 ..整数'最后的左，右，分裂:正;如果A'Length = 0，则返回0;如果;左:= 'First;右:= 'Last;如果A(左)>值然后返回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;
现在让我们使用SPARK 2014技术来进行正式的验证。1SPARK 2014包括一个语言(Ada 2012的子集)和一个静态分析工具，可以用来证明各种程序属性。它的好处在某种程度上取决于你付出了多少努力。您可以尝试消除运行时错误(即，确保不会出现超出边界的索引这样的错误)。或者，您可以针对正式指定的需求进行完整的功能验证。然而，这通常需要添加契约。
在Ada 2012和SPARK 2014中，契约是布尔表达式，可以附加到子程序声明中，指定它们对调用者的要求(前置条件)和保证结果(后置条件)。在本例中，二进制搜索只适用于已排序的数组(这是前提条件)，如果数组中没有值，它将返回0，或者为找到的值返回一个索引。在Ada 2012(和SPARK 2014)中，你可以将此类合同表述如下:
函数Sorted (A: Integer_Array)返回Boolean is (A'Length < 2或else(对于A'First ..A'Last - 1 =>(对于X + 1中的所有Y。A'Last => A (X) <= A (Y))));函数搜索(A: Integer_Array;值:整数)返回自然与Pre =>排序(A)， Post =>(如果搜索'结果= 0然后(所有索引在A'范围=> A(索引)/=值)else A(搜索'结果)=值));
我们首先引入了一个布尔函数“Sorted”，如果它的参数是排序的，则返回True。请注意Ada 2012量化表达的使用。然后，通过将表达式sorted (A)放在前置条件中，将Search函数的应用限制在排序数组中。最后，在后置条件中表示函数结果的预期值:如果返回0，则Value不在数组中，如果返回其他数字，则这是数组的一个下标，在这个下标处的数组元素包含Value。
通过在代码警报上运行SPARK工具，我们可以得到一些问题的警报。它确定了三个可能的运行时错误，并指出它不能建立后置条件。让我们逐一看看这些问题。
第一个可能的运行时错误在这一行中：
拆分:=(左+右)/ 2;
显然，加法可能会溢出，也就是说，当我们有一个很大的数组，并且在靠近右边的地方搜索时。同样的错误也在其他二进制搜索的实现中被发现。2
实际上，在Ada中，即使使用小阵列，这个问题也会出现。这是因为ADA中的数组的第一个索引可以是靠近最大可代表整数的一些大的正数。因此，我们需要避免溢出，这意味着写入分裂点的计算有点不同：
分割:=左+(右-左)/ 2;
毫无疑问，我们不是通过测试发现这一点的;我们应该用非常大的数组来测试。CodePeer的默认设置试图最小化“假警报”，因此CodePeer没有报告潜在的溢出。在工具的另一组选项下，问题就会被检测到。
下一个可能的运行时错误如下:
如果A (Split) = Value then
这里的火花抱怨拆分可能不在阵列的范围内。但是，由于左右在阵列的范围内，拆分清楚地在范围内。
实际上，这是SPARK工具的错误警报。问题是，在这一点上，SPARK不能单独计算出这些变量的可能范围，特别是因为它们是在循环中修改的。实际上，需要向SPARK解释在循环中修改的变量发生了什么。你可以使用pragma Loop_Invariant来做到这一点。这里，有趣的属性是Left和Right总是在数组范围内:
while Left <= Right循环pragma Loop_Invariant(左在A'Range内);pragma Loop_Invariant(在A'Range的右边);.．.
这消除了关于Split的错误消息。同样，这不是一个真正的错误，而是用户没有提供足够的信息使SPARK意识到问题永远不会发生的情况。
Spark报告的最后一次运行时错误是此处添加的可能溢出：
elsif a（split）<值然后左：= split + 1;
为什么Split会变得这么大，添加一个就会使它溢出?这可能发生在A'Last接近最大整数值;例如，对于非常大的数组，或者，就像上面的溢出一样，对于Ada中下界较大的小数组。不管怎样，Left不应该保持在数组范围内吗?事实上，这个错误与我们通过测试发现的第一个错误非常相似。我们需要防止查找的值大于数组中最大(最右边)值的情况。
要解决此问题，我们在While循环之前添加以下测试：
如果a（右）<值然后返回0;万一;
这使得我们的代码没有运行时错误!但是它总是返回正确的结果吗?SPARK仍然抱怨后置条件。
再一次，通过告诉它维持哪个财产，我们需要帮助火花的情况。在这种情况下，它实际上非常简单：我们只需指示我们正在搜索的数组区域。换句话说，我们需要指示我们已经排除在外的阵列的区域。我们通过Pragma Loop_Invariant表示此属性：
pragma Loop_Invariant (A'Range => (if Index < Left or Index > Right then A (Index) /= Value));
SPARK现在可以证明整个代码是正确的，没有运行时错误，功能上是完全正确的(也就是说，如果前提条件得到满足，它的后置条件将为真)。
下面是最终的实现:
功能搜索（A：Integer_Array;值：Integer）返回自然左，右，分裂：正面;如果A'Length = 0，则返回0;如果;左:= 'First;右:= 'Last;如果A(左)>值然后返回0;如果;如果a（右）<值然后返回0;如果;while Left <= Right循环pragma Loop_Invariant(左在A'Range内); pragma Loop_Invariant (Right in A'Range); -- Value is not before left and not after right pragma Loop_Invariant (for all Index in A'Range => (if Index < Left or Index > Right then A (Index) /= Value)); Split := Left + (Right - Left) / 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非常容易运行;比编写测试简单得多。在其默认设置中，CodePeer发现了一个很可能发生的错误，即空数组的情况。当将CodePeer设置为潜在错误的最大检测时，它将发现示例中的所有运行时错误。
像CodePeer这样的静态分析工具的一个限制是，它主要用于查找可能的运行时错误。但是，它通常找不到功能错误，因为CodePeer不知道代码应该做什么。尽管如此，它将指出许多可能影响功能正确性的可疑情况。但在我的例子中并非如此。也就是说，静态分析非常容易应用，所以它应该始终是验证活动的一部分。您可以控制潜在错误的最大检测和最小的“假警报”报告之间的权衡。
最后，形式化验证(例如，使用SPARK)可以以与静态分析相似的方式进行全部代码中的运行时间错误，即使是多年可能未被发现的最不可能的错误，例如拆分计算中的数值溢出。此外，正式验证可以告诉您您的代码在所有情况下是否在功能上正确。这是正式验证（Spark）提供比静态分析（Codepeer）提供更多功率的地方，因为表达功能正确性通常需要复杂的断言（如对所有人对于静态分析工具来说太复杂而无法使用。
但是，正式核查需要更多的努力，因为您需要包括计划要求的正式规范（例如，通过合同）。根据您的应用，这项努力可能是矫枉过正（例如，仅在内部使用的实用程序）或相反，可能对用户的安全或安全性至关重要。
更多信息请参阅嵌入式软件系列:使用ADA合同强制编码
引用:
2.额外的，额外 - 阅读所有内容：几乎所有二进制搜索和合并都被打破了
