Test.Tasty.DejaFu

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

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

testAuto

Arguments

:: (Eq a, Show a)

=> Program pty IO a

The computation to test.

-> TestTree

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

Since: 2.0.0.0

testDejafu

Arguments

:: Show b

=> TestName

The name of the test.

-> ProPredicate a b

The predicate to check.

-> Program pty IO a

The computation to test.

-> TestTree

Check that a predicate holds.

Since: 2.0.0.0

testDejafus

Arguments

:: Show b

=> [(TestName, ProPredicate a b)]

The list of predicates (with names) to check.

-> Program pty IO 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: 2.0.0.0

testAutoWay

Arguments

:: (Eq a, Show a)

=> Way

How to execute the concurrent program.

-> MemType

The memory model to use for non-synchronised IORef operations.

-> Program pty IO a

The computation to test.

-> TestTree

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

Since: 2.0.0.0

testDejafuWay

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.

-> Program pty IO a

The computation to test.

-> TestTree

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

Since: 2.0.0.0

testDejafusWay

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.

-> Program pty IO a

The computation to test.

-> TestTree

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

Since: 2.0.0.0

testAutoWithSettings

Arguments

:: (Eq a, Show a)

=> Settings IO a

The SCT settings.

-> Program pty IO a

The computation to test.

-> TestTree

Variant of testAuto which takes a settings record.

Since: 2.0.0.0

testDejafuWithSettings

Arguments

:: Show b

=> Settings IO a

The settings record

-> TestName

The name of the test.

-> ProPredicate a b

The predicate to check.

-> Program pty IO a

The computation to test.

-> TestTree

Variant of testDejafu which takes a settings record.

Since: 2.0.0.0

testDejafusWithSettings

Arguments

:: Show b

=> Settings IO a

The SCT settings.

-> [(TestName, ProPredicate a b)]

The list of predicates (with names) to check.

-> Program pty IO a

The computation to test.

-> TestTree

Variant of testDejafus which takes a settings record.

Since: 2.0.0.0

Re-exports

data Condition

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

Instances

Eq Condition

Defined in Test.DejaFu.Types

Methods

(==) :: Condition -> Condition -> Bool

(/=) :: Condition -> Condition -> Bool

Ord Condition

Defined in Test.DejaFu.Types

Methods

compare :: Condition -> Condition -> Ordering

(<) :: Condition -> Condition -> Bool

(<=) :: Condition -> Condition -> Bool

(>) :: Condition -> Condition -> Bool

(>=) :: Condition -> Condition -> Bool

max :: Condition -> Condition -> Condition

min :: Condition -> Condition -> Condition

Show Condition

Defined in Test.DejaFu.Types

Methods

showsPrec :: Int -> Condition -> ShowS

show :: Condition -> String

showList :: [Condition] -> ShowS

Generic Condition

Defined in Test.DejaFu.Types

Associated Types

type Rep Condition :: Type -> Type

Methods

from :: Condition -> Rep Condition x

to :: Rep Condition x -> Condition

NFData Condition

Defined in Test.DejaFu.Types

Methods

rnf :: Condition -> ()

type Rep Condition

Defined in Test.DejaFu.Types

type Rep Condition = D1 ('MetaData "Condition" "Test.DejaFu.Types" "dejafu-2.4.0.3-3mGbtTqSt0UArHQ7j0hezX" '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: 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

Fields

• pdiscard :: Either Condition a -> Maybe Discard

  Selectively discard results before computing the result.

• peval :: [(Either Condition a, Trace)] -> Result b

  Compute the result with the un-discarded results.

Instances

Profunctor ProPredicate

Defined in Test.DejaFu

Methods

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

Methods

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

Instances

IsTest (ConcIO (Maybe String))

Since: 0.3.0.0

Defined in Test.Tasty.DejaFu

Methods

run :: OptionSet -> ConcIO (Maybe String) -> (Progress -> IO ()) -> IO Result

testOptions :: Tagged (ConcIO (Maybe String)) [OptionDescription]

pty ~ Basic => Monad (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

(>>=) :: Program pty n a -> (a -> Program pty n b) -> Program pty n b

(>>) :: Program pty n a -> Program pty n b -> Program pty n b

return :: a -> Program pty n a

pty ~ Basic => Functor (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

fmap :: (a -> b) -> Program pty n a -> Program pty n b

(<$) :: a -> Program pty n b -> Program pty n a

pty ~ Basic => MonadFail (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

fail :: String -> Program pty n a

pty ~ Basic => Applicative (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

pure :: a -> Program pty n a

(<*>) :: Program pty n (a -> b) -> Program pty n a -> Program pty n b

liftA2 :: (a -> b -> c) -> Program pty n a -> Program pty n b -> Program pty n c

(*>) :: Program pty n a -> Program pty n b -> Program pty n b

(<*) :: Program pty n a -> Program pty n b -> Program pty n a

type ThreadId (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

type ThreadId (Program pty n) = ThreadId

type Ticket (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

type Ticket (Program pty n) = ModelTicket

type IORef (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

type IORef (Program pty n) = ModelIORef n

type MVar (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

type MVar (Program pty n) = ModelMVar n

type STM (Program pty n)

Defined in Test.DejaFu.Conc.Internal.Program

type STM (Program pty n) = ModelSTM n

data Basic

A type used to constrain Program: a Program Basic is a "basic" program with no set-up or teardown.

Construct with the MonadConc instance.

Since: dejafu-2.0.0.0

Instances

IsTest (ConcIO (Maybe String))

Since: 0.3.0.0

Defined in Test.Tasty.DejaFu

Methods

run :: OptionSet -> ConcIO (Maybe String) -> (Progress -> IO ()) -> IO Result

testOptions :: Tagged (ConcIO (Maybe String)) [OptionDescription]

type ConcT = Program Basic

Since: dejafu-1.4.0.0

type ConcIO = ConcT IO

A MonadConc implementation using IO.

Since: dejafu-0.4.0.0

data WithSetup x

A type used to constrain Program: a Program (WithSetup x) is a program with some set-up action producing a value of type x.

Construct with withSetup.

Since: dejafu-2.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 set-up action producing a value of type x and a teardown action producing the final result.

Construct with withTeardown or withSetupAndTeardown.

Since: dejafu-2.0.0.0

withSetup

Arguments

:: 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 set-up 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: dejafu-2.0.0.0

withTeardown

Arguments

:: 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 set-up 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: dejafu-2.0.0.0

withSetupAndTeardown

Arguments

:: 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: dejafu-2.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: dejafu-2.0.0.0

Instances

Monad (Invariant n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

(>>=) :: Invariant n a -> (a -> Invariant n b) -> Invariant n b

(>>) :: Invariant n a -> Invariant n b -> Invariant n b

return :: a -> Invariant n a

Functor (Invariant n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

fmap :: (a -> b) -> Invariant n a -> Invariant n b

(<$) :: a -> Invariant n b -> Invariant n a

MonadFail (Invariant n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

fail :: String -> Invariant n a

Applicative (Invariant n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

pure :: a -> Invariant n a

(<*>) :: Invariant n (a -> b) -> Invariant n a -> Invariant n b

liftA2 :: (a -> b -> c) -> Invariant n a -> Invariant n b -> Invariant n c

(*>) :: Invariant n a -> Invariant n b -> Invariant n b

(<*) :: Invariant n a -> Invariant n b -> Invariant n a

MonadThrow (Invariant n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

throwM :: Exception e => e -> Invariant n a

MonadCatch (Invariant n)

Defined in Test.DejaFu.Conc.Internal.Common

Methods

catch :: Exception e => Invariant n a -> (e -> Invariant n a) -> Invariant n a

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: dejafu-2.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: dejafu-2.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: dejafu-2.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: dejafu-2.0.0.0

Refinement property testing

testProperty

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: 0.6.0.0

testPropertyFor

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

Fields

• initialise :: x -> ConcIO s

  Create a new instance of the state variable.

• observe :: s -> x -> ConcIO o

  The 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

Testable (RefinementProperty o x)

Defined in Test.DejaFu.Refinement

Associated Types

type O (RefinementProperty o x)

type X (RefinementProperty o x)

Methods

rpropTiers :: RefinementProperty o x -> [[([String], RefinementProperty (O (RefinementProperty o x)) (X (RefinementProperty o x)))]]

type X (RefinementProperty o x)

Defined in Test.DejaFu.Refinement

type X (RefinementProperty o x) = x

type O (RefinementProperty o x)

Defined 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)

Defined in Test.DejaFu.Refinement

Associated Types

type O (a -> b)

type X (a -> b)

Methods

rpropTiers :: (a -> b) -> [[([String], RefinementProperty (O (a -> b)) (X (a -> b)))]]

Testable (RefinementProperty o x)

Defined in Test.DejaFu.Refinement

Associated Types

type O (RefinementProperty o x)

type X (RefinementProperty o x)

Methods

rpropTiers :: 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.

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 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

list | tiers

Methods

tiers :: [[a]]

list :: [a]

Instances

Listable Bool

tiers :: [[Bool]]  =  [[False,True]]
list :: [[Bool]]  =  [False,True]

Defined in Test.LeanCheck.Core

Methods

tiers :: [[Bool]]

list :: [Bool]

Listable Char

list :: [Char]  =  ['a', ' ', 'b', 'A', 'c', '\', 'n', 'd', ...]

Defined in Test.LeanCheck.Core

Methods

tiers :: [[Char]]

list :: [Char]

Listable Double

NaN and -0 are not included in the list of Doubles.

list :: [Double]  =  [0.0, 1.0, -1.0, Infinity, 0.5, 2.0, ...]

Defined in Test.LeanCheck.Core

Methods

tiers :: [[Double]]

list :: [Double]

Listable Float

NaN and -0 are not included in the list of Floats.

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
  , ...
  ]

Defined in Test.LeanCheck.Core

Methods

tiers :: [[Float]]

list :: [Float]

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, ...]

Defined in Test.LeanCheck.Core

Methods

tiers :: [[Int]]

list :: [Int]

Listable Integer

list :: [Int]  =  [0, 1, -1, 2, -2, 3, -3, 4, -4, 5, -5, 6, ...]

Defined in Test.LeanCheck.Core

Methods

tiers :: [[Integer]]

list :: [Integer]

Listable Ordering

list :: [Ordering]  =  [LT, EQ, GT]

Defined in Test.LeanCheck.Core

Methods

tiers :: [[Ordering]]

list :: [Ordering]

Listable ()

list :: [()]  =  [()]
tiers :: [[()]]  =  [[()]]

Defined in Test.LeanCheck.Core

Methods

tiers :: [[()]]

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], ... ]

Defined in Test.LeanCheck.Core

Methods

tiers :: [[[a]]]

list :: [[a]]

Listable a => Listable (Maybe a)

tiers :: [[Maybe Int]]  =  [[Nothing], [Just 0], [Just 1], ...]
tiers :: [[Maybe Bool]]  =  [[Nothing], [Just False, Just True]]

Defined in Test.LeanCheck.Core

Methods

tiers :: [[Maybe a]]

list :: [Maybe a]

(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]
                                , ... ]

Defined in Test.LeanCheck.Core

Methods

tiers :: [[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), ...]

Defined in Test.LeanCheck.Core

Methods

tiers :: [[(a, b)]]

list :: [(a, b)]

(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

Methods

tiers :: [[(a, b, c)]]

list :: [(a, b, c)]

(Listable a, Listable b, Listable c, Listable d) => Listable (a, b, c, d)

Defined in Test.LeanCheck.Core

Methods

tiers :: [[(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)

Defined in Test.LeanCheck.Core

Methods

tiers :: [[(a, b, c, d, e)]]

list :: [(a, b, c, d, e)]

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 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

Orphan instances

IsOption Way

Since: 0.5.0.0

Methods

defaultValue :: Way

parseValue :: String -> Maybe Way

optionName :: Tagged Way String

optionHelp :: Tagged Way String

showDefaultValue :: Way -> Maybe String

optionCLParser :: Parser Way

IsOption MemType

Since: 0.3.0.0

Methods

defaultValue :: MemType

parseValue :: String -> Maybe MemType

optionName :: Tagged MemType String

optionHelp :: Tagged MemType String

showDefaultValue :: MemType -> Maybe String

optionCLParser :: Parser MemType

IsTest (ConcIO (Maybe String))

Since: 0.3.0.0

Methods

run :: OptionSet -> ConcIO (Maybe String) -> (Progress -> IO ()) -> IO Result

testOptions :: Tagged (ConcIO (Maybe String)) [OptionDescription]