QuickCheck中是否存在"存在"量词？

Question

有一个forAll量词,它返回一个属性,检查所有测试用例是否通过.有没有办法定义一个"存在"量词,它返回一个属性,检查它至少有一个测试用例通过？

Answer 1

通过枚举测试存在会更可靠:SmallCheck,LeanCheck,FEAT.

如果必须使用随机生成,则QuickCheck中有一些间接方法.

expectFailure似乎是一个很好的否定候选人.然而它并不完全,因为它不是非对称的,所以你必须以其他方式否定属性,例如not,如果你的属性实际上是布尔值.

exists :: Gen a -> (a -> Bool) -> Property
exists gen prop = once $ expectFailure (forAll gen (not . prop))

这会将崩溃视为失败,因此即使您可能没有预期,也会使测试通过.

存在量化是一种分离,QuickCheck有disjoin.只要做出足够大的分离.

exists :: Gen a -> (a -> Property) -> Property
exists gen prop = once $ disjoin $ replicate 10000 $ forAll gen prop

但是,当没有找到好的例子时,你会被反复发送垃圾邮件.也许最好重写forAll自己的逻辑以避免调用counterexample.

更简单地说,您总是可以将自己的属性编写为生成器以获得正确的量化.

exists :: Gen a -> (a -> Bool) -> Property
exists gen prop = property (exists' 1000 gen prop)

exists' :: Int -> Gen a -> (a -> Bool) -> Gen Bool
exists' 0 _ _ = return False
exists' n gen prop = do
  a <- gen
  if prop a
    then return True
    else exists' (n - 1) gen prop

手动执行此操作还具有以下属性:如果prop意外崩溃,则会立即将其报告为失败,与之前的方法相反.

编辑

因此,如果你只有一个(a -> Property)而不是(a -> Bool)看起来更难以实现一个好的结果,因为检查一个属性是否成功是非常重要的.一个正确的方法是混淆QuickCheck的内部,可能是类似的东西disjoin.这是一个快速黑客

• 用于在未找到(计数器)示例时mapResult使输出静音disjoin.

• 覆盖size参数,因为如果您的证人不重要,如果尺寸太小或太大,则无法找到它们.

import Test.QuickCheck
import Test.QuickCheck.Property as P

-- Retry n times.
exists :: Testable prop => Int -> Gen a -> (a -> prop) -> Property
exists n gen prop =
  mapResult (\r -> r {P.reason = "No witness found.", P.callbacks = []}) $
  once $
  disjoin $
  replicate n $ do
    a <- gen
    return (prop a)

main = quickCheck $ exists 100
  (resize 5 arbitrary)
  (\x -> (x :: Integer) == 2)