测试一个过于笼统的程序

Question

假设谓词的正确定义是

len([],0).
len([_|T],N)  :-  len(T,X), N is  X+1.

然而，我们最终得到了以下错误的定义。

len2([],0).
len2([_|T],N)  :-  len(T,X),  ( N  is  X+1 ; N is X + 2, N = 10000 ).

所有标准测试都没有发现错误，因为它的工作原理与 len/2 一样，除非它偶然发现长度正好为 9999 的元素列表，其中有两个可能的答案。

正如用户mjano314 所 观察到的。怎么可能检测到这样的错误？

---

请注意，len2/2上面使用len/2. 以这种方式，恰好有一个定义过于笼统的情况。将len2/2是直接递归的，我们将有无限多的过于笼统的情况。显然，在这种情况下，定位错误会更容易。

Answer 1

如果我们已经怀疑谓词len2(X,Y)不起作用，而我们期望它起作用，这意味着在这种情况下，不存在第一个参数具有相同值而第二个参数具有不同值的两个答案，那么我们可以通过以下方式验证我们的怀疑使用以下代码片段搜索这两个答案：

len2(X,Y1), len2(X,Y2), Y1\=Y2

在这种情况下，程序将为我们提供答案Y1=9999,Y2=10000以及X9999 个变量的列表。

但是，如果错误不存在，或者谓词的代码使得触发错误的输入不是在有限时间内生成的（想象一下它在任何奇数长度列表之前生成所有偶数长度列表），则代码上面不会完成。在我看来，这意味着这种方法仅作为调试工具有用，但并不真正适合作为谓词的某些自动化测试/验证的一部分。