-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | A library for stateful property-based testing -- -- Please see the README on GitHub at -- https://github.com/input-output-hk/quickcheck-dynamic#readme @package quickcheck-dynamic @version 2.0.0 module Test.QuickCheck.DynamicLogic.CanGenerate -- | canGenerate prob g p returns False if we are sure -- Prob(g generates x satisfying p) >= prob otherwise -- True (and we know such an x can be generated). canGenerate :: Double -> Gen a -> (a -> Bool) -> Bool -- | This module defines Quantifications, which are used together with -- forAllQ in DynamicLogic. A `Quantification t` can be used to generate -- a t, shrink a t, and recognise a generated -- t. module Test.QuickCheck.DynamicLogic.Quantify -- | A Quantification over a type a is a generator that can -- be used with forAllQ to generate random values in DL scenarios. -- In addition to a QuickCheck generator a Quantification contains -- a shrinking strategy that ensures that shrunk values stay in the range -- of the generator. data Quantification a isEmptyQ :: Quantification a -> Bool generateQ :: Quantification a -> Gen a shrinkQ :: Quantification a -> a -> [a] -- | Pack up an Arbitrary instance as a Quantification. -- Treats all values as being in range. arbitraryQ :: Arbitrary a => Quantification a -- | Generates exactly the given value. Does not shrink. exactlyQ :: Eq a => a -> Quantification a -- | Pick a random value from a list. Treated as an empty choice if the -- list is empty: -- -- 
--   forAllQ (elementsQ []) == empty
--
elementsQ :: Eq a => [a] -> Quantification a -- | Choose from a list of quantifications. Same as frequencyQ with -- all weights the same (and > 0). oneofQ :: [Quantification a] -> Quantification a -- | Choose from a weighted list of quantifications. Treated as an -- empty choice if no quantification has weight > 0. frequencyQ :: [(Int, Quantification a)] -> Quantification a -- | Quantification is not a Functor, since it also keeps -- track of the range of the generators. However, if you have two -- functions to :: a -> b from :: b -> a satisfying -- from . to = id you can go from a quantification over -- a to one over b. Note that the from -- function need only be defined on the image of to. mapQ :: (a -> b, b -> a) -> Quantification a -> Quantification b -- | Restrict the range of a quantification. whereQ :: Quantification a -> (a -> Bool) -> Quantification a -- | Generate a random value in a given range (inclusive). chooseQ :: (Arbitrary a, Random a, Ord a) => (a, a) -> Quantification a -- | Wrap a `Gen a` generator in a `Quantification a`. Uses given shrinker. withGenQ :: Gen a -> (a -> [a]) -> Quantification a validQuantification :: Show a => Quantification a -> Property -- | Generalization of Quantifications, which lets you treat lists -- and tuples of quantifications as quantifications. For instance, -- -- 
--   ...
--   (die1, die2) <- forAllQ (chooseQ (1, 6), chooseQ (1, 6))
--   ...
--
class (Eq (Quantifies q), Show (Quantifies q), Typeable (Quantifies q)) => Quantifiable q where { -- | The type of values quantified over. -- -- 
    --   Quantifies (Quantification a) = a
    --
type Quantifies q; } -- | Computing the actual Quantification. quantify :: Quantifiable q => q -> Quantification (Quantifies q) instance (GHC.Classes.Eq a, GHC.Show.Show a, Data.Typeable.Internal.Typeable a) => Test.QuickCheck.DynamicLogic.Quantify.Quantifiable (Test.QuickCheck.DynamicLogic.Quantify.Quantification a) instance (Test.QuickCheck.DynamicLogic.Quantify.Quantifiable a, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable b) => Test.QuickCheck.DynamicLogic.Quantify.Quantifiable (a, b) instance (Test.QuickCheck.DynamicLogic.Quantify.Quantifiable a, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable b, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable c) => Test.QuickCheck.DynamicLogic.Quantify.Quantifiable (a, b, c) instance (Test.QuickCheck.DynamicLogic.Quantify.Quantifiable a, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable b, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable c, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable d) => Test.QuickCheck.DynamicLogic.Quantify.Quantifiable (a, b, c, d) instance (Test.QuickCheck.DynamicLogic.Quantify.Quantifiable a, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable b, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable c, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable d, Test.QuickCheck.DynamicLogic.Quantify.Quantifiable e) => Test.QuickCheck.DynamicLogic.Quantify.Quantifiable (a, b, c, d, e) instance Test.QuickCheck.DynamicLogic.Quantify.Quantifiable a => Test.QuickCheck.DynamicLogic.Quantify.Quantifiable [a] module Test.QuickCheck.DynamicLogic.SmartShrinking -- | This combinator captures the 'smart shrinking' implemented for the -- Smart type wrapper in Test.QuickCheck.Modifiers. shrinkSmart :: (a -> [a]) -> Smart a -> [Smart a] module Test.QuickCheck.DynamicLogic.Utils withSize :: Testable prop => (Int -> prop) -> Property -- | Simple (stateful) Model-Based Testing library for use with Haskell -- QuickCheck. -- -- This module provides the basic machinery to define a StateModel -- from which traces can be generated and executed against some -- actual implementation code to define monadic Property to -- be asserted by QuickCheck. module Test.QuickCheck.StateModel -- | The typeclass users implement to define a model against which to -- validate some implementation. -- -- To implement a StateModel, user needs to provide at least the -- following: -- -- -- -- For finer grained control over the testing process, one can also -- define: -- -- class (forall a. Show (Action state a), Show state) => StateModel state where { -- | The type of Action relevant for this state. -- -- This is expected to be defined as a GADT where the a -- parameter is instantiated to some observable output from the SUT a -- given action is expected to produce. For example, here is a fragment -- of the `Action RegState` (taken from the RegistryModel module) -- : -- -- 
    --   data Action RegState a where
    --     Spawn      ::                           Action RegState ThreadId
    --     Register   :: String -> Var ThreadId -> Action RegState (Either ErrorCall ())
    --     KillThread :: Var ThreadId           -> Action RegState ()
    --
-- -- The Spawn action should produce a ThreadId, whereas -- the KillThread action does not return anything. data Action state a; } -- | Display name for Action. This is useful to provide sensible -- statistics about the distribution of Actions run when checking -- a property. -- -- Default implementation uses a poor-man's string manipulation method to -- extract the constructor name from the value. actionName :: StateModel state => Action state a -> String -- | Generator for Action depending on state. The generated -- values are wrapped in Any type to allow the model to not -- generate an action under some circumstances: Any generated -- Error value will be ignored when generating a trace for -- testing. arbitraryAction :: StateModel state => state -> Gen (Any (Action state)) -- | Shrinker for Action. Defaults to no-op but as usual, defining a -- good shrinker greatly enhances the usefulness of property-based -- testing. shrinkAction :: (StateModel state, Typeable a) => state -> Action state a -> [Any (Action state)] -- | Initial state of generated traces. initialState :: StateModel state => state -- | Transition function for the model. The `Var a` parameter is useful to -- keep reference to actual value of type a produced by -- performing the Action inside the state so that -- further actions can use Lookup to retrieve that data. This -- allows the model to be ignorant of those values yet maintain some -- references that can be compared and looked for. nextState :: (StateModel state, Typeable a) => state -> Action state a -> Var a -> state -- | Precondition for filtering generated Action. This function is -- applied before the action is performed, it is useful to refine -- generators that can produce more values than are useful. precondition :: StateModel state => state -> Action state a -> Bool class Monad m => RunModel state m -- | Perform an Action in some state in the Monad -- m. This is the function that's used to exercise the actual -- stateful implementation, usually through various side-effects as -- permitted by m. It produces a value of type a, eg. -- some observable output from the Action that should later be -- kept in the environment through a `Var a` also passed to the -- nextState function. -- -- The Lookup parameter provides an environment to lookup -- `Var a` instances from previous steps. perform :: forall a. (RunModel state m, Typeable a) => state -> Action state a -> LookUp m -> m (Realized m a) -- | Postcondition on the a value produced at some step. The -- result is asserted and will make the property fail should it be -- False. This is useful to check the implementation produces -- expected values. postcondition :: forall a. RunModel state m => (state, state) -> Action state a -> LookUp m -> Realized m a -> m Bool -- | Allows the user to attach information to the Property at each -- step of the process. This function is given the full transition that's -- been executed, including the start and ending state, the -- Action, the current environment to Lookup and the -- value produced by perform while executing this step. monitoring :: forall a. RunModel state m => (state, state) -> Action state a -> LookUp m -> Realized m a -> Property -> Property data Any f [Some] :: (Typeable a, Eq (f a)) => f a -> Any f [Error] :: String -> Any f data Step state [:=] :: (Typeable a, Eq (Action state a), Show (Action state a)) => Var a -> Action state a -> Step state infix 5 := type LookUp m = forall a. Typeable a => Var a -> Realized m a newtype Var a Var :: Int -> Var a data Actions state Actions_ :: [String] -> Smart [Step state] -> Actions state pattern Actions :: [Step state] -> Actions state data EnvEntry m [:==] :: Typeable a => Var a -> Realized m a -> EnvEntry m infix 5 :== pattern (:=?) :: forall a m. Typeable a => Var a -> Realized m a -> EnvEntry m type Env m = [EnvEntry m] type family Realized (m :: Type -> Type) a :: Type stateAfter :: StateModel state => Actions state -> state runActions :: forall state m. (StateModel state, RunModel state m) => Actions state -> PropertyM m (state, Env m) runActionsInState :: forall state m. (StateModel state, RunModel state m) => state -> Actions state -> PropertyM m (state, Env m) lookUpVar :: Typeable a => Env m -> Var a -> Realized m a lookUpVarMaybe :: forall a m. Typeable a => Env m -> Var a -> Maybe (Realized m a) instance Data.Data.Data a => Data.Data.Data (Test.QuickCheck.StateModel.Var a) instance GHC.Show.Show (Test.QuickCheck.StateModel.Var a) instance GHC.Classes.Ord (Test.QuickCheck.StateModel.Var a) instance GHC.Classes.Eq (Test.QuickCheck.StateModel.Var a) instance (forall a. GHC.Show.Show (Test.QuickCheck.StateModel.Action state a)) => GHC.Show.Show (Test.QuickCheck.StateModel.Any (Test.QuickCheck.StateModel.Action state)) instance (forall a. GHC.Show.Show (Test.QuickCheck.StateModel.Action state a)) => GHC.Show.Show (Test.QuickCheck.StateModel.Step state) instance GHC.Base.Semigroup (Test.QuickCheck.StateModel.Actions state) instance GHC.Classes.Eq (Test.QuickCheck.StateModel.Actions state) instance (forall a. GHC.Show.Show (Test.QuickCheck.StateModel.Action state a)) => GHC.Show.Show (Test.QuickCheck.StateModel.Actions state) instance Test.QuickCheck.StateModel.StateModel state => Test.QuickCheck.Arbitrary.Arbitrary (Test.QuickCheck.StateModel.Actions state) instance GHC.Classes.Eq (Test.QuickCheck.StateModel.Step state) instance GHC.Classes.Eq (Test.QuickCheck.StateModel.Any f) module Test.QuickCheck.DynamicLogic.Core -- | 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. data DynLogic s type DynPred s = s -> DynLogic s -- | A DynFormula may depend on the QuickCheck size parameter data DynFormula s -- | 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. class StateModel s => DynLogicModel s restricted :: DynLogicModel s => Action s a -> Bool data DynLogicTest s BadPrecondition :: [TestStep s] -> [Any (Action s)] -> s -> DynLogicTest s Looping :: [TestStep s] -> DynLogicTest s Stuck :: [TestStep s] -> s -> DynLogicTest s DLScript :: [TestStep s] -> DynLogicTest s data TestStep s Do :: Step s -> TestStep s Witness :: a -> TestStep s -- | False for DL formulae. ignore :: DynFormula s -- | True for DL formulae. passTest :: DynFormula s -- | Given f must be True given any state. afterAny :: (s -> DynFormula s) -> DynFormula s -- | Given f must be True after some action. -- f is passed the state resulting from executing the -- Action. after :: (Typeable a, Eq (Action s a)) => Action s a -> (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. (|||) :: DynFormula s -> 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. forAllQ :: Quantifiable q => q -> (Quantifies q -> 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. weight :: Double -> DynFormula s -> DynFormula s withSize :: (Int -> DynFormula s) -> DynFormula s toStop :: DynFormula s -> DynFormula s -- | Successfully ends the test. done :: s -> DynFormula s -- | Ends test with given error message. errorDL :: String -> 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. monitorDL :: (Property -> Property) -> DynFormula 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. always :: (s -> DynFormula s) -> s -> DynFormula s -- | 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 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 -- | 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 forAllMappedScripts_ :: (DynLogicModel s, Testable a, Show rep) => (rep -> DynLogicTest s) -> (DynLogicTest s -> rep) -> DynFormula s -> (Actions s -> a) -> Property -- | Property function suitable for formulae without choice. forAllUniqueScripts :: (DynLogicModel s, Testable a) => Int -> s -> DynFormula s -> (Actions s -> a) -> Property propPruningGeneratedScriptIsNoop :: DynLogicModel s => DynLogic s -> Property instance GHC.Show.Show Test.QuickCheck.DynamicLogic.Core.ChoiceType instance GHC.Classes.Eq Test.QuickCheck.DynamicLogic.Core.ChoiceType instance Test.QuickCheck.StateModel.StateModel s => GHC.Show.Show (Test.QuickCheck.DynamicLogic.Core.DynLogicTest s) instance GHC.Classes.Eq (Test.QuickCheck.DynamicLogic.Core.TestStep s) instance Test.QuickCheck.StateModel.StateModel s => GHC.Show.Show (Test.QuickCheck.DynamicLogic.Core.TestStep s) -- | 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. module Test.QuickCheck.DynamicLogic -- | 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. data DL s a action :: (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 -- | Fail if the boolean is False. -- -- Equivalent to -- -- 
--   assert msg b = unless b (fail msg)
--
assert :: String -> Bool -> DL s () assertModel :: String -> (s -> Bool) -> DL s () monitorDL :: (Property -> Property) -> DL s () -- | 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. 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 -- | 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. data DynLogic s -- | 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. class StateModel s => DynLogicModel s restricted :: DynLogicModel s => Action s a -> Bool data DynLogicTest s BadPrecondition :: [TestStep s] -> [Any (Action s)] -> s -> DynLogicTest s Looping :: [TestStep s] -> DynLogicTest s Stuck :: [TestStep s] -> s -> DynLogicTest s DLScript :: [TestStep s] -> DynLogicTest s data TestStep s Do :: Step s -> TestStep s Witness :: a -> TestStep s instance GHC.Base.Functor (Test.QuickCheck.DynamicLogic.DL s) instance GHC.Base.Applicative (Test.QuickCheck.DynamicLogic.DL s) instance GHC.Base.Alternative (Test.QuickCheck.DynamicLogic.DL s) instance GHC.Base.Monad (Test.QuickCheck.DynamicLogic.DL s) instance Control.Monad.Fail.MonadFail (Test.QuickCheck.DynamicLogic.DL s)