Safe Haskell	Safe-Inferred
Language	Haskell2010

Test.QuickCheck.DynamicLogic.Core

Synopsis

module Test.QuickCheck.DynamicLogic.Quantify
data DynLogic s
type DynPred s = s -> DynLogic s
data DynFormula 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
ignore :: DynFormula s
passTest :: DynFormula s
afterAny :: (s -> DynFormula s) -> DynFormula s
after :: (Show a, Typeable a, Eq (Action s a)) => Action s a -> (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 :: s -> DynFormula s
errorDL :: String -> DynFormula s
monitorDL :: (Property -> Property) -> DynFormula s -> DynFormula s
always :: (s -> DynFormula s) -> s -> DynFormula s
forAllScripts :: (DynLogicModel s, Testable a) => DynFormula s -> (Actions s -> a) -> Property
forAllScripts_ :: (DynLogicModel s, Testable a) => 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
forAllMappedScripts :: (DynLogicModel s, Testable a, Show rep) => (rep -> DynLogicTest s) -> (DynLogicTest s -> rep) -> DynFormula s -> (Actions s -> a) -> Property
forAllMappedScripts_ :: (DynLogicModel s, Testable a, Show rep) => (rep -> DynLogicTest s) -> (DynLogicTest s -> rep) -> DynFormula s -> (Actions s -> a) -> Property
forAllUniqueScripts :: (DynLogicModel s, Testable a) => Int -> s -> DynFormula s -> (Actions s -> a) -> Property
propPruningGeneratedScriptIsNoop :: DynLogicModel s => DynLogic s -> Property

Documentation

module Test.QuickCheck.DynamicLogic.Quantify

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.

type DynPred s = s -> DynLogic s Source #

data DynFormula s Source #

A DynFormula may depend on the QuickCheck size parameter

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 #

ignore :: DynFormula s Source #

False for DL formulae.

passTest :: DynFormula s Source #

True for DL formulae.

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

Given f must be True given any state.

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

Given f must be True after some action. f is passed the state resulting from executing the 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 #

toStop :: DynFormula s -> DynFormula s Source #

done :: 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 :: (s -> DynFormula s) -> 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.

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

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

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

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

forAllMappedScripts :: (DynLogicModel s, Testable a, Show rep) => (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. ??

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

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

Property function suitable for formulae without choice.

propPruningGeneratedScriptIsNoop :: DynLogicModel s => DynLogic s -> Property Source #