测试 "Safe term order"谓词

Question

在最近的一个问题 ( How to define (and name) the corresponding safe term comparison predicates in ISO Prolog? ) 中，@false 要求实现术语排序谓词 lt/2 , ISO 内置的变体 (@<)/2 .

lt(T1,T2)的真值是稳定的 w.r.t. T1 中的任意变量绑定(bind)和 T2 .

在各种答案中，提出了不同的实现(基于隐式/显式术语遍历)。评论中提出了一些注意事项和提示，也提出了反例。

那么我的问题是:如何测试候选实现？一些蛮力方法？或者更聪明的东西？

无论如何，请分享您的自动测试机器lt/2 !这是为了更大的利益!

Answer 1

有两种测试策略:验证和验证。

验证:测试总是一样的。首先，您需要对要测试的内容进行规范。其次，您需要实现要测试的内容。

然后从实现中提取代码执行路径。对于规范中的每个代码执行路径，您都可以获得所需的结果。

然后您编写结合每个执行路径和期望结果的测试用例。不仅要测试正路径，还要测试负路径。

如果你的代码是递归的，理论上你有无限多的执行路径。

但是您可能会发现子递归或多或少地询问与另一个测试用例已经询问的相同的问题。因此，在许多情况下，您还可以使用有限集进行测试。

验证给你信心。

验证:您将使用一些正式的方法从规范中得出您的实现的正确性。

验证给您 100% 的保证。