State machine based testing in Haskell QuickCheck

Question

Does Haskell QuickCheck have the state machine based features that John Hughes' describes in the following talk and paper -

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

If not, how does one actually do stateful testing using Haskell's QuickCheck? For example, what is the best way to test a circular buffer using Haskell QuickCheck without reimplementing the core logic in the test itself.

Answer 1

I don't think there's any explicit support in QuickCheck, but I think the general approach in Haskell would be something like the following example.

It tests a test system (custom List instance) against a model (a real Haskell list). The key is to generate arbitrary sequences of stateful primitive operations (e.g., Push, Pop, and IsEmpty) and apply them to both the test system and the model in a monadic fashion, checking post conditions after each operation. In this case, the post conditions are just to test that operations that return values (pop and isEmpty) return the same values for the test system and model, but it could easily be modified to test other post conditions (or add pre-conditions).

If a test fails, it will return a minimal sequence of operations applied to the empty list that causes the post conditions to fail.

{-# 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