How to validate commutativity involving the dif/2 constraint?
There is a lot of hype around the dif/2 constraint, especially as a rescue for some non-declarativity of (=)/2 and (==)/2. This non-declarativity is often characterized as non-monotonicity and examples of non-communtativity are given.
But what would be the means to test whether test cases involving dif/2 are commutative. Here is a meta explanation what I want to do:
I make a commutativity test, and I want to probe that both variants give the same result:
?- A, B.
-- versus --
?- B, A.
So usually you can check monotonicity, if it boils down to checking commutativity, with the (==)/2 built-in predicate. Since this predicate follows instantiated variables.
But if you are testing cases that produce constraints, call_with_residue/2 is not enough, you need also to have equality of constraints. Which can be tricky, as the following example shows:
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)).
Any ideas how to proceed?
Disclaimer, its a trap:
I don't endorse commutativity testing as a good testing method, where you can separate good and bad predicates versus a specification. Since usually both the good and bad predicates might have no problems with commutativity.
I am using commutativity testing as a vehicle to find out about methods for equality of dif/2 constraints. This equality can then be used in more traditional test cases as a validation point.
There are several ways. Maybe the easiest in this case is to simply re-post the collected residual constraints.
In this example, we get:
?- 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(U, T), f(g(Z), Z)).
The goal is now much simpler!
You can collect residual goals with copy_term/3 and call_residue_vars/2 .
上一篇: 内存数据库。 单元测试或集成测试？
下一篇: 如何验证涉及dif / 2约束的交换性？