3

我想写一个如下的属性：

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

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

4

2 回答 2

5

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

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

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

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

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

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

    (prop/for-all [[x y] (gen/bind gen/nat
                       (fn [v]
                         (gen/tuple
                           (gen/return (inc v))
                           (gen/choose 0 v))))]
  (> x y))
于 2015-11-18T23:33:51.120 回答
3

您可以使用 bind 函数创建一个依赖于先前值的生成器。我确信必须有一种更清洁的方法来做到这一点。

(def always-greater-than
  (gen/bind gen/nat
           (fn [v] (gen/tuple (gen/return (inc v))
                              (gen/fmap #(mod % (inc v)) gen/nat)))))

示例输出：

(gen/sample always-greater-than)
([1 0] [2 0] [1 0] [3 0] [1 0] [6 4] [7 6] [2 0] [3 2] [6 4])
于 2015-11-19T00:06:54.407 回答