tasty-dejafu-1.2.0.7: Deja Fu support for the Tasty test framework.

Test.Tasty.DejaFu

Description

This module allows using Deja Fu predicates with Tasty to test the behaviour of concurrent systems.

Synopsis

# Unit testing

This is supported by an IsTest instance for ConcIO. This instance tries all executions, reporting as failures the cases which return a Just string.

instance IsTest (ConcIO (Maybe String)) instance IsOption Bounds instance IsOption MemType

# Unit testing

Arguments

 :: (Eq a, Show a) => ConcIO a The computation to test. -> TestTree

Automatically test a computation. In particular, look for deadlocks, uncaught exceptions, and multiple return values.

Since: tasty-dejafu-1.0.0.0

Arguments

 :: Show b => TestName The name of the test. -> ProPredicate a b The predicate to check. -> ConcIO a The computation to test. -> TestTree

Check that a predicate holds.

Since: tasty-dejafu-1.0.0.0

Arguments

 :: Show b => [(TestName, ProPredicate a b)] The list of predicates (with names) to check. -> ConcIO a The computation to test. -> TestTree

Variant of testDejafu which takes a collection of predicates to test. This will share work between the predicates, rather than running the concurrent computation many times for each predicate.

Since: tasty-dejafu-1.0.0.0

Arguments

 :: (Eq a, Show a) => Way How to execute the concurrent program. -> MemType The memory model to use for non-synchronised IORef operations. -> ConcIO a The computation to test. -> TestTree

Variant of testAuto which tests a computation under a given execution way and memory model.

Since: tasty-dejafu-1.0.0.0

Arguments

 :: Show b => Way How to execute the concurrent program. -> MemType The memory model to use for non-synchronised IORef operations. -> TestName The name of the test. -> ProPredicate a b The predicate to check. -> ConcIO a The computation to test. -> TestTree

Variant of testDejafu which takes a way to execute the program and a memory model.

Since: tasty-dejafu-1.0.0.0

Arguments

 :: Show b => Way How to execute the concurrent program. -> MemType The memory model to use for non-synchronised IORef operations. -> [(TestName, ProPredicate a b)] The list of predicates (with names) to check. -> ConcIO a The computation to test. -> TestTree

Variant of testDejafus which takes a way to execute the program and a memory model.

Since: tasty-dejafu-1.0.0.0

Arguments

 :: (Eq a, Show a) => Settings IO a The SCT settings. -> ConcIO a The computation to test. -> TestTree

Variant of testAuto which takes a settings record.

Since: tasty-dejafu-1.1.0.0

Arguments

 :: Show b => Settings IO a The settings record -> TestName The name of the test. -> ProPredicate a b The predicate to check. -> ConcIO a The computation to test. -> TestTree

Variant of testDejafu which takes a settings record.

Since: tasty-dejafu-1.1.0.0

Arguments

 :: Show b => Settings IO a The SCT settings. -> [(TestName, ProPredicate a b)] The list of predicates (with names) to check. -> ConcIO a The computation to test. -> TestTree

Variant of testDejafus which takes a settings record.

Since: tasty-dejafu-1.1.0.0

## Re-exports

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: dejafu-1.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: dejafu-1.0.0.0

Constructors

 ProPredicate Fieldspdiscard :: Either Failure a -> Maybe DiscardSelectively discard results before computing the result.peval :: [(Either Failure a, Trace)] -> Result bCompute the result with the un-discarded results.
Instances
 Instance detailsDefined in Test.DejaFu Methodsdimap :: (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 #(#.) :: Coercible c b => (b -> c) -> ProPredicate a b -> ProPredicate a c #(.#) :: Coercible b a => ProPredicate b c -> (a -> b) -> ProPredicate a c # Instance detailsDefined in Test.DejaFu Methodsfmap :: (a -> b) -> ProPredicate x a -> ProPredicate x b #(<\$) :: a -> ProPredicate x b -> ProPredicate x a #

# Refinement property testing

Arguments

 :: (Testable p, Listable (X p), Eq (X p), Show (X p), Show (O p)) => TestName The name of the test. -> p The property to check. -> TestTree

Check a refinement property with a variety of seed values and variable assignments.

Since: tasty-dejafu-0.6.0.0

Arguments

 :: (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. -> TestName The name of the test. -> p The property to check. -> TestTree

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: tasty-dejafu-0.7.1.0

## Re-exports

data Sig s o x #

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: dejafu-0.7.0.0

Constructors

 Sig Fieldsinitialise :: x -> ConcIO sCreate a new instance of the state variable.observe :: s -> x -> ConcIO oThe observation to make.interfere :: s -> x -> ConcIO ()Set the state value. This doesn't need to be atomic, or even guaranteed to work, its purpose is to cause interference.expression :: s -> ConcIO ()The expression to evaluate.

data RefinementProperty o x #

A property which can be given to check.

Since: dejafu-0.7.0.0

Instances
 Instance detailsDefined in Test.DejaFu.Refinement Associated Typestype O (RefinementProperty o x) :: * #type X (RefinementProperty o x) :: * # MethodsrpropTiers :: RefinementProperty o x -> [[([String], RefinementProperty (O (RefinementProperty o x)) (X (RefinementProperty o x)))]] type X (RefinementProperty o x) Instance detailsDefined in Test.DejaFu.Refinement type X (RefinementProperty o x) = x type O (RefinementProperty o x) Instance detailsDefined in Test.DejaFu.Refinement type O (RefinementProperty o x) = o

class Testable a #

Things which can be tested.

Since: dejafu-0.7.0.0

Minimal complete definition

rpropTiers

Associated Types

type O a :: * #

The observation value type. This is used to compare the results.

type X a :: * #

The seed value type. This is used to construct the concurrent states.

Instances
 (Listable a, Show a, Testable b) => Testable (a -> b) Instance detailsDefined in Test.DejaFu.Refinement Associated Typestype O (a -> b) :: * #type X (a -> b) :: * # MethodsrpropTiers :: (a -> b) -> [[([String], RefinementProperty (O (a -> b)) (X (a -> b)))]] Instance detailsDefined in Test.DejaFu.Refinement Associated Typestype O (RefinementProperty o x) :: * #type X (RefinementProperty o x) :: * # MethodsrpropTiers :: RefinementProperty o x -> [[([String], RefinementProperty (O (RefinementProperty o x)) (X (RefinementProperty o x)))]]

class Listable a where #

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 sub-lists (tiers): the first sub-list contains elements of size 0, the second sub-list contains elements of size 1 and so on. Size here is defined by the implementor of the type-class 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.

Instances can be alternatively defined by list. In this case, each sub-list 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 higher-order properties.

Minimal complete definition

Methods

tiers :: [[a]] #

list :: [a] #

Instances
 tiers :: [[Bool]] = [[False,True]] list :: [[Bool]] = [False,True] Instance detailsDefined in Test.LeanCheck.Core Methodstiers :: [[Bool]] #list :: [Bool] # Instance detailsDefined in Test.LeanCheck.Core Methodstiers :: [[Char]] #list :: [Char] # Instance detailsDefined in Test.LeanCheck.Core Methodstiers :: [[Double]] #list :: [Double] # Instance detailsDefined in Test.LeanCheck.Core Methodstiers :: [[Float]] #list :: [Float] # tiers :: [[Int]] = [[0], [1], [-1], [2], [-2], [3], [-3], ...] list :: [Int] = [0, 1, -1, 2, -2, 3, -3, 4, -4, 5, -5, 6, ...] Instance detailsDefined in Test.LeanCheck.Core Methodstiers :: [[Int]] #list :: [Int] # Instance detailsDefined in Test.LeanCheck.Core Methodstiers :: [[Integer]] #list :: [Integer] # Instance detailsDefined in Test.LeanCheck.Core Methodstiers :: [[Ordering]] #list :: [Ordering] # Listable () Instance detailsDefined in Test.LeanCheck.Core Methodstiers :: [[()]] #list :: [()] # 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], ... ] Instance detailsDefined in Test.LeanCheck.Core Methodstiers :: [[[a]]] #list :: [[a]] # Listable a => Listable (Maybe a) tiers :: [[Maybe Int]] = [[Nothing], [Just 0], [Just 1], ...] tiers :: [[Maybe Bool]] = [[Nothing], [Just False, Just True]] Instance detailsDefined in Test.LeanCheck.Core Methodstiers :: [[Maybe a]] #list :: [Maybe a] # (Listable a, Listable b) => Listable (Either a b) Instance detailsDefined in Test.LeanCheck.Core Methodstiers :: [[Either a b]] #list :: [Either a b] # (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), ...] Instance detailsDefined in Test.LeanCheck.Core Methodstiers :: [[(a, b)]] #list :: [(a, b)] # (Listable a, Listable b, Listable c) => Listable (a, b, c) Instance detailsDefined in Test.LeanCheck.Core Methodstiers :: [[(a, b, c)]] #list :: [(a, b, c)] # (Listable a, Listable b, Listable c, Listable d) => Listable (a, b, c, d) Instance detailsDefined in Test.LeanCheck.Core Methodstiers :: [[(a, b, c, d)]] #list :: [(a, b, c, d)] # (Listable a, Listable b, Listable c, Listable d, Listable e) => Listable (a, b, c, d, e) Instances for Listable sixtuples up to 12-tuples are exported by default form Test.LeanCheck but are hidden from Haddock documentation. These instances are defined in Test.LeanCheck.Basic. Instance detailsDefined in Test.LeanCheck.Core Methodstiers :: [[(a, b, c, d, e)]] #list :: [(a, b, c, d, e)] #

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 result-set of the left expression is a subset (not necessarily proper) of the result-set 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: dejafu-0.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 result-set of A is a subset of the result-set 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: dejafu-0.7.0.0

strictlyRefines :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x #

Strict observational refinement.

True iff the result-set of the left expression is a proper subset of the result-set 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: dejafu-0.7.0.0

(->-) :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x #

Infix synonym for strictlyRefines

Since: dejafu-0.7.0.0

equivalentTo :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x #

Observational equivalence.

True iff the result-set of the left expression is equal to the result-set 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: dejafu-0.7.0.0

(===) :: Ord o => Sig s1 o x -> Sig s2 o x -> RefinementProperty o x #

Infix synonym for equivalentTo.

Since: dejafu-0.7.0.0

# Deprecated

Arguments

 :: Show b => (Either Failure a -> Maybe Discard) Selectively discard results. -> Way How to execute the concurrent program. -> MemType The memory model to use for non-synchronised IORef operations. -> String The name of the test. -> ProPredicate a b The predicate to check. -> ConcIO a The computation to test. -> TestTree

Variant of testDejafuWay which can selectively discard results.

Since: tasty-dejafu-1.0.0.0

Arguments

 :: Show b => (Either Failure a -> Maybe Discard) Selectively discard results. -> Way How to execute the concurrent program. -> MemType The memory model to use for non-synchronised IORef operations. -> [(TestName, ProPredicate a b)] The list of predicates (with names) to check. -> ConcIO a The computation to test. -> TestTree

Variant of testDejafusWay which can selectively discard results, beyond what each predicate already discards.