5

给定一棵任意树，我可以在该树上构建一个子类型关系，使用舒伯特编号：

constructH :: Tree a -> Tree (Type a)

whereType嵌套原始标签，并额外提供执行子/父（或子类型）检查所需的数据。使用舒伯特编号，两个 Int 参数就足够了。

data Type a where !Int -> !Int -> a -> Type a

这导致二元谓词

subtypeOf :: Type a -> Type a -> Bool

我现在想用 QuickCheck 测试这确实做了我想做的事情。但是，以下属性不起作用，因为 QuickCheck 只是放弃了：

subtypeSanity ∷ Tree (Type ()) → Gen Prop
subtypeSanity Node { rootLabel = t, subForest = f } =
  let subtypes = concatMap flatten f
  in (not $ null subtypes) ==> conjoin
     (forAll (elements subtypes) (\x → x `subtypeOf` t):(map subtypeSanity f))

如果我省略对 的递归调用subtypeSanity，即我传递给的列表的尾部，则conjoin该属性运行良好，但只测试树的根节点！如何在 QuickCheck 不放弃生成新测试用例的情况下递归地进入我的数据结构？

如果需要，我可以提供构建 Schubert Hierarchy 的代码和 的Arbitrary实例Tree (Type a)，以提供完整的可运行示例，但这将是相当多的代码。我确信我只是没有“获得”QuickCheck，并且在这里以错误的方式使用它。

编辑：不幸的是，该sized功能似乎并没有消除这里的问题。它最终得到相同的结果（请参阅对 J. Abrahamson 的回答的评论。）

编辑二：我最终通过避免递归步骤来“解决”我的问题，并避免conjoin. 我们只需列出树中所有节点的列表，然后在这些节点上测试单节点属性（从一开始就很好）。

allNodes ∷ Tree a → [Tree a]
allNodes n@(Node { subForest = f }) = n:(concatMap allNodes f)

subtypeSanity ∷ Tree (Type ()) → Gen Prop
subtypeSanity tree = forAll (elements $ allNodes tree)
  (\(Node { rootLabel = t, subForest = f }) →
    let subtypes = concatMap flatten f
    in (not $ null subtypes) ==> forAll (elements subtypes) (\x → x `subtypeOf` t))

调整树的Arbitrary实例不起作用。这是我仍在使用的任意实例：

instance (Arbitrary a, Eq a) ⇒ Arbitrary (Tree (Type a)) where
  arbitrary = liftM (constructH) $ sized arbTree

arbTree ∷ Arbitrary a ⇒ Int → Gen (Tree a)
arbTree n = do
  m ← choose (0,n)
  if m == 0
    then Node <$> arbitrary <*> (return [])
    else do part ← randomPartition n m
            Node <$> arbitrary <*> mapM arbTree part

-- this is a crude way to find a sufficiently random x1,..,xm,
-- such that x1 + .. + xm = n, for any n, m, with 0 < m.
randomPartition ∷ Int → Int → Gen [Int]
randomPartition n m' = do
  let m = m' - 1
  seed ← liftM ((++[n]) . sort) $ replicateM m (choose (0,n))
  return $ zipWith (-) seed (0:seed)

我认为这个问题“现在已经解决了”，但是如果有人可以向我解释为什么递归步骤和/或conjoin让 QuickCheck 放弃（在通过“仅”0 个测试之后），我将不胜感激。

4

2 回答 2

7

在生成Arbitrary递归结构时，QuickCheck 通常有点过于急切，会生成庞大的随机示例。这些是不可取的，因为它们通常不能更好地检查感兴趣的属性并且可能非常慢。两种解决方案是

  1. 使用大小参数（sized函数）和frequency函数之类的东西将生成器偏向小树。

  2. 使用像smallcheck. 这些试图详尽地生成所有“小”示例，从而有助于保持树的大小。

为了阐明控制世代大小的方法sized和frequency方法，这里有一个例子RoseTree

data Rose a = It a | Rose [Rose a]

instance Arbitrary a => Arbitrary (Rose a) where
  arbitrary = frequency 
    [ (3, It <$> arbitrary)                   -- The 3-to-1 ratio is chosen, ah,
                                              -- arbitrarily...
                                              -- you'll want to tune it
    , (1, Rose <$> children)
    ]
    where children = sized $ \n -> vectorOf n arbitrary

Rose通过非常小心地控制子列表的大小，可以更简单地使用不同的格式来完成

data Rose a = Rose a [Rose a]

instance Arbitrary a => Arbitrary (Rose a) where
  arbitrary = Rose <$> arbitrary <*> sized (\n -> vectorOf (tuneUp n) arbitrary)
    where tuneUp n = round $ fromIntegral n / 4.0

您可以在不引用 的情况下执行此操作sized，但这会为您的Arbitrary实例的用户提供一个旋钮，以便在需要时请求更大的树。

于 2013-12-03T14:16:28.923 回答
3

如果它对那些偶然发现这个问题的人有用：当 QuickCheck “放弃”时，这表明您的先决条件（使用==>）太难以满足。

QuickCheck 使用简单的拒绝抽样技术：前置条件对值的生成没有影响。QuickCheck 会像正常一样生成一堆随机值。在这些生成之后，它们通过前置条件发送：如果结果是True，则使用该值测试属性；如果是False，则丢弃该值。如果您的先决条件拒绝了 QuickCheck 生成的大部分值，那么 QuickCheck 将“放弃”（最好完全放弃，而不是提出统计上可疑的通过/失败声明）。

特别是，QuickCheck不会尝试生成满足给定前提条件的值。确保您使用的生成器（arbitrary或其他方式）产生大量通过您的前提条件的值取决于您。

让我们看看这在您的示例中是如何体现的：

subtypeSanity :: Tree (Type ()) -> Gen Prop
subtypeSanity Node { rootLabel = t, subForest = f } =
  let subtypes = concatMap flatten f
  in (not $ null subtypes) ==> conjoin
     (forAll (elements subtypes) (`subtypeOf` t):(map subtypeSanity f))

只出现一次==>，所以它的前提条件 ( not $ null subtypes) 一定很难满足。这是由于递归调用map subtypeSanity f：您不仅拒绝任何Tree具有空的subForest内容，而且（由于递归）拒绝任何包含s 和空s 的地方，Tree并拒绝任何包含s 和s 包含s 的地方带有空的 s，依此类推。subForestTreesubForestTreesubForestTreesubForestTreesubForest

根据您的arbitrary实例，Trees 仅嵌套到有限深度：最终我们将始终达到空subForest，因此您的递归前提条件将始终失败，并且 QuickCheck 将放弃。

于 2015-09-08T08:36:47.910 回答