测试过于笼统的程序
Testing a too general program
假设谓词的正确定义是
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 ).
All the standard testing doesn’t reveal the mistake because it works just like len/2 except when it stumbles upon a list of length exactly 9999 elements where there are two possible answers.
作为用户 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 个变量的列表的答案。
但是，如果错误不存在，或者谓词的代码使得触发错误的输入在有限时间内没有生成（假设它在任何奇数长度列表之前生成所有偶数长度列表), 那么上面的代码将不会完成。这意味着，在我看来，这种方法仅作为调试工具有用，但并不真正适合作为谓词的某些自动化 testing/validation 的一部分。
正如@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,_B,_C,_D,_E,_F,_G,_H,_I,_J|...], N = 10000, M = 9999
; *LOOPS*
可以检测到len2/2中的错误。毕竟，L 不能有两个不同的长度。此外，
?- len2([_|L], N), len2(L, N).
N = 10000, L = [_A,_B,_C,_D,_E,_F,_G,_H,_I,_J|...]
; *LOOPS*
标识错误进入另一个方向。 L 和 [_|L] 的长度不能相同。这可以概括为涵盖所有此类错误：
?- len2(L, N), phrase(([_],...), L,K), len2(K, N).
L = [_A,_B,_C,_D,_E,_F,_G,_H,_I,_J|...], N = 10000, K = [_B,_C,_D,_E,_F,_G,_H,_I,_J,_K|...]
; *LOOPS*
至此我们直接使用了Prolog。我们能够通过提出这个查询来陈述一般属性。但是，如果有反例，我们只会找到反例，否则我们就不确定了。而且，我们非常幸运，实际定义以公平的方式列举了答案，让每个答案都在有限的时间内出现。如果定义要求更高（考虑交换 len/2 中子句的顺序），只需在目前所有查询前添加 length(L, _)。
然而，在 运行 查询的情况下，我们不可避免地会问：我们应该继续等待答案，还是已经中止查询？毕竟，对于正确的实现，查询不会产生任何答案，因此会无限循环。
没有办法（在当前的实现中）将这样的查询至少委派到后台 运行 那里具有较低的优先级。因此，此类查询根本不用于测试。
另一方面，此类查询是表达许多可测试属性的一种非常强大的方式。例如，SICStus、SWI 和 Scryer 的 clpfd 系统中的许多错误已使用 condor 以这种方式识别。然而，更粗糙的支持并没有带来非常优雅的解决方案。
要开始解决这个问题，以下注释可能会有所帮助：
:/-& len2(L, N), dif(N, M), len2(L, M).
:/-& len2(L, N), phrase(([_],...), L,K), len2(K, N).
:/- 意味着无解 - 类似于 :- \+ Q_0. 和附加的 &，一个 asciified ∞，意味着 Prolog 的执行将是无限的。因此，此注释留有空间来尝试更好的策略，以证明没有解决方案。
在 GUPU 中，此注释作为 Prolog 目标执行，具有（相对较短的）超时。还尝试了替代策略，特别是迭代深化，在这种情况下也会超时。如此有效，错误仍然未被发现。但是如果有更多的资源或更好的策略，错误可能会被发现。
假设谓词的正确定义是
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 ).
All the standard testing doesn’t reveal the mistake because it works just like len/2 except when it stumbles upon a list of length exactly 9999 elements where there are two possible answers.
作为用户 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 个变量的列表的答案。
但是，如果错误不存在，或者谓词的代码使得触发错误的输入在有限时间内没有生成（假设它在任何奇数长度列表之前生成所有偶数长度列表), 那么上面的代码将不会完成。这意味着，在我看来，这种方法仅作为调试工具有用，但并不真正适合作为谓词的某些自动化 testing/validation 的一部分。
正如@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,_B,_C,_D,_E,_F,_G,_H,_I,_J|...], N = 10000, M = 9999
; *LOOPS*
可以检测到len2/2中的错误。毕竟，L 不能有两个不同的长度。此外，
?- len2([_|L], N), len2(L, N).
N = 10000, L = [_A,_B,_C,_D,_E,_F,_G,_H,_I,_J|...]
; *LOOPS*
标识错误进入另一个方向。 L 和 [_|L] 的长度不能相同。这可以概括为涵盖所有此类错误：
?- len2(L, N), phrase(([_],...), L,K), len2(K, N).
L = [_A,_B,_C,_D,_E,_F,_G,_H,_I,_J|...], N = 10000, K = [_B,_C,_D,_E,_F,_G,_H,_I,_J,_K|...]
; *LOOPS*
至此我们直接使用了Prolog。我们能够通过提出这个查询来陈述一般属性。但是，如果有反例，我们只会找到反例，否则我们就不确定了。而且，我们非常幸运，实际定义以公平的方式列举了答案，让每个答案都在有限的时间内出现。如果定义要求更高（考虑交换 len/2 中子句的顺序），只需在目前所有查询前添加 length(L, _)。
然而，在 运行 查询的情况下，我们不可避免地会问：我们应该继续等待答案，还是已经中止查询？毕竟，对于正确的实现，查询不会产生任何答案，因此会无限循环。
没有办法（在当前的实现中）将这样的查询至少委派到后台 运行 那里具有较低的优先级。因此，此类查询根本不用于测试。
另一方面，此类查询是表达许多可测试属性的一种非常强大的方式。例如，SICStus、SWI 和 Scryer 的 clpfd 系统中的许多错误已使用 condor 以这种方式识别。然而，更粗糙的支持并没有带来非常优雅的解决方案。
要开始解决这个问题，以下注释可能会有所帮助：
:/-& len2(L, N), dif(N, M), len2(L, M).
:/-& len2(L, N), phrase(([_],...), L,K), len2(K, N).
:/- 意味着无解 - 类似于 :- \+ Q_0. 和附加的 &，一个 asciified ∞，意味着 Prolog 的执行将是无限的。因此，此注释留有空间来尝试更好的策略，以证明没有解决方案。
在 GUPU 中，此注释作为 Prolog 目标执行，具有（相对较短的）超时。还尝试了替代策略，特别是迭代深化，在这种情况下也会超时。如此有效，错误仍然未被发现。但是如果有更多的资源或更好的策略，错误可能会被发现。