时间戳

首页 > 解决方案 > quickCheck 命题逻辑生成器

haskell - quickCheck 命题逻辑生成器

问题描述

所以我有这个 quickCheck 命题逻辑生成器：

instance Arbitrary Form where
   arbitrary = genForm

genForm = sized genForm'
genForm' 0 = fmap Prop (choose (1,15))
genForm' n | n > 15 = genForm' (n `div` 2)
genForm' n | n > 0 =
          oneof [fmap Prop (choose (1,15)),
                 fmap Neg subform,
                 fmap Cnj subforms,
                 fmap Dsj subforms,
                 liftM2 Impl subform subform,
                 liftM2 Equiv subform subform]
          where subform = genForm' (n `div` 2)
                subforms = resize (n `div` 2) (vector (n `div` 2))

数据类型定义如下：

type Name = Int

data Form = Prop Name
          | Neg  Form
          | Cnj [Form]
          | Dsj [Form]
          | Impl Form Form
          | Equiv Form Form
          deriving (Eq,Ord)

问题是这个生成器将以以下形式生成：（+[]什么都没有的析取）。我不希望我的运算符没有嵌套Prop成员，因为它会生成无效的命题公式。我想确保Prop最后没有成员没有选择。

我的想法是这个问题来自resize (div n 2). 什么时候n甚至这最终会命中0并且不会进一步生成，从而创建一个空成员。删除resize将无济于事，因为它不会生成结尾的“树”。所以它似乎是必要的，但应该以某种方式进行调整。

但是我在 Haskell 方面并不出色，而且我在调试/阅读文档时遇到了困难。

标签： haskellgeneratorquickcheck

解决方案

应用于vector非零参数：

subforms = resize (n `div` 2) (vector (1 + (n `div` 2)))

或使用listOf1 arbitrary代替vector

subforms = resize (n `div` 2) (listOf1 arbitrary)

来自后续评论：

甚至需要生成量至少>2

应用于vector长度 >= 2：

subforms = resize (n `div` 2) (vector (2 + (n `div` 2)))

或者在前面显式附加两个元素（listOf用于允许长度也不同）：

subforms = resize (n `div` 2) (listOf2 arbitrary)
  where
    listOf2 :: Gen a -> Gen [a]
    listOf2 gen = liftA2 (:) gen (liftA2 (:) gen (listOf gen))
    -- 1. (listOf gen) to generate a list
    -- 2. Call gen twice to generate two more elements
    -- 3. Append everything together with `(:)`

推荐阅读