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

Since: 2.0.0.0

Check that a predicate holds.

Since: 2.0.0.0

Variant of testDejafu which takes a collection of predicates to test.

Since: 2.0.0.0

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

Since: 2.0.0.0

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

Since: 2.0.0.0

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

Since: 2.0.0.0

Variant of testAuto which takes a settings record.

Since: 2.0.0.0

Variant of testDejafu which takes a settings record.

Since: 2.0.0.0

Variant of testDejafus which takes a settings record.

Since: 2.0.0.0

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

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

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

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

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

Since: dejafu-1.4.0.0

A MonadConc implementation using IO.

Since: dejafu-0.4.0.0

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

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

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

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

A combination of withSetup and withTeardown for convenience.

withSetupAndTeardown setup teardown =
  withTeardown teardown . withSetup setup

Since: dejafu-2.0.0.0

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

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

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

Read the content of an MVar.

This is essentially tryReadMVar.

Since: dejafu-2.0.0.0

Read the content of a TVar.

This is essentially readTVar.

Since: dejafu-2.0.0.0

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

Since: 0.6.0.0

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

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

A property which can be given to check.

Since: dejafu-0.7.0.0

Things which can be tested.

Since: dejafu-0.7.0.0

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.

Indicates that the property is supposed to fail.

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

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

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

Infix synonym for strictlyRefines

Since: dejafu-0.7.0.0

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

Infix synonym for equivalentTo.

Since: dejafu-0.7.0.0