测试一个过于笼统的程序

假设谓词的正确定义是

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是直接递归的，我们将有无限多的过于笼统的情况。显然，在这种情况下，定位错误会更容易。