clojure.test.check 生成两个整数，一个小于另一个

Question

我想写一个如下的属性:

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

但是，该属性仅在 x > y 时成立。表达此属性的前提条件的正确方法是什么？ (更好的是，我如何编写这个属性，使 y 生成为小于 x 的自然数？)

Answer 1

1. 你可以生成y和一个中间数dy，然后计算x为(+ y dy)。

   使用 clojure.test.check.generators/nat 生成 dy 确保它是非负的——无需在用户代码中应用绝对值。如果 x 需要严格大于 - 并且不等于 - y，请使用 clojure.test.check.generators/pos-int 来改为生成 dy。

   我相信这将倾向于将两个数字更接近的情况视为“更简单”，以便生成最少的失败案例。似乎这对于许多场景来说都是一个有用的属性——您必须判断它是否适合您的场景。

2. 您可以独立生成 x 和 y 并使用拒绝采样 - clojure.test.check.generators/such-that允许您使用您选择的谓词“过滤”由基本生成器生成的值。

   当您要查找的案例以非常低的概率生成时，这不是一个好方法，但 x 将大于 y ~½在所有情况下，所以这里应该没问题。

3. 您可以按照 Mike 的建议使用 clojure.test.check.generators/bind。我建议将它与 clojure.test.check.generators/choose 一起使用以生成正 x 然后在范围 [0…x-1]，可能是以下方式:

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