| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.QuickCheck.StateModel
Description
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.
Synopsis
- module Test.QuickCheck.StateModel.Variables
- class (forall a. Show (Action state a), forall a. HasVariables (Action state a), Show state, HasVariables state) => StateModel state where
- data Action state a
- type Error state
- actionName :: Action state a -> String
- arbitraryAction :: VarContext -> state -> Gen (Any (Action state))
- shrinkAction :: Typeable a => VarContext -> state -> Action state a -> [Any (Action state)]
- initialState :: state
- nextState :: Typeable a => state -> Action state a -> Var a -> state
- failureNextState :: Typeable a => state -> Action state a -> state
- precondition :: state -> Action state a -> Bool
- validFailingAction :: state -> Action state a -> Bool
- class (forall a. Show (Action state a), Monad m) => RunModel state m where
- perform :: Typeable a => state -> Action state a -> LookUp m -> m (PerformResult (Error state) (Realized m a))
- postcondition :: (state, state) -> Action state a -> LookUp m -> Realized m a -> PostconditionM m Bool
- postconditionOnFailure :: (state, state) -> Action state a -> LookUp m -> Either (Error state) (Realized m a) -> PostconditionM m Bool
- monitoring :: (state, state) -> Action state a -> LookUp m -> Either (Error state) (Realized m a) -> Property -> Property
- monitoringFailure :: state -> Action state a -> LookUp m -> Error state -> Property -> Property
- newtype PostconditionM m a = PostconditionM {}
- data WithUsedVars a = WithUsedVars VarContext a
- data Annotated state = Metadata {
- vars :: VarContext
- underlyingState :: state
- data Step state where
- data Polarity
- data ActionWithPolarity state a = Eq (Action state a) => ActionWithPolarity {
- polarAction :: Action state a
- polarity :: Polarity
- type LookUp m = forall a. Typeable a => Var a -> Realized m a
- data Actions state = Actions_ [String] (Smart [Step state])
- pattern Actions :: [Step state] -> Actions state
- data EnvEntry m where
- 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
- class Generic a
- monitorPost :: Monad m => (Property -> Property) -> PostconditionM m ()
- counterexamplePost :: Monad m => String -> PostconditionM m ()
- stateAfter :: forall state. StateModel state => Actions state -> Annotated state
- runActions :: forall state m e. (StateModel state, RunModel state m, e ~ Error state, forall a. IsPerformResult e a) => Actions state -> PropertyM m (Annotated 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)
- initialAnnotatedState :: StateModel state => Annotated state
- computeNextState :: (StateModel state, Typeable a) => Annotated state -> ActionWithPolarity state a -> Var a -> Annotated state
- computePrecondition :: StateModel state => Annotated state -> ActionWithPolarity state a -> Bool
- computeArbitraryAction :: StateModel state => Annotated state -> Gen (Any (ActionWithPolarity state))
- computeShrinkAction :: forall state a. (Typeable a, StateModel state) => Annotated state -> ActionWithPolarity state a -> [Any (ActionWithPolarity state)]
Documentation
class (forall a. Show (Action state a), forall a. HasVariables (Action state a), Show state, HasVariables state) => StateModel state where Source #
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:
- A datatype for
Actions: Each test case is a sequence ofActions that's supposed to lead from someinitialStateto some end state, - A generator for traces of
Actions, thearbitraryActionfunction, - An
initialState, - A transition function,
nextState, that "interprets" eachActionand producing some newstate.
For finer grained control over the testing process, one can also define:
shrinkAction: Shrinking is an important part of MBT as it allows QuickCheck engine to look for simpler test cases when something goes wrong which makes troubleshooting easier,precondition: Filters generatedActiondepending on thestate. Whenpreconditionis False then the action is rejected and a new one is tried. This is also useful when shrinking a trace in order to ensure that removing someActionstill produces a valid trace. Thepreconditioncan be somewhat redundant with the generator's conditions,validFailingAction: Specifies when an action that fails it'spreconditioncan still run as what is called a _negative_ action. This means that the action is (1) expected to fail and (2) not expected to change the model state. This is very useful for testing the checks and failure conditions in the SUT are implemented correctly. Should it be necessary to update the model state with e.g. book-keeping for a negative action one can definefailureNextState- but it is generally recommended to let this be as simple an action as possible.
Minimal complete definition
Associated Types
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 ()
KillThread :: Var ThreadId -> Action RegState ()
The Spawn action should produce a ThreadId, whereas the KillThread action does not return
anything.
Methods
actionName :: Action state a -> String Source #
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.
arbitraryAction :: VarContext -> state -> Gen (Any (Action state)) Source #
shrinkAction :: Typeable a => VarContext -> state -> Action state a -> [Any (Action state)] Source #
Shrinker for Action.
Defaults to no-op but as usual, defining a good shrinker greatly enhances the usefulness
of property-based testing.
initialState :: state Source #
Initial state of generated traces.
nextState :: Typeable a => state -> Action state a -> Var a -> state Source #
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.
failureNextState :: Typeable a => state -> Action state a -> state Source #
Transition function for negative actions. Note that most negative testing applications should not require an implementation of this function!
precondition :: state -> Action state a -> Bool Source #
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.
validFailingAction :: state -> Action state a -> Bool Source #
Precondition for filtering an Action that can meaningfully run but is supposed to fail.
An action will run as a _negative_ action if the precondition fails and validFailingAction succeeds.
A negative action should have _no effect_ on the model state. This may not be desierable in all
situations - in which case one can override this semantics for book-keeping in failureNextState.
class (forall a. Show (Action state a), Monad m) => RunModel state m where Source #
Minimal complete definition
Methods
perform :: Typeable a => state -> Action state a -> LookUp m -> m (PerformResult (Error state) (Realized m a)) Source #
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.
postcondition :: (state, state) -> Action state a -> LookUp m -> Realized m a -> PostconditionM m Bool Source #
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.
postconditionOnFailure :: (state, state) -> Action state a -> LookUp m -> Either (Error state) (Realized m a) -> PostconditionM m Bool Source #
Postcondition on the result of running a _negative_ Action.
The result is asserted and will make the property fail should it be False. This is useful
to check the implementation produces e.g. the expected errors or to check that the SUT hasn't
been updated during the execution of the negative action.
monitoring :: (state, state) -> Action state a -> LookUp m -> Either (Error state) (Realized m a) -> Property -> Property Source #
Allows the user to attach additional 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.
monitoringFailure :: state -> Action state a -> LookUp m -> Error state -> Property -> Property Source #
Allows the user to attach additional information to the Property if a positive action fails.
newtype PostconditionM m a Source #
Instances
data WithUsedVars a Source #
Constructors
| WithUsedVars VarContext a |
Instances
| Show (WithUsedVars (Step state)) Source # | |
Defined in Test.QuickCheck.StateModel | |
Constructors
| Metadata | |
Fields
| |
data Step state where Source #
Constructors
| (:=) :: (Typeable a, Eq (Action state a), Show (Action state a)) => Var a -> ActionWithPolarity state a -> Step state infix 5 |
Instances
| Show (Step state) Source # | |
| Show (WithUsedVars (Step state)) Source # | |
Defined in Test.QuickCheck.StateModel | |
| Eq (Step state) Source # | |
| (forall a. HasVariables (Action state a)) => HasVariables (Step state) Source # | |
Defined in Test.QuickCheck.StateModel | |
Constructors
| PosPolarity | |
| NegPolarity |
data ActionWithPolarity state a Source #
Constructors
| Eq (Action state a) => ActionWithPolarity | |
Fields
| |
Instances
| Eq (Action state a) => Eq (ActionWithPolarity state a) Source # | |
Defined in Test.QuickCheck.StateModel Methods (==) :: ActionWithPolarity state a -> ActionWithPolarity state a -> Bool # (/=) :: ActionWithPolarity state a -> ActionWithPolarity state a -> Bool # | |
| HasVariables (Action state a) => HasVariables (ActionWithPolarity state a) Source # | |
Defined in Test.QuickCheck.StateModel Methods getAllVariables :: ActionWithPolarity state a -> Set (Any Var) Source # | |
Instances
| StateModel state => Arbitrary (Actions state) Source # | |
| Semigroup (Actions state) Source # | |
| Generic (Actions state) Source # | |
| StateModel state => Show (Actions state) Source # | |
| Eq (Actions state) Source # | |
| type Rep (Actions state) Source # | |
Defined in Test.QuickCheck.StateModel type Rep (Actions state) = D1 ('MetaData "Actions" "Test.QuickCheck.StateModel" "quickcheck-dynamic-3.4.0-5jm8bgdYPgSHb9lOqRV763" 'False) (C1 ('MetaCons "Actions_" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Smart [Step state])))) | |
type family Realized (m :: Type -> Type) a :: Type Source #
Instances
| type Realized Identity a Source # | |
Defined in Test.QuickCheck.StateModel | |
| type Realized IO a Source # | |
Defined in Test.QuickCheck.StateModel | |
| type Realized (ReaderT r m) a Source # | |
Defined in Test.QuickCheck.StateModel | |
| type Realized (StateT s m) a Source # | |
Defined in Test.QuickCheck.StateModel | |
| type Realized (WriterT w m) a Source # | |
Defined in Test.QuickCheck.StateModel | |
Representable types of kind *.
This class is derivable in GHC with the DeriveGeneric flag on.
A Generic instance must satisfy the following laws:
from.to≡idto.from≡id
Instances
monitorPost :: Monad m => (Property -> Property) -> PostconditionM m () Source #
Apply the property transformation to the property after evaluating
the postcondition. Useful for collecting statistics while avoiding
duplication between monitoring and postcondition.
counterexamplePost :: Monad m => String -> PostconditionM m () Source #
Acts as counterexample if the postcondition fails.
stateAfter :: forall state. StateModel state => Actions state -> Annotated state Source #
runActions :: forall state m e. (StateModel state, RunModel state m, e ~ Error state, forall a. IsPerformResult e a) => Actions state -> PropertyM m (Annotated state, Env m) Source #
initialAnnotatedState :: StateModel state => Annotated state Source #
computeNextState :: (StateModel state, Typeable a) => Annotated state -> ActionWithPolarity state a -> Var a -> Annotated state Source #
computePrecondition :: StateModel state => Annotated state -> ActionWithPolarity state a -> Bool Source #
computeArbitraryAction :: StateModel state => Annotated state -> Gen (Any (ActionWithPolarity state)) Source #
computeShrinkAction :: forall state a. (Typeable a, StateModel state) => Annotated state -> ActionWithPolarity state a -> [Any (ActionWithPolarity state)] Source #