clojure.test.check generate two ints, one less than the other

Question

I want to write a property like the following:

(prop/for-all [x (gen/nat)
               y (gen/nat)]
  (= (g x y) (f x y)))

However, the property only holds when x > y. What is the correct way to express that precondition for this property? (Better yet, how can I write this property such that y is generated as a natural number less than x?)

Answer 1

1. You could generate y and an intermediate number dy, then compute x as (+ y dy).

   Generating dy using clojure.test.check.generators/nat ensures that it will be nonnegative – no need to apply absolute value in user code. If x needs to be strictly greater than – and not equal to – y, use clojure.test.check.generators/pos-int to generate dy instead.

   I believe this will tend to treat cases where the two numbers are closer together as "simpler" for the purposes of generating minimal failing cases. It seems that that would be a useful property for many scenarios – you'll have to judge if it's ok for yours.

2. You could generate x and y independently and use rejection sampling – clojure.test.check.generators/such-that allows you to "filter" the values generated by a base generator with a predicate of your choice.

   This isn't a great approach when the case you're looking for is generated with a very low probability, but x will be greater than y in ~½ of all cases, so it should be fine here.

3. You could use clojure.test.check.generators/bind as suggested by Mike. I'd suggest using it in tandem with clojure.test.check.generators/choose to generate a positive x and then a y in the range [0…x-1], perhaps in the following way:

   (prop/for-all [[x y] (gen/bind gen/nat
                          (fn [v]
                            (gen/tuple
                              (gen/return (inc v))
                              (gen/choose 0 v))))]
     (> x y))