Refinement Testing
Déjà Fu also supports a form of propertytesting where you can check things
about the sideeffects of stateful operations. For example, we can assert that
readMVar
is equivalent to sequencing takeMVar
and putMVar
like so:
prop_mvar_read_take_put =
sig readMVar `equivalentTo` sig (\v > takeMVar v >>= putMVar v)
Given the signature function, sig
, defined in the next section. If we check
this, our property fails!
> check prop_mvar_read_take_put
*** Failure: (seed Just 0)
left: [(Nothing,Just 0)]
right: [(Nothing,Just 0),(Just Deadlock,Just 0)]
False
This is because readMVar
is atomic, whereas sequencing takeMVar
with
putMVar
is not, and so another thread can interfere with the MVar
in the
middle. The check
and equivalentTo
functions come from
Test.DejaFu.Refinement
(also reexported from Test.DejaFu
).
Signatures
A signature tells the propertytester something about the state your operation acts upon, it has a few components:
data Sig s o x = Sig
{ initialise :: x > ConcIO s
, observe :: s > x > ConcIO o
, interfere :: s > x > ConcIO ()
, expression :: s > ConcIO ()
}

s
is the state type, it's the thing which your operations mutate. ForreadMVar
, the state is someMVar a
. 
o
is the observation type, it's some pure (and comparable) proxy for a snapshot of your mutable state. ForMVar a
, the observation is probably aMaybe a
. 
x
is the seed type, it's some pure value used to construct the initial mutable state. ForMVar a
, the seed is probably aMaybe a
. 
ConcIO
is just one of the instances ofMonadConc
that Déjà Fu defines for testing purposes. Just write code polymorphic in the monad as usual, and all will work.
The initialise
, observe
, and expression
functions should be
selfexplanatory, but the interfere
one may not be. It's the job of the
interfere
function to change the state in some way; it's run concurrently with
the expression, to simulate the nondeterministic action of other threads.
Here's a concrete example for our MVar
example:
sig :: (MVar ConcIO Int > ConcIO a) > Sig (MVar ConcIO Int) (Maybe Int) (Maybe Int)
sig e = Sig
{ initialise = maybe newEmptyMVar newMVar
, observe = \v _ > tryTakeMVar v
, interfere = \v s > tryTakeMVar v >> maybe (pure ()) (\x > void $ tryPutMVar v (x * 1000)) s
, expression = void . e
}
The observe
function should be deterministic, but as it is run after the
normal execution ends, it may have sideeffects on the state. The interfere
function can do just about anything (there are probably some concrete rules for
a good function, but I haven't figured them out yet), but a poor one may result
in the propertychecker being unable to distinguish between atomic and nonatomic
expressions.
Properties
A property is a pair of signatures linked by one of three provided functions. These functions are:
Function  Operator  Checks that... 

equivalentTo  ===  ... the left and right have exactly the same behaviours 
refines  =>=  ... every behaviour of the left is also a behaviour of the right 
strictlyRefines  >  ... left =>= right holds but left === right does not 
The signatures can have different state types, as long as the seed and
observation types are the same. This lets you compare different implementations
of the same idea: for example, comparing a concurrent stack implemented using
MVar
with one implemented using IORef
.
Properties can have parameters, given in the obvious way:
check $ \a b c > sig1 ... `op` sig2 ...
Under the hood, seed and parameter values are generated using the leancheck
package, an enumerative propertybased testing library. This means that any
types you use will need to have a Listable
instance.
You can also think about the three functions in terms of sets of results, where
a result is a (Maybe Failure, o)
value. A Failure
is something like
deadlocking, or being killed by an exception; o
is the observation type. An
observation is always made, even if execution of the expression fails.
Function  Resultset operation 

refines  For all seed and parameter assignments, subsetorequal 
strictlyRefines  For at least one seed and parameter assignment, proper subset; for all others, subsetorequal 
equivalentTo  For all seed and parameter assignments, equality 
Finally, there is an expectFailure
function, which inverts the expected result
of a property.
The Déjà Fu testsuite has a collection of refinement properties, which may help you get a feel for this sort of testing.
Using HUnit and Tasty
As for unit testing, HUnit and tasty integration is provided for refinement testing in the hunitdejafu and tastydejafu packages.
The testProperty
function is used to check properties. Our example from the
start becomes:
testProperty "Read is equivalent to Take then Put" prop_mvar_read_take_put