Safe Haskell	Safe-Inferred
Language	Haskell2010

Test.QuickCheck.DynamicLogic.Internal

Contents

Building formulae
Generate Properties

Synopsis

newtype DynFormula s = DynFormula {
- unDynFormula :: Int -> DynLogic s
}
data DynLogic s
- = EmptySpec
- | Stop
- | AfterAny (DynPred s)
- | Alt ChoiceType (DynLogic s) (DynLogic s)
- | Stopping (DynLogic s)
- | forall a.(Eq (Action s a), Show (Action s a), Typeable a) => After (ActionWithPolarity s a) (Var a -> DynPred s)
- | Error String (DynPred s)
- | Weight Double (DynLogic s)
- | forall a.QuantifyConstraints a => ForAll (Quantification a) (a -> DynLogic s)
- | Monitor (Property -> Property) (DynLogic s)
data ChoiceType
- = Angelic
- | Demonic
type DynPred s = Annotated s -> DynLogic s
ignore :: DynFormula s
passTest :: DynFormula s
afterAny :: (Annotated s -> DynFormula s) -> DynFormula s
afterPolar :: (Typeable a, Eq (Action s a), Show (Action s a)) => ActionWithPolarity s a -> (Var a -> Annotated s -> DynFormula s) -> DynFormula s
after :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> (Var a -> Annotated s -> DynFormula s) -> DynFormula s
afterNegative :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> (Annotated s -> DynFormula s) -> DynFormula s
(|||) :: DynFormula s -> DynFormula s -> DynFormula s
forAllQ :: Quantifiable q => q -> (Quantifies q -> DynFormula s) -> DynFormula s
weight :: Double -> DynFormula s -> DynFormula s
withSize :: (Int -> DynFormula s) -> DynFormula s
toStop :: DynFormula s -> DynFormula s
done :: Annotated s -> DynFormula s
errorDL :: String -> DynFormula s
monitorDL :: (Property -> Property) -> DynFormula s -> DynFormula s
always :: (Annotated s -> DynFormula s) -> Annotated s -> DynFormula s
data FailingAction s
- = ErrorFail String
- | forall a.(Typeable a, Eq (Action s a)) => ActionFail (ActionWithPolarity s a)
data DynLogicTest s
- = BadPrecondition (TestSequence s) (FailingAction s) (Annotated s)
- | Looping (TestSequence s)
- | Stuck (TestSequence s) (Annotated s)
- | DLScript (TestSequence s)
data Witnesses r where
- Do :: r -> Witnesses r
- Witness :: QuantifyConstraints a => a -> Witnesses r -> Witnesses r
discardWitnesses :: Witnesses r -> r
pattern Witnesses :: Witnesses () -> r -> Witnesses r
type TestStep s = Witnesses (Step s)
newtype TestSequence s = TestSeq (Witnesses (TestContinuation s))
data TestContinuation s
- = ContStep (Step s) (TestSequence s)
- | ContStop
pattern TestSeqStop :: TestSequence s
pattern TestSeqStep :: Step s -> TestSequence s -> TestSequence s
pattern TestSeqWitness :: () => forall a. QuantifyConstraints a => a -> TestSequence s -> TestSequence s
consSeq :: TestStep s -> TestSequence s -> TestSequence s
unconsSeq :: TestSequence s -> Maybe (TestStep s, TestSequence s)
unstopSeq :: TestSequence s -> Maybe (Witnesses ())
pattern TestSeqStopW :: Witnesses () -> TestSequence s
pattern (:>) :: TestStep s -> TestSequence s -> TestSequence s
nullSeq :: TestSequence s -> Bool
dropSeq :: Int -> TestSequence s -> TestSequence s
getContinuation :: TestSequence s -> TestSequence s
unlines' :: [String] -> String
prettyTestSequence :: VarContext -> TestSequence s -> String
prettyWitnesses :: Witnesses () -> [String]
usedVariables :: forall s. StateModel s => TestSequence s -> VarContext
class StateModel s => DynLogicModel s where
- restricted :: Action s a -> Bool
restrictedPolar :: DynLogicModel s => ActionWithPolarity s a -> Bool
forAllScripts :: (DynLogicModel s, Testable a) => DynFormula s -> (Actions s -> a) -> Property
forAllUniqueScripts :: (DynLogicModel s, Testable a) => Annotated s -> DynFormula s -> (Actions s -> a) -> Property
forAllMappedScripts :: (DynLogicModel s, Testable a) => (rep -> DynLogicTest s) -> (DynLogicTest s -> rep) -> DynFormula s -> (Actions s -> a) -> Property
withDLScript :: (DynLogicModel s, Testable a) => DynLogic s -> (Actions s -> a) -> DynLogicTest s -> Property
withDLScriptPrefix :: (DynLogicModel s, Testable a) => DynFormula s -> (Actions s -> a) -> DynLogicTest s -> Property
generateDLTest :: DynLogicModel s => DynLogic s -> Int -> Gen (DynLogicTest s)
onDLTestSeq :: (TestSequence s -> TestSequence s) -> DynLogicTest s -> DynLogicTest s
consDLTest :: TestStep s -> DynLogicTest s -> DynLogicTest s
consDLTestW :: Witnesses () -> DynLogicTest s -> DynLogicTest s
generate :: (Monad m, DynLogicModel s) => (Annotated s -> Int -> DynLogic s -> m (NextStep s)) -> DynLogic s -> Int -> Annotated s -> Int -> m (DynLogicTest s)
sizeLimit :: Int -> Int
initialStateFor :: StateModel s => DynLogic s -> Annotated s
stopping :: DynLogic s -> DynLogic s
noStopping :: DynLogic s -> DynLogic s
noAny :: DynLogic s -> DynLogic s
nextSteps :: DynLogic s -> Gen [(Double, Witnesses (DynLogic s))]
nextSteps' :: Monad m => (forall a. Quantification a -> m a) -> DynLogic s -> m [(Double, Witnesses (DynLogic s))]
chooseOneOf :: [(Double, a)] -> Gen a
never :: Double
data NextStep s
- = StoppingStep
- | Stepping (Witnesses (Step s)) (DynLogic s)
- | NoStep
- | BadAction (Witnesses (FailingAction s))
chooseNextStep :: DynLogicModel s => Annotated s -> Int -> DynLogic s -> Gen (NextStep s)
chooseUniqueNextStep :: (MonadFail m, DynLogicModel s) => Annotated s -> Int -> DynLogic s -> m (NextStep s)
keepTryingUntil :: Int -> Gen a -> (a -> Bool) -> Gen (Maybe a)
shrinkDLTest :: DynLogicModel s => DynLogic s -> DynLogicTest s -> [DynLogicTest s]
nextStateStep :: StateModel s => Step s -> Annotated s -> Annotated s
shrinkScript :: forall s. DynLogicModel s => DynLogic s -> TestSequence s -> [TestSequence s]
shrinkWitness :: (StateModel s, Typeable a) => DynLogic s -> a -> [a]
pruneDLTest :: forall s. DynLogicModel s => DynLogic s -> TestSequence s -> TestSequence s
stepDL :: DynLogicModel s => DynLogic s -> Annotated s -> TestStep s -> [DynLogic s]
stepDLW :: forall s a. (DynLogicModel s, Typeable a) => DynLogic s -> a -> [DynLogic s]
stepDLSeq :: DynLogicModel s => DynLogic s -> Annotated s -> TestSequence s -> DynLogic s
stepDLWitness :: forall a s. (DynLogicModel s, Typeable a) => DynLogic s -> a -> DynLogic s
stepDLStep :: DynLogicModel s => DynLogic s -> Annotated s -> Step s -> DynLogic s
demonicAlt :: [DynLogic s] -> DynLogic s
propPruningGeneratedScriptIsNoop :: DynLogicModel s => DynLogic s -> Property
getScript :: DynLogicTest s -> TestSequence s
makeTestFromPruned :: forall s. DynLogicModel s => DynLogic s -> TestSequence s -> DynLogicTest s
unfailDLTest :: DynLogicModel s => DynLogic s -> DynLogicTest s -> DynLogicTest s
stuck :: DynLogicModel s => DynLogic s -> Annotated s -> Bool
validDLTest :: StateModel s => DynLogic s -> DynLogicTest s -> Property -> Property
scriptFromDL :: DynLogicTest s -> Actions s
sequenceSteps :: TestSequence s -> [Step s]
badActionsGiven :: StateModel s => DynLogic s -> Annotated s -> Witnesses a -> [Witnesses (FailingAction s)]
badActions :: StateModel s => DynLogic s -> Annotated s -> [FailingAction s]
applyMonitoring :: DynLogicModel s => DynLogic s -> DynLogicTest s -> Property -> Property
findMonitoring :: DynLogicModel s => DynLogic s -> Annotated s -> TestSequence s -> Maybe (Property -> Property)

Documentation

newtype DynFormula s Source #

A DynFormula may depend on the QuickCheck size parameter

Constructors

DynFormula
Fields unDynFormula :: Int -> DynLogic s

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.

Constructors

EmptySpec	False
Stop	True
AfterAny (DynPred s)	After any action the predicate should hold
Alt ChoiceType (DynLogic s) (DynLogic s)	Choice (angelic or demonic)
Stopping (DynLogic s)	Prefer this branch if trying to stop.
forall a.(Eq (Action s a), Show (Action s a), Typeable a) => After (ActionWithPolarity s a) (Var a -> DynPred s)	After a specific action the predicate should hold
Error String (DynPred s)
Weight Double (DynLogic s)	Adjust the probability of picking a branch
forall a.QuantifyConstraints a => ForAll (Quantification a) (a -> DynLogic s)	Generating a random value
Monitor (Property -> Property) (DynLogic s)	Apply a QuickCheck property modifier (like `tabulate` or `collect`)

data ChoiceType Source #

Constructors

Angelic
Demonic

Instances

Instances details

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

type DynPred s = Annotated s -> DynLogic s Source #

Building formulae

ignore :: DynFormula s Source #

Ignore this formula, i.e. backtrack and try something else. forAllScripts ignore (const True) will discard all test cases (equivalent to False ==> True).

passTest :: DynFormula s Source #

True for DL formulae.

afterAny :: (Annotated s -> DynFormula s) -> DynFormula s Source #

Given f must be True given any state.

afterPolar :: (Typeable a, Eq (Action s a), Show (Action s a)) => ActionWithPolarity s a -> (Var a -> Annotated s -> DynFormula s) -> DynFormula s Source #

after :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> (Var a -> Annotated s -> DynFormula s) -> DynFormula s Source #

Given f must be True after some action. f is passed the state resulting from executing the Action.

afterNegative :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> (Annotated s -> DynFormula s) -> DynFormula s Source #

Given f must be True after some negative action. f is passed the state resulting from executing the Action as a negative action.

(|||) :: DynFormula s -> DynFormula s -> DynFormula s Source #

Disjunction for DL formulae. Is True if either formula is True. The choice is angelic, ie. it is always made by the "caller". This is mostly important in case a test is Stuck.

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

First-order quantification of variables. Formula f is True iff. it is True for all possible values of q. The underlying framework will generate values of q and check the formula holds for those values. Quantifiable values are thus values that can be generated and checked and the Quantify module defines basic combinators to build those from building blocks.

weight :: Double -> DynFormula s -> DynFormula s Source #

Adjust weight for selecting formula. This is mostly useful in relation with (|||) combinator, in order to tweak the priority for generating the next step(s) of the test that matches the formula.

withSize :: (Int -> DynFormula s) -> DynFormula s Source #

Get the current QuickCheck size parameter.

toStop :: DynFormula s -> DynFormula s Source #

Prioritise doing this if we are trying to stop generation.

done :: Annotated s -> DynFormula s Source #

Successfully ends the test.

errorDL :: String -> DynFormula s Source #

Ends test with given error message.

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

Embed QuickCheck's monitoring functions (eg. label, tabulate) in a formula. This is useful to improve the reporting from test execution, esp. in the case of failures.

always :: (Annotated s -> DynFormula s) -> Annotated s -> DynFormula s Source #

Formula should hold at any state. In effect this leads to exploring alternatives from a given state s and ensuring formula holds in all those states.

data FailingAction s Source #

Constructors

ErrorFail String
forall a.(Typeable a, Eq (Action s a)) => ActionFail (ActionWithPolarity s a)

Instances

Instances details

StateModel s => Show (FailingAction s) Source #
Instance details Defined in Test.QuickCheck.DynamicLogic.Internal Methods showsPrec :: Int -> FailingAction s -> ShowS # show :: FailingAction s -> String # showList :: [FailingAction s] -> ShowS #
StateModel s => Eq (FailingAction s) Source #
Instance details Defined in Test.QuickCheck.DynamicLogic.Internal Methods (==) :: FailingAction s -> FailingAction s -> Bool # (/=) :: FailingAction s -> FailingAction s -> Bool #
StateModel s => HasVariables (FailingAction s) Source #
Instance details Defined in Test.QuickCheck.DynamicLogic.Internal Methods getAllVariables :: FailingAction s -> Set (Any Var) Source #

data DynLogicTest s Source #

Constructors

BadPrecondition (TestSequence s) (FailingAction s) (Annotated s)
Looping (TestSequence s)
Stuck (TestSequence s) (Annotated s)
DLScript (TestSequence s)

Instances

Instances details

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

data Witnesses r where Source #

Constructors

Do :: r -> Witnesses r
Witness :: QuantifyConstraints a => a -> Witnesses r -> Witnesses r

Instances

Instances details

Foldable Witnesses Source #
Instance details Defined in Test.QuickCheck.DynamicLogic.Internal Methods fold :: Monoid m => Witnesses m -> m # foldMap :: Monoid m => (a -> m) -> Witnesses a -> m # foldMap' :: Monoid m => (a -> m) -> Witnesses a -> m # foldr :: (a -> b -> b) -> b -> Witnesses a -> b # foldr' :: (a -> b -> b) -> b -> Witnesses a -> b # foldl :: (b -> a -> b) -> b -> Witnesses a -> b # foldl' :: (b -> a -> b) -> b -> Witnesses a -> b # foldr1 :: (a -> a -> a) -> Witnesses a -> a # foldl1 :: (a -> a -> a) -> Witnesses a -> a # toList :: Witnesses a -> [a] # null :: Witnesses a -> Bool # length :: Witnesses a -> Int # elem :: Eq a => a -> Witnesses a -> Bool # maximum :: Ord a => Witnesses a -> a # minimum :: Ord a => Witnesses a -> a # sum :: Num a => Witnesses a -> a # product :: Num a => Witnesses a -> a #
Traversable Witnesses Source #
Instance details Defined in Test.QuickCheck.DynamicLogic.Internal Methods traverse :: Applicative f => (a -> f b) -> Witnesses a -> f (Witnesses b) # sequenceA :: Applicative f => Witnesses (f a) -> f (Witnesses a) # mapM :: Monad m => (a -> m b) -> Witnesses a -> m (Witnesses b) # sequence :: Monad m => Witnesses (m a) -> m (Witnesses a) #
Functor Witnesses Source #
Instance details Defined in Test.QuickCheck.DynamicLogic.Internal Methods fmap :: (a -> b) -> Witnesses a -> Witnesses b # (<$) :: a -> Witnesses b -> Witnesses a #
Show r => Show (Witnesses r) Source #
Instance details Defined in Test.QuickCheck.DynamicLogic.Internal Methods showsPrec :: Int -> Witnesses r -> ShowS # show :: Witnesses r -> String # showList :: [Witnesses r] -> ShowS #
Eq r => Eq (Witnesses r) Source #
Instance details Defined in Test.QuickCheck.DynamicLogic.Internal Methods (==) :: Witnesses r -> Witnesses r -> Bool # (/=) :: Witnesses r -> Witnesses r -> Bool #

discardWitnesses :: Witnesses r -> r Source #

pattern Witnesses :: Witnesses () -> r -> Witnesses r Source #

type TestStep s = Witnesses (Step s) Source #

newtype TestSequence s Source #

Constructors

TestSeq (Witnesses (TestContinuation s))

Instances

Instances details

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

data TestContinuation s Source #

Constructors

ContStep (Step s) (TestSequence s)
ContStop

Instances

Instances details

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

pattern TestSeqStop :: TestSequence s Source #

pattern TestSeqStep :: Step s -> TestSequence s -> TestSequence s Source #

pattern TestSeqWitness :: () => forall a. QuantifyConstraints a => a -> TestSequence s -> TestSequence s Source #

consSeq :: TestStep s -> TestSequence s -> TestSequence s Source #

unconsSeq :: TestSequence s -> Maybe (TestStep s, TestSequence s) Source #

unstopSeq :: TestSequence s -> Maybe (Witnesses ()) Source #

pattern TestSeqStopW :: Witnesses () -> TestSequence s Source #

pattern (:>) :: TestStep s -> TestSequence s -> TestSequence s Source #

nullSeq :: TestSequence s -> Bool Source #

dropSeq :: Int -> TestSequence s -> TestSequence s Source #

getContinuation :: TestSequence s -> TestSequence s Source #

unlines' :: [String] -> String Source #

prettyTestSequence :: VarContext -> TestSequence s -> String Source #

prettyWitnesses :: Witnesses () -> [String] Source #

usedVariables :: forall s. StateModel s => TestSequence s -> VarContext Source #

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 #

restrictedPolar :: DynLogicModel s => ActionWithPolarity s a -> Bool Source #