问题描述
假设谓词的正确定义是
len([],0).
len([_|T],N) :- len(T,X),N is X+1.
然而，我们最终得到了以下错误的定义。
len2([],0).
len2([_|T],( N is X+1 ; N is X + 2,N = 10000 ).
所有标准测试都没有发现错误，因为它的工作方式与 len/2 一样，除非它偶然发现长度正好为 9999 元素的列表，其中有两个可能的答案。
作为用户 mjano314 observes。怎么可能检测到这样的错误？
请注意，上面的 len2/2 使用了 len/2。以这种方式，恰好有一个定义过于笼统的情况。 len2/2 是否是直接递归的，我们将有无数过于笼统的情况。显然，在这种情况下，定位错误会更容易。
解决方法
如果我们已经怀疑谓词 len2(X,Y) 在我们期望的时候不起作用，这意味着在这种情况下，没有两个答案的第一个参数具有相同的值，而第二个参数的值不同，然后我们可以通过使用以下代码段搜索这两个答案来验证我们的怀疑：
len2(X,Y1),len2(X,Y2),Y1\=Y2
在这种情况下，程序会给我们一个包含 Y1=9999、Y2=10000 和 X 一个包含 9999 个变量的列表的答案。
但是，如果错误不存在或者谓词的代码使得触发错误的输入不是在有限时间内生成的（想象一下它在任何奇数长度列表之前生成所有偶数长度列表），那么上面的代码将无法完成。这意味着，在我看来，这种方法仅可用作调试工具，但并不真正适合作为谓词的某些自动化测试/验证的一部分。
,正如@jnmonette 所指出的，从第一个参数到第二个参数存在函数依赖。像这样的查询
?- len2(L,N),dif(N,M),len2(L,M).
L = [_A,_B,_C,_D,_E,_F,_G,_H,_I,_J|...],N = 9999,M = 10000
; L = [_A,N = 10000,M = 9999
; *LOOPS*
可以检测到 len2/2 中的错误。毕竟，L 不能有两个不同的长度。此外，
?- len2([_|L],N).
N = 10000,L = [_A,_J|...]
; *LOOPS*
标识错误进入另一个方向。 L 和 [_|L] 的长度不能相同。这可以概括为涵盖所有此类错误：
?- len2(L,phrase(([_],...),L,K),len2(K,N).
L = [_A,K = [_B,_J,_K|...]
; *LOOPS*
到目前为止，我们直接使用了 Prolog。我们能够通过提出这个查询来说明一般属性。然而，只有在有一些反例时，我们才会找到反例，否则我们就会陷入不确定中。而且，我们很幸运，实际定义以公平的方式列举了答案，让每个答案都在有限的时间内出现。如果定义要求更高（考虑交换 len/2 中子句的顺序），只需在所有查询前添加 length(L,_)。
但是，在运行查询的情况下，我们不可避免地会问：我们应该继续等待答案，还是可以中止查询？毕竟，对于正确的实现，查询不会产生任何答案，因此会无限循环。
没有办法（在当前的实现中）至少将这样的查询委托给以较低优先级运行的后台。因此，此类查询根本不用于测试。
另一方面，这样的查询是表达许多可测试属性的一种非常强大的方式。例如，SICStus、SWI 和 Scryer 的 clpfd 系统中的许多错误已使用 condor 以这种方式识别。然而，粗略的支持并没有带来非常优雅的解决方案。
要开始解决这个问题，以下注释可能会有所帮助：
:/-& len2(L,M).
:/-& len2(L,N).
:/- 表示没有解 - 类似于 :- \+ Q_0. 和附加的 &，一个 asciified ∞，意味着 Prolog 的执行将是无限的。因此，此注释为尝试证明没有解决方案的更好策略留下了空间。
在 GUPU 中，此注释作为具有（相对较短）超时的 Prolog 目标执行。还尝试了替代策略，特别是迭代深化，在这种情况下也会超时。如此有效地，错误仍未被检测到。但是如果有更多的资源或更好的策略，错误可能会被发现。