haskell - QuickCheck 中是否有 "there exists"量词？

Question

有forAll量词返回一个检查所有测试用例是否通过的属性。有没有办法定义一个“存在”量词，它返回一个属性来检查它至少一个测试用例是否通过？

Answer 1

通过枚举测试存在会更可靠:SmallCheck , LeanCheck , FEAT .
如果必须使用随机生成，QuickCheck 中有一些间接方法。

expectFailure 似乎是一个很好的否定候选人。然而它并不完全如此，因为它不是内合的，所以你必须以其他方式否定该属性，如 not ，如果您的属性实际上是 bool 值。

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

手动执行此操作还具有 if prop 的属性。意外崩溃，它立即报告为失败，与以前的方法相反。

编辑
因此，如果您只有 (a -> Property)而不是 (a -> Bool)获得一个好的结果似乎要复杂得多，因为检查一个属性是否成功并非易事。正确的方法是弄乱 QuickCheck 的内部结构，可能类似于 disjoin .这是一个快速破解

使用mapResult使 disjoin 的输出静音当没有找到(反)示例时。

覆盖大小参数，因为如果您的见证不平凡，那么如果大小太小或太大，将无法找到它们。

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)