Safe Haskell	Safe-Inferred
Language	Haskell2010

Test.QuickCheck.DynamicLogic

Description

Monadic interface for writing Dynamic Logic properties.

This interface offers a much nicer experience than manipulating the expressions it is implemented on top of, especially as it improves readability. It's still possible to express properties as pure expressions using the Core module and it might make sense depending on the context and the kind of properties one wants to express.

Synopsis

data DL s a
action :: (Show a, Typeable a, Eq (Action s a)) => Action s a -> DL s ()
anyAction :: DL s ()
anyActions :: Int -> DL s ()
anyActions_ :: DL s ()
stopping :: DL s ()
weight :: Double -> DL s ()
getSize :: DL s Int
getModelStateDL :: DL s s
assert :: String -> Bool -> DL s ()
assertModel :: String -> (s -> Bool) -> DL s ()
monitorDL :: (Property -> Property) -> DL s ()
forAllQ :: Quantifiable q => q -> DL s (Quantifies q)
forAllDL :: (DynLogicModel s, Testable a) => DL s () -> (Actions s -> a) -> Property
forAllDL_ :: (DynLogicModel s, Testable a) => DL s () -> (Actions s -> a) -> Property
forAllMappedDL :: (DynLogicModel s, Testable a, Show rep) => (rep -> DynLogicTest s) -> (DynLogicTest s -> rep) -> (Actions s -> srep) -> DL s () -> (srep -> a) -> Property
forAllMappedDL_ :: (DynLogicModel s, Testable a, Show rep) => (rep -> DynLogicTest s) -> (DynLogicTest s -> rep) -> (Actions s -> srep) -> DL s () -> (srep -> a) -> Property
forAllUniqueDL :: (DynLogicModel s, Testable a) => Int -> s -> DL s () -> (Actions s -> a) -> Property
withDLTest :: (DynLogicModel s, Testable a) => DL s () -> (Actions s -> a) -> DynLogicTest s -> Property
data DynLogic s
class StateModel s => DynLogicModel s where
- restricted :: Action s a -> Bool
data DynLogicTest s
- = BadPrecondition [TestStep s] [Any (Action s)] s
- | Looping [TestStep s]
- | Stuck [TestStep s] s
- | DLScript [TestStep s]
data TestStep s
- = Do (Step s)
- | forall a.(Eq a, Show a, Typeable a) => Witness a
module Test.QuickCheck.DynamicLogic.Quantify

Documentation

data DL s a Source #

The DL monad provides a nicer interface to dynamic logic formulae than the plain API. It's a continuation monad producing a DynFormula formula, with a state component threaded through.

Instances

Instances details

MonadFail (DL s) Source #
Instance details Defined in Test.QuickCheck.DynamicLogic Methods fail :: String -> DL s a #
Alternative (DL s) Source #
Instance details Defined in Test.QuickCheck.DynamicLogic Methods empty :: DL s a # (<\|>) :: DL s a -> DL s a -> DL s a # some :: DL s a -> DL s [a] # many :: DL s a -> DL s [a] #
Applicative (DL s) Source #
Instance details Defined in Test.QuickCheck.DynamicLogic Methods pure :: a -> DL s a # (<>) :: DL s (a -> b) -> DL s a -> DL s b # liftA2 :: (a -> b -> c) -> DL s a -> DL s b -> DL s c # (>) :: DL s a -> DL s b -> DL s b # (<*) :: DL s a -> DL s b -> DL s a #
Functor (DL s) Source #
Instance details Defined in Test.QuickCheck.DynamicLogic Methods fmap :: (a -> b) -> DL s a -> DL s b # (<$) :: a -> DL s b -> DL s a #
Monad (DL s) Source #
Instance details Defined in Test.QuickCheck.DynamicLogic Methods (>>=) :: DL s a -> (a -> DL s b) -> DL s b # (>>) :: DL s a -> DL s b -> DL s b # return :: a -> DL s a #

action :: (Show a, Typeable a, Eq (Action s a)) => Action s a -> DL s () Source #

anyAction :: DL s () Source #

anyActions :: Int -> DL s () Source #

anyActions_ :: DL s () Source #

stopping :: DL s () Source #

weight :: Double -> DL s () Source #

getSize :: DL s Int Source #

getModelStateDL :: DL s s Source #

assert :: String -> Bool -> DL s () Source #

Fail if the boolean is False.

Equivalent to

assert msg b = unless b (fail msg)

assertModel :: String -> (s -> Bool) -> DL s () Source #

monitorDL :: (Property -> Property) -> DL s () Source #

forAllQ :: Quantifiable q => q -> DL s (Quantifies q) Source #

Generate a random value using the given Quantification (or list/tuple of quantifications). Generated values will only shrink to smaller values that could also have been generated.

forAllDL :: (DynLogicModel s, Testable a) => DL s () -> (Actions s -> a) -> Property Source #

forAllDL_ :: (DynLogicModel s, Testable a) => DL s () -> (Actions s -> a) -> Property Source #

forAllMappedDL :: (DynLogicModel s, Testable a, Show rep) => (rep -> DynLogicTest s) -> (DynLogicTest s -> rep) -> (Actions s -> srep) -> DL s () -> (srep -> a) -> Property Source #

forAllMappedDL_ :: (DynLogicModel s, Testable a, Show rep) => (rep -> DynLogicTest s) -> (DynLogicTest s -> rep) -> (Actions s -> srep) -> DL s () -> (srep -> a) -> Property Source #

forAllUniqueDL :: (DynLogicModel s, Testable a) => Int -> s -> DL s () -> (Actions s -> a) -> Property Source #

withDLTest :: (DynLogicModel s, Testable a) => DL s () -> (Actions s -> a) -> DynLogicTest s -> Property Source #

data DynLogic s Source #

Base Dynamic logic formulae language. Formulae are parameterised over the type of state s to which they apply. A DynLogic value cannot be constructed directly, one has to use the various "smart constructors" provided, see the Building formulae section.

class StateModel s => DynLogicModel s where Source #

Restricted calls are not generated by AfterAny; they are included in tests explicitly using After in order to check specific properties at controlled times, so they are likely to fail if invoked at other times.

Minimal complete definition

Nothing

Methods

restricted :: Action s a -> Bool Source #

data DynLogicTest s Source #

Constructors

BadPrecondition [TestStep s] [Any (Action s)] s
Looping [TestStep s]
Stuck [TestStep s] s
DLScript [TestStep s]

Instances

Instances details

StateModel s => Show (DynLogicTest s) Source #
Instance details Defined in Test.QuickCheck.DynamicLogic.Core Methods showsPrec :: Int -> DynLogicTest s -> ShowS # show :: DynLogicTest s -> String # showList :: [DynLogicTest s] -> ShowS #

data TestStep s Source #

Constructors

Do (Step s)
forall a.(Eq a, Show a, Typeable a) => Witness a

Instances

Instances details

StateModel s => Show (TestStep s) Source #
Instance details Defined in Test.QuickCheck.DynamicLogic.Core Methods showsPrec :: Int -> TestStep s -> ShowS # show :: TestStep s -> String # showList :: [TestStep s] -> ShowS #
Eq (TestStep s) Source #
Instance details Defined in Test.QuickCheck.DynamicLogic.Core Methods (==) :: TestStep s -> TestStep s -> Bool # (/=) :: TestStep s -> TestStep s -> Bool #

module Test.QuickCheck.DynamicLogic.Quantify