haskell - Haskell QuickCheck 中基于状态机的测试

Question

Haskell QuickCheck 是否具有 John Hughes 在以下演讲和论文中描述的基于状态机的功能 -

• http://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf
• https://www.youtube.com/watch?v=zi0rHwfiX1Q

如果没有，如何使用 Haskell 的 QuickCheck 进行状态测试？例如，使用 Haskell QuickCheck 测试循环缓冲区的最佳方法是什么，而无需重新实现测试本身的核心逻辑。

Answer 1

我认为 QuickCheck 中没有任何明确的支持，但我认为 Haskell 中的一般方法类似于以下示例。

它根据模型(真实的 Haskell 列表)测试测试系统(自定义 List 实例)。关键是生成有状态原语操作的任意序列(例如，Push、Pop 和 IsEmpty)并将它们应用到测试系统以及以单子(monad)方式的模型，在每次操作后检查后置条件。在这种情况下，后置条件只是为了测试返回值的操作(pop 和 isEmpty)是否为测试系统和模型返回相同的值，但它可以很容易地进行修改以测试其他后置条件(或添加前置条件)。

如果测试失败，它将返回应用于空列表的最小操作序列，从而导致后置条件失败。

{-# LANGUAGE GADTs, StandaloneDeriving #-}

module ListTest where

import Test.QuickCheck
import Data.Monoid
import Control.Monad

-- |The system to test

data List a = Empty | Cons a (List a) deriving (Show, Eq)
push x lst = Cons x lst
pop (Cons x lst) = (Just x, lst)
pop Empty = (Nothing, Empty)
isEmpty Empty = True
isEmpty _     = False

-- |The model (based on plain Haskell lists)

type Model a = [a]
pushM = (:)
popM []     = (Nothing, [])
popM (x:xs) = (Just x, xs)
isEmptyM [] = True
isEmptyM _  = False

-- |Operations on lists of `a`s
data Op a = Push a | Pop | IsEmpty deriving (Show, Eq)
instance Arbitrary a => Arbitrary (Op a) where
  arbitrary = oneof ([Push <$> arbitrary, pure Pop, pure IsEmpty])

-- |For each op, return tuple of: (return values matched?, (new List, new Model))
compare_op :: (Eq a) => Op a -> (List a, Model a) -> (All, (List a, Model a))
compare_op (Push x) (lst, mdl) = -- True b/c no return value to compare
                                 (All True, (push x lst, pushM x mdl))
compare_op Pop      (lst, mdl) = let (y1, lst') = pop lst
                                     (y2, mdl') = popM mdl
                                 in  (All (y1 == y2), (lst', mdl'))
compare_op IsEmpty  (lst, mdl) = (All (isEmpty lst == isEmptyM mdl), (lst, mdl))

-- |The property that a sequence of operations has matching return values.
prop_model :: [Op Int] -> Bool
prop_model ops = (getAll . fst . foldM (flip compare_op) (Empty, [])) ops

main :: IO ()
main = quickCheck prop_model