Copyright  (c) 20152019 Michael Walker 

License  MIT 
Maintainer  Michael Walker <mike@barrucadu.co.uk> 
Stability  stable 
Portability  FlexibleContexts, FlexibleInstances, LambdaCase 
Safe Haskell  SafeInferred 
Language  Haskell2010 
This module allows using Deja Fu predicates with HUnit to test the behaviour of concurrent systems.
Synopsis
 testAuto :: (Eq a, Show a) => Program pty IO a > Test
 testDejafu :: Show b => String > ProPredicate a b > Program pty IO a > Test
 testDejafus :: Show b => [(String, ProPredicate a b)] > Program pty IO a > Test
 testAutoWay :: (Eq a, Show a) => Way > MemType > Program pty IO a > Test
 testDejafuWay :: Show b => Way > MemType > String > ProPredicate a b > Program pty IO a > Test
 testDejafusWay :: Show b => Way > MemType > [(String, ProPredicate a b)] > Program pty IO a > Test
 testAutoWithSettings :: (Eq a, Show a) => Settings IO a > Program pty IO a > Test
 testDejafuWithSettings :: Show b => Settings IO a > String > ProPredicate a b > Program p IO a > Test
 testDejafusWithSettings :: Show b => Settings IO a > [(String, ProPredicate a b)] > Program pty IO a > Test
 data Condition
 type Predicate a = ProPredicate a a
 data ProPredicate a b = ProPredicate {}
 module Test.DejaFu.Settings
 data Program pty (n :: Type > Type) a
 data Basic
 type ConcT = Program Basic
 type ConcIO = ConcT IO
 data WithSetup x
 data WithSetupAndTeardown x y
 withSetup :: forall (n :: Type > Type) x a. Program Basic n x > (x > Program Basic n a) > Program (WithSetup x) n a
 withTeardown :: forall x y (n :: Type > Type) a. (x > Either Condition y > Program Basic n a) > Program (WithSetup x) n y > Program (WithSetupAndTeardown x y) n a
 withSetupAndTeardown :: forall (n :: Type > Type) x y a. Program Basic n x > (x > Either Condition y > Program Basic n a) > (x > Program Basic n y) > Program (WithSetupAndTeardown x y) n a
 data Invariant (n :: Type > Type) a
 registerInvariant :: forall (n :: Type > Type) a. Invariant n a > Program Basic n ()
 inspectIORef :: forall (n :: Type > Type) a. ModelIORef n a > Invariant n a
 inspectMVar :: forall (n :: Type > Type) a. ModelMVar n a > Invariant n (Maybe a)
 inspectTVar :: forall (n :: Type > Type) a. ModelTVar n a > Invariant n a
 testProperty :: (Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) => String > p > Test
 testPropertyFor :: (Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) => Int > Int > String > p > Test
 data Sig s o x = Sig {
 initialise :: x > ConcIO s
 observe :: s > x > ConcIO o
 interfere :: s > x > ConcIO ()
 expression :: s > ConcIO ()
 data RefinementProperty o x
 class Testable a where
 class Listable a where
 expectFailure :: RefinementProperty o x > RefinementProperty o x
 refines :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x
 (=>=) :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x
 strictlyRefines :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x
 (>) :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x
 equivalentTo :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x
 (===) :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x
Unit testing
This is supported by the Assertable
and Testable
instances
for ConcIO
. These instances try all executions, reporting as
failures the cases which throw an HUnitFailure
exception.
instance Testable (ConcIO ())
instance Assertable (ConcIO ())
These instances use defaultWay
and defaultMemType
.
Unit testing
Automatically test a computation. In particular, look for deadlocks, uncaught exceptions, and multiple return values.
Since: 2.0.0.0
:: Show b  
=> String  The name of the test. 
> ProPredicate a b  The predicate to check. 
> Program pty IO a  The computation to test. 
> Test 
Check that a predicate holds.
Since: 2.0.0.0
:: Show b  
=> [(String, ProPredicate a b)]  The list of predicates (with names) to check. 
> Program pty IO a  The computation to test. 
> Test 
Variant of testDejafu
which takes a collection of predicates to
test.
Since: 2.0.0.0
:: (Eq a, Show a)  
=> Way  How to execute the concurrent program. 
> MemType  The memory model to use for nonsynchronised 
> Program pty IO a  The computation to test. 
> Test 
Variant of testAuto
which tests a computation under a given
execution way and memory model.
Since: 2.0.0.0
:: Show b  
=> Way  How to execute the concurrent program. 
> MemType  The memory model to use for nonsynchronised 
> String  The name of the test. 
> ProPredicate a b  The predicate to check. 
> Program pty IO a  The computation to test. 
> Test 
Variant of testDejafu
which takes a way to execute the program
and a memory model.
Since: 2.0.0.0
:: Show b  
=> Way  How to execute the concurrent program. 
> MemType  The memory model to use for nonsynchronised 
> [(String, ProPredicate a b)]  The list of predicates (with names) to check. 
> Program pty IO a  The computation to test. 
> Test 
Variant of testDejafus
which takes a way to execute the program
and a memory model.
Since: 2.0.0.0
:: (Eq a, Show a)  
=> Settings IO a  The SCT settings. 
> Program pty IO a  The computation to test. 
> Test 
Variant of testAuto
which takes a settings record.
Since: 2.0.0.0
testDejafuWithSettings Source #
:: Show b  
=> Settings IO a  The SCT settings. 
> String  The name of the test. 
> ProPredicate a b  The predicate to check. 
> Program p IO a  The computation to test. 
> Test 
Variant of testDejafu
which takes a settings record.
Since: 2.0.0.0
testDejafusWithSettings Source #
:: Show b  
=> Settings IO a  The SCT settings. 
> [(String, ProPredicate a b)]  The list of predicates (with names) to check. 
> Program pty IO a  The computation to test. 
> Test 
Variant of testDejafus
which takes a settings record.
Since: 2.0.0.0
Reexports
An indication of how a concurrent computation terminated, if it didn't produce a value.
The Eq
, Ord
, and NFData
instances compare/evaluate the
exception with show
in the UncaughtException
and
InvariantFailure
cases.
Since: dejafu2.0.0.0
Instances
Generic Condition  
Show Condition  
NFData Condition  
Defined in Test.DejaFu.Types  
Eq Condition  
Ord Condition  
Defined in Test.DejaFu.Types  
type Rep Condition  
Defined in Test.DejaFu.Types type Rep Condition = D1 ('MetaData "Condition" "Test.DejaFu.Types" "dejafu2.4.0.5G4EEj1kXZBX5wEYbPUnAst" 'False) ((C1 ('MetaCons "Abort" 'PrefixI 'False) (U1 :: Type > Type) :+: C1 ('MetaCons "Deadlock" 'PrefixI 'False) (U1 :: Type > Type)) :+: (C1 ('MetaCons "UncaughtException" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SomeException)) :+: C1 ('MetaCons "InvariantFailure" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SomeException)))) 
type Predicate a = ProPredicate a a #
A Predicate
is a function which collapses a list of results
into a Result
, possibly discarding some on the way.
Predicate
cannot be a functor as the type parameter is used both
co and contravariantly.
Since: dejafu1.0.0.0
data ProPredicate a b #
A ProPredicate
is a function which collapses a list of results
into a Result
, possibly discarding some on the way.
Since: dejafu1.0.0.0
Instances
Profunctor ProPredicate  
Defined in Test.DejaFu dimap :: (a > b) > (c > d) > ProPredicate b c > ProPredicate a d # lmap :: (a > b) > ProPredicate b c > ProPredicate a c # rmap :: (b > c) > ProPredicate a b > ProPredicate a c # (#.) :: forall a b c q. Coercible c b => q b c > ProPredicate a b > ProPredicate a c # (.#) :: forall a b c q. Coercible b a => ProPredicate b c > q a b > ProPredicate a c #  
Functor (ProPredicate x)  
Defined in Test.DejaFu fmap :: (a > b) > ProPredicate x a > ProPredicate x b # (<$) :: a > ProPredicate x b > ProPredicate x a # 
Settings
module Test.DejaFu.Settings
Expressing concurrent programs
data Program pty (n :: Type > Type) a #
A representation of a concurrent program for testing.
To construct these, use the MonadConc
instance, or see
withSetup
, withTeardown
, and
withSetupAndTeardown
.
Since: dejafu2.0.0.0
Instances
A type used to constrain Program
: a Program Basic
is a
"basic" program with no setup or teardown.
Construct with the MonadConc
instance.
Since: dejafu2.0.0.0
data WithSetupAndTeardown x y #
A type used to constrain Program
: a Program
(WithSetupAndTeardown x y)
is a program producing a value of type
y
with some setup action producing a value of type x
and a
teardown action producing the final result.
Construct with withTeardown
or
withSetupAndTeardown
.
Since: dejafu2.0.0.0
:: forall (n :: Type > Type) x a. Program Basic n x  Setup action 
> (x > Program Basic n a)  Main program 
> Program (WithSetup x) n a 
A concurrent program with some setup action.
In terms of results, this is the same as setup >>= program
.
However, the setup action will be snapshotted (see
recordSnapshot
and runSnapshot
) by the testing functions. This
means that even if dejafu runs this program many many times, the
setup action will only be run the first time, and its effects
remembered for subsequent executions.
Since: dejafu2.0.0.0
:: forall x y (n :: Type > Type) a. (x > Either Condition y > Program Basic n a)  Teardown action 
> Program (WithSetup x) n y  Main program 
> Program (WithSetupAndTeardown x y) n a 
A concurrent program with some setup and teardown actions.
This is similar to
do x < setup y < program x teardown x y
But with two differences:
 The setup action can be snapshotted, as described for
withSetup
 The teardown action will be executed even if the main action fails to produce a value.
Since: dejafu2.0.0.0
:: forall (n :: Type > Type) x y a. Program Basic n x  Setup action 
> (x > Either Condition y > Program Basic n a)  Teardown action 
> (x > Program Basic n y)  Main program 
> Program (WithSetupAndTeardown x y) n a 
A combination of withSetup
and withTeardown
for convenience.
withSetupAndTeardown setup teardown = withTeardown teardown . withSetup setup
Since: dejafu2.0.0.0
Invariants
data Invariant (n :: Type > Type) a #
Invariants are atomic actions which can inspect the shared state of your computation, and terminate it on failure. Invariants have no visible effects, and are checked after each scheduling point.
To be checked, an invariant must be created during the setup phase
of your Program
, using registerInvariant
. The
invariant will then be checked in the main phase (but not in the
setup or teardown phase). As a consequence of this, any shared
state you want your invariant to check must also be created in the
setup phase, and passed into the main phase as a parameter.
Since: dejafu2.0.0.0
Instances
MonadFail (Invariant n)  
Defined in Test.DejaFu.Conc.Internal.Common  
Applicative (Invariant n)  
Defined in Test.DejaFu.Conc.Internal.Common  
Functor (Invariant n)  
Monad (Invariant n)  
MonadCatch (Invariant n)  
MonadThrow (Invariant n)  
Defined in Test.DejaFu.Conc.Internal.Common 
registerInvariant :: forall (n :: Type > Type) a. Invariant n a > Program Basic n () #
Call this in the setup phase to register new invariant which will be checked after every scheduling point in the main phase. Invariants are atomic actions which can inspect the shared state of your computation.
If the invariant throws an exception, the execution will be aborted
with n InvariantFailure
. Any teardown action will still be run.
Since: dejafu2.0.0.0
inspectIORef :: forall (n :: Type > Type) a. ModelIORef n a > Invariant n a #
Read the content of an IORef
.
This returns the globally visible value, which may not be the same
as the value visible to any particular thread when using a memory
model other than SequentialConsistency
.
Since: dejafu2.0.0.0
inspectMVar :: forall (n :: Type > Type) a. ModelMVar n a > Invariant n (Maybe a) #
Read the content of an MVar
.
This is essentially tryReadMVar
.
Since: dejafu2.0.0.0
inspectTVar :: forall (n :: Type > Type) a. ModelTVar n a > Invariant n a #
Read the content of a TVar
.
This is essentially readTVar
.
Since: dejafu2.0.0.0
Refinement property testing
:: (Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p))  
=> String  The name of the test. 
> p  The property to check. 
> Test 
Check a refinement property with a variety of seed values and variable assignments.
Since: 0.6.0.0
:: (Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p))  
=> Int  The number of seed values to try. 
> Int  The number of variable assignments per seed value to try. 
> String  The name of the test. 
> p  The property to check. 
> Test 
Like testProperty
, but takes a number of cases to check.
The maximum number of cases tried by testPropertyFor n m
will be
n * m
.
Since: 0.7.1.0
Reexports
A concurrent function and some information about how to execute it and observe its effect.
s
is the state type (MVar ConcIO a
in the example)o
is the observation type (Maybe a
in the example)x
is the seed type (Maybe a
in the example)
Since: dejafu0.7.0.0
Sig  

data RefinementProperty o x #
A property which can be given to check
.
Since: dejafu0.7.0.0
Instances
Testable (RefinementProperty o x)  
Defined in Test.DejaFu.Refinement type O (RefinementProperty o x) # type X (RefinementProperty o x) # rpropTiers :: RefinementProperty o x > [[([String], RefinementProperty (O (RefinementProperty o x)) (X (RefinementProperty o x)))]]  
type O (RefinementProperty o x)  
Defined in Test.DejaFu.Refinement  
type X (RefinementProperty o x)  
Defined in Test.DejaFu.Refinement 
Things which can be tested.
Since: dejafu0.7.0.0
rpropTiers
The observation value type. This is used to compare the results.
The seed value type. This is used to construct the concurrent states.
Instances
Testable (RefinementProperty o x)  
Defined in Test.DejaFu.Refinement type O (RefinementProperty o x) # type X (RefinementProperty o x) # rpropTiers :: RefinementProperty o x > [[([String], RefinementProperty (O (RefinementProperty o x)) (X (RefinementProperty o x)))]]  
(Listable a, Show a, Testable b) => Testable (a > b)  
Defined in Test.DejaFu.Refinement rpropTiers :: (a > b) > [[([String], RefinementProperty (O (a > b)) (X (a > b)))]] 
A type is Listable
when there exists a function that
is able to list (ideally all of) its values.
Ideally, instances should be defined by a tiers
function that
returns a (potentially infinite) list of finite sublists (tiers):
the first sublist contains elements of size 0,
the second sublist contains elements of size 1
and so on.
Size here is defined by the implementor of the typeclass instance.
For algebraic data types, the general form for tiers
is
tiers = cons<N> ConstructorA \/ cons<N> ConstructorB \/ ... \/ cons<N> ConstructorZ
where N
is the number of arguments of each constructor A...Z
.
Here is a datatype with 4 constructors and its listable instance:
data MyType = MyConsA  MyConsB Int  MyConsC Int Char  MyConsD String instance Listable MyType where tiers = cons0 MyConsA \/ cons1 MyConsB \/ cons2 MyConsC \/ cons1 MyConsD
The instance for Hutton's Razor is given by:
data Expr = Val Int  Add Expr Expr instance Listable Expr where tiers = cons1 Val \/ cons2 Add
Instances can be alternatively defined by list
.
In this case, each sublist in tiers
is a singleton list
(each succeeding element of list
has +1 size).
The function deriveListable
from Test.LeanCheck.Derive can automatically derive
instances of this typeclass.
A Listable
instance for functions is also available but is not exported by
default. Import Test.LeanCheck.Function if you need to test higherorder
properties.
Instances
Listable Ordering  list :: [Ordering] = [LT, EQ, GT] 
Listable Integer  list :: [Int] = [0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, ...] 
Listable ()  list :: [()] = [()] tiers :: [[()]] = [[()]] 
Defined in Test.LeanCheck.Core  
Listable Bool  tiers :: [[Bool]] = [[False,True]] list :: [[Bool]] = [False,True] 
Listable Char  list :: [Char] = ['a', ' ', 'b', 'A', 'c', '\', 'n', 'd', ...] 
Listable Double 
list :: [Double] = [0.0, 1.0, 1.0, Infinity, 0.5, 2.0, ...] 
Listable Float 
list :: [Float] = [ 0.0 , 1.0, 1.0, Infinity , 0.5, 2.0, Infinity, 0.5, 2.0 , 0.33333334, 3.0, 0.33333334, 3.0 , 0.25, 0.6666667, 1.5, 4.0, 0.25, 0.6666667, 1.5, 4.0 , ... ] 
Listable Int  tiers :: [[Int]] = [[0], [1], [1], [2], [2], [3], [3], ...] list :: [Int] = [0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, ...] 
Listable a => Listable (Maybe a)  tiers :: [[Maybe Int]] = [[Nothing], [Just 0], [Just 1], ...] tiers :: [[Maybe Bool]] = [[Nothing], [Just False, Just True]] 
Listable a => Listable [a]  tiers :: [[ [Int] ]] = [ [ [] ] , [ [0] ] , [ [0,0], [1] ] , [ [0,0,0], [0,1], [1,0], [1] ] , ... ] list :: [ [Int] ] = [ [], [0], [0,0], [1], [0,0,0], ... ] 
Defined in Test.LeanCheck.Core  
(Listable a, Listable b) => Listable (Either a b)  tiers :: [[Either Bool Bool]] = [[Left False, Right False, Left True, Right True]] tiers :: [[Either Int Int]] = [ [Left 0, Right 0] , [Left 1, Right 1] , [Left (1), Right (1)] , [Left 2, Right 2] , ... ] 
(Listable a, Listable b) => Listable (a, b)  tiers :: [[(Int,Int)]] = [ [(0,0)] , [(0,1),(1,0)] , [(0,1),(1,1),(1,0)] , ...] list :: [(Int,Int)] = [ (0,0), (0,1), (1,0), (0,1), (1,1), ...] 
Defined in Test.LeanCheck.Core  
(Listable a, Listable b, Listable c) => Listable (a, b, c)  list :: [(Int,Int,Int)] = [ (0,0,0), (0,0,1), (0,1,0), ...] 
Defined in Test.LeanCheck.Core  
(Listable a, Listable b, Listable c, Listable d) => Listable (a, b, c, d)  
Defined in Test.LeanCheck.Core  
(Listable a, Listable b, Listable c, Listable d, Listable e) => Listable (a, b, c, d, e)  
Defined in Test.LeanCheck.Core 
expectFailure :: RefinementProperty o x > RefinementProperty o x #
Indicates that the property is supposed to fail.
refines :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x #
Observational refinement.
True iff the resultset of the left expression is a subset (not necessarily proper) of the resultset of the right expression.
The two signatures can have different state types, this lets you compare the behaviour of different data structures. The observation and seed types must match, however.
Since: dejafu0.7.0.0
(=>=) :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x #
Infix synonym for refines
.
You might think this should be =<=
, so it looks kind of like a
funny subset operator, with A =<= B
meaning "the resultset of A
is a subset of the resultset of B". Unfortunately you would be
wrong. The operator used in the literature for refinement has the
open end pointing at the LESS general term and the closed end at
the MORE general term. It is read as "is refined by", not
"refines". So for consistency with the literature, the open end
of =>=
points at the less general term, and the closed end at the
more general term, to give the same argument order as refines
.
Since: dejafu0.7.0.0
strictlyRefines :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x #
Strict observational refinement.
True iff the resultset of the left expression is a proper subset of the resultset of the right expression.
The two signatures can have different state types, this lets you compare the behaviour of different data structures. The observation and seed types must match, however.
Since: dejafu0.7.0.0
(>) :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x #
Infix synonym for strictlyRefines
Since: dejafu0.7.0.0
equivalentTo :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x #
Observational equivalence.
True iff the resultset of the left expression is equal to the resultset of the right expression.
The two signatures can have different state types, this lets you compare the behaviour of different data structures. The observation and seed types must match, however.
Since: dejafu0.7.0.0
(===) :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x #
Infix synonym for equivalentTo
.
Since: dejafu0.7.0.0