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).

   生成dy使用clojure.test.check.generators/nat可确保它是非负的 - 无需在用户代码中应用绝对值.如果x需要严格大于 - 而不等于 - y,请使用clojure.test.check.generators/pos-int生成dy代替.

   我认为,为了产生最小的失败案例,这将倾向于将两个数字更接近的情况视为"更简单".对于许多情况来说,这似乎是一个有用的属性 - 您必须判断它是否适合您的情况.

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

   当你正在寻找的情况以非常低的概率生成时,这不是一个很好的方法,但是x会大于y所有情况的~1/2,所以这里应该没问题.

3. 您可以clojure.test.check.generators/bind按照Mike的建议使用.我建议使用它clojure.test.check.generators/choose来生成一个正数x,然后y在[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))