关于dif/2约束有很多炒作，特别是作为对(=)/2和(==)/2的一些非声明性的拯救。这种非声明性通常被描述为非单调性，并给出了非社群性的例子。
但是，测试涉及dif/2的测试用例是否可交换的方法是什么呢?下面是我想要做的meta解释:
我做一个交换性检验，我想探测这两个变异体给出相同的结果:
?- 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约束相等的方法。这个等式可以在更传统的测试用例中用作验证点。
有几种方法。也许在这种情况下最简单的方法是简单地重新发布收集到的剩余约束。
在这个例子中，我们得到: <>之前- X = a(g(Z)， U)，dif (f (g (Z), U), U, Z, U, T), f ((U g (T)), g (Z), T, g (Z), Z))。X = a(g(Z)， U)，dif(f(U, T)， f(g(Z)， Z))之前目标现在简单多了!
您可以收集copy_term/3和call_residue_vars/2的剩余目标。