7

围绕 dif/2 约束有很多炒作，尤其是作为 (\=)/2 和 (\==)/2 的一些非声明性的补救措施。这种非声明性通常以非单调性为特征，并给出了非交流性的例子。

但是测试涉及 dif/2 的测试用例是否可交换的方法是什么。这是我想要做的元解释：

我做了一个交换性测试，我想探测两个变体给出相同的结果：

?- A, B.
-- versus --
?- B, A.

因此，通常您可以使用 (==)/2 内置谓词检查单调性，如果归结为检查交换性。由于此谓词遵循实例化变量。

但是如果你在测试产生约束的用例， call_with_residue/2 是不够的，你还需要约束相等。这可能很棘手，如以下示例所示：

Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.3.23)
Copyright (c) 1990-2015 University of Amsterdam, VU Amsterdam

?- dif(f(X,X),f(a(U,g(T)),a(g(Z),U))), X=a(g(Z),U).
X = a(g(Z), U),
dif(f(a(g(Z), U), U, Z, U, T), f(a(U, g(T)), g(Z), T, g(Z), Z)).

?- X=a(g(Z),U), dif(f(X,X),f(a(U,g(T)),a(g(Z),U))).
X = a(g(Z), U),
dif(f(U, T), f(g(Z), Z)).

任何想法如何进行？

免责声明，这是一个陷阱：
我不认可交换性测试是一种好的测试方法，您可以在其中将好的和坏的谓词与规范分开。因为通常好谓词和坏谓词都可能没有交换性问题。

我正在使用交换性测试作为一种工具来了解 Dif/2 约束相等的方法。然后可以在更传统的测试用例中将这种相等用作验证点。

4

1 回答 1

3

有几种方法。在这种情况下，最简单的方法可能是简单地重新发布收集到的剩余约束。

在这个例子中，我们得到：

?- X = a(g(Z), U),
   差异（f（a（g（Z），U），U，Z，U，T），f（a（U，g（T）），g（Z），T，g（Z），Z）） .
X = a(g(Z), U),
差异（f（U，T），f（g（Z），Z））。

现在的目标要简单得多！

copy_term/3您可以使用和 收集剩余目标call_residue_vars/2。

于 2016-06-27T23:11:52.290 回答