Modulequickcheck-dynamic-4.0.1Haskell2010

Test.QuickCheck.DynamicLogic.Internal

Contents

Building formulae
Generate Properties

Synopsis

newtype DynFormula
data DynLogic
data ChoiceType
type DynPred
value ignore
value passTest
value afterAny
value afterPolar
value after
value afterNegative
value |||
value forAllQ
value weight
value withSize
value toStop
value done
value errorDL
value monitorDL
value always
data FailingAction
data DynLogicTest
data Witnesses
value discardWitnesses
pattern Witnesses
type TestStep
newtype TestSequence
data TestContinuation
pattern TestSeqStop
pattern TestSeqStep
pattern TestSeqWitness
value consSeq
value unconsSeq
value unstopSeq
pattern TestSeqStopW
pattern :>
value nullSeq
value dropSeq
value getContinuation
value unlines'
value prettyTestSequence
value prettyWitnesses
value usedVariables
class DynLogicModel
value restrictedPolar
value forAllScripts
value forAllUniqueScripts
value forAllMappedScripts
value withDLScript
value withDLScriptPrefix
value validDLTest
value generateDLTest
value onDLTestSeq
value consDLTest
value consDLTestW
value generate
value sizeLimit
value initialStateFor
value stopping
value noStopping
value noAny
value nextSteps
value nextSteps'
value chooseOneOf
value never
data NextStep
value chooseNextStep
value chooseUniqueNextStep
value keepTryingUntil
value shrinkDLTest
value nextStateStep
value shrinkScript
value shrinkWitness
value pruneDLTest
value stepDL
value stepDLW
value stepDLSeq
value stepDLWitness
value stepDLStep
value demonicAlt
value propPruningGeneratedScriptIsNoop
value getScript
value makeTestFromPruned
value unfailDLTest
value stuck
value scriptFromDL
value sequenceSteps
value badActionsGiven
value badActions
value applyMonitoring
value findMonitoring

Packagequickcheck-dynamic-4.0.1
Exports90
LanguageHaskell2010
LicenceApache-2.0
SourceInternal.hs

newtypenewtype DynFormula s

Source#

A DynFormula may depend on the QuickCheck size parameter

Constructors

DynFormula
- unDynFormula :: Int -> DynLogic s

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

datadata ChoiceType

Angelic Demonic

Instances2Eq, Show

Eq ChoiceTypeDefined in quickcheck-dynamic-4.0.1 · Test.QuickCheck.DynamicLogic.Internal
Show ChoiceTypeDefined in quickcheck-dynamic-4.0.1 · Test.QuickCheck.DynamicLogic.Internal

typetype DynPred s = Annotated s -> DynLogic s

Building formulae

valueignore :: 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).

valuepassTest :: DynFormula s

Source#

True for DL formulae.

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

Source#

Given f must be True given any state.

valueafterPolar

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

valueafter

:: (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.

valueafterNegative

:: (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.

value(|||) :: 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.

valueforAllQ

:: 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 Test.QuickCheck.DynamicLogic.Quantify module defines basic combinators to build those from building blocks.

valueweight :: 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.

valuewithSize :: (Int -> DynFormula s) -> DynFormula s

Source#

Get the current QuickCheck size parameter.

valuetoStop :: DynFormula s -> DynFormula s

Source#

Prioritise doing this if we are trying to stop generation.

valuedone :: Annotated s -> DynFormula s

Source#

Successfully ends the test.

valueerrorDL :: String -> DynFormula s

Source#

Ends test with given error message.

valuemonitorDL :: (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.

valuealways :: (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.

datadata FailingAction s

Constructors

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

Instances3Eq, Show, HasVariables

StateModel s => Eq (FailingAction s)Defined in quickcheck-dynamic-4.0.1 · Test.QuickCheck.DynamicLogic.Internal
StateModel s => Show (FailingAction s)Defined in quickcheck-dynamic-4.0.1 · Test.QuickCheck.DynamicLogic.Internal
StateModel s => HasVariables (FailingAction s)Defined in quickcheck-dynamic-4.0.1 · Test.QuickCheck.DynamicLogic.Internal

datadata DynLogicTest s

Constructors

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

Instances1Show

StateModel s => Show (DynLogicTest s)Defined in quickcheck-dynamic-4.0.1 · Test.QuickCheck.DynamicLogic.Internal

datadata Witnesses r where

Constructors

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

Instances5Functor, Foldable, Traversable, Eq, Show

Functor WitnessesDefined in quickcheck-dynamic-4.0.1 · Test.QuickCheck.DynamicLogic.Internal
Foldable WitnessesDefined in quickcheck-dynamic-4.0.1 · Test.QuickCheck.DynamicLogic.Internal
Traversable WitnessesDefined in quickcheck-dynamic-4.0.1 · Test.QuickCheck.DynamicLogic.Internal
Eq r => Eq (Witnesses r)Defined in quickcheck-dynamic-4.0.1 · Test.QuickCheck.DynamicLogic.Internal
Show r => Show (Witnesses r)Defined in quickcheck-dynamic-4.0.1 · Test.QuickCheck.DynamicLogic.Internal

valuediscardWitnesses :: Witnesses r -> r

patternpattern Witnesses :: Witnesses () -> r -> Witnesses r

typetype TestStep s = Witnesses (Step s)

newtypenewtype TestSequence s

Constructors

TestSeq (Witnesses (TestContinuation s))

Instances2Eq, Show

StateModel s => Eq (TestSequence s)Defined in quickcheck-dynamic-4.0.1 · Test.QuickCheck.DynamicLogic.Internal
StateModel s => Show (TestSequence s)Defined in quickcheck-dynamic-4.0.1 · Test.QuickCheck.DynamicLogic.Internal

datadata TestContinuation s

Constructors

ContStep (Step s) (TestSequence s)
ContStop

Instances2Eq, Show

StateModel s => Eq (TestContinuation s)Defined in quickcheck-dynamic-4.0.1 · Test.QuickCheck.DynamicLogic.Internal
StateModel s => Show (TestContinuation s)Defined in quickcheck-dynamic-4.0.1 · Test.QuickCheck.DynamicLogic.Internal

patternpattern TestSeqStop :: TestSequence s

patternpattern TestSeqStep :: Step s -> TestSequence s -> TestSequence s

patternpattern TestSeqWitness :: () => QuantifyConstraints a => a -> TestSequence s -> TestSequence s

valueconsSeq :: TestStep s -> TestSequence s -> TestSequence s

valueunconsSeq :: TestSequence s -> Maybe (TestStep s, TestSequence s)

valueunstopSeq :: TestSequence s -> Maybe (Witnesses ())

patternpattern TestSeqStopW :: Witnesses () -> TestSequence s

patternpattern (:>) :: TestStep s -> TestSequence s -> TestSequence s

valuenullSeq :: TestSequence s -> Bool

valuedropSeq :: Int -> TestSequence s -> TestSequence s

valuegetContinuation :: TestSequence s -> TestSequence s

valueunlines' :: [String] -> String

valueprettyTestSequence :: VarContext -> TestSequence s -> String

valueprettyWitnesses :: Witnesses () -> [String]

valueusedVariables :: StateModel s => TestSequence s -> VarContext

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

Methods

restricted :: Action s a -> Bool

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

Generate Properties

valueforAllScripts

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

Source#

Simplest "execution" function for DynFormula. Turns a given a DynFormula paired with an interpreter function to produce some result from an Actions sequence into a proper Property that can be run by QuickCheck.

valueforAllUniqueScripts

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

Source#

Property function suitable for formulae without choice.

valueforAllMappedScripts

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

Source#

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

valuewithDLScript

:: (DynLogicModel s, Testable a)
=> DynLogic s
-> Actions s -> a
-> DynLogicTest s
-> Property

valuewithDLScriptPrefix

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

valuevalidDLTest :: StateModel s => DynLogicTest s -> Property -> Property

Source#

Validate generated test case.

Test case generation does not always produce a valid test case. In some cases, we did not find a suitable test case matching some DynFormula and we are Stuck, hence we want to discard the test case and start over ; in other cases we found a genuine issue with the formula leading to the impossibility of producing a valid test case.

valuegenerateDLTest