Test.QuickCheck.DynamicLogic.Internal

Documentation

newtype DynFormula s

A DynFormula may depend on the QuickCheck size parameter

Constructors

DynFormula

Fields

• unDynFormula :: Int -> DynLogic s

data DynLogic s

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

Constructors

Angelic

Demonic

Instances

Show ChoiceType

Defined in Test.QuickCheck.DynamicLogic.Internal

Methods

showsPrec :: Int -> ChoiceType -> ShowS

show :: ChoiceType -> String

showList :: [ChoiceType] -> ShowS

Eq ChoiceType

Defined in Test.QuickCheck.DynamicLogic.Internal

Methods

(==) :: ChoiceType -> ChoiceType -> Bool

(/=) :: ChoiceType -> ChoiceType -> Bool

type DynPred s = Annotated s -> DynLogic s

Building formulae

ignore :: DynFormula s

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

True for DL formulae.

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

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

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

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

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

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

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

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

Get the current QuickCheck size parameter.

toStop :: DynFormula s -> DynFormula s

Prioritise doing this if we are trying to stop generation.

done :: Annotated s -> DynFormula s

Successfully ends the test.

errorDL :: String -> DynFormula s

Ends test with given error message.

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

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

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

Constructors

ErrorFail String

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

Instances

StateModel s => Show (FailingAction s)

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)

Defined in Test.QuickCheck.DynamicLogic.Internal

Methods

(==) :: FailingAction s -> FailingAction s -> Bool

(/=) :: FailingAction s -> FailingAction s -> Bool

StateModel s => HasVariables (FailingAction s)

Defined in Test.QuickCheck.DynamicLogic.Internal

Methods

getAllVariables :: FailingAction s -> Set (Any Var)

data DynLogicTest s

Constructors

BadPrecondition (TestSequence s) (FailingAction s) (Annotated s)

Looping (TestSequence s)

Stuck (TestSequence s) (Annotated s)

DLScript (TestSequence s)

Instances

StateModel s => Show (DynLogicTest s)

Defined in Test.QuickCheck.DynamicLogic.Internal

Methods

showsPrec :: Int -> DynLogicTest s -> ShowS

show :: DynLogicTest s -> String

showList :: [DynLogicTest s] -> ShowS

data Witnesses r where

Constructors

Do :: r -> Witnesses r

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

Instances

Foldable Witnesses

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

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

Defined in Test.QuickCheck.DynamicLogic.Internal

Methods

fmap :: (a -> b) -> Witnesses a -> Witnesses b

(<$) :: a -> Witnesses b -> Witnesses a

Show r => Show (Witnesses r)

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)

Defined in Test.QuickCheck.DynamicLogic.Internal

Methods

(==) :: Witnesses r -> Witnesses r -> Bool

(/=) :: Witnesses r -> Witnesses r -> Bool

discardWitnesses :: Witnesses r -> r

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

type TestStep s = Witnesses (Step s)

newtype TestSequence s

Constructors

TestSeq (Witnesses (TestContinuation s))

Instances

StateModel s => Show (TestSequence s)

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)

Defined in Test.QuickCheck.DynamicLogic.Internal

Methods

(==) :: TestSequence s -> TestSequence s -> Bool

(/=) :: TestSequence s -> TestSequence s -> Bool

data TestContinuation s

Constructors

ContStep (Step s) (TestSequence s)

ContStop

Instances

StateModel s => Show (TestContinuation s)

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)

Defined in Test.QuickCheck.DynamicLogic.Internal

Methods

(==) :: TestContinuation s -> TestContinuation s -> Bool

(/=) :: TestContinuation s -> TestContinuation s -> Bool

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

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

Generate Properties

forAllScripts :: (DynLogicModel s, Testable a) => DynFormula s -> (Actions s -> a) -> Property

Simplest "execution" function for DynFormula. Turns a given a DynFormula paired with an interpreter function to produce some result from an

forAllUniqueScripts :: (DynLogicModel s, Testable a) => Annotated s -> DynFormula s -> (Actions s -> a) -> Property

Property function suitable for formulae without choice.

forAllMappedScripts :: (DynLogicModel s, Testable a) => (rep -> DynLogicTest s) -> (DynLogicTest s -> rep) -> DynFormula s -> (Actions s -> a) -> Property

Creates a Property from DynFormula with some specialised isomorphism for shrinking purpose.

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

Constructors

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

If failed, return the prefix up to the failure. Also prunes the test in case the model has changed.

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)