dejafu/doc/refinement_testing.rst

Refinement Testing
==================

Déjà Fu also supports a form of property-testing where you can check
things about the side-effects of stateful operations.  For example, we
can assert that ``readMVar`` is equivalent to sequencing ``takeMVar``
and ``putMVar`` like so:

.. code-block:: haskell

  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!

.. code-block:: none

  > 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
re-exported from ``Test.DejaFu``).


Signatures
----------

A signature tells the property-tester something about the state your
operation acts upon, it has a few components:

.. code-block:: haskell

  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.  For ``readMVar``, the state is some ``MVar a``.

* ``o`` is the **observation type**, it's some pure (and comparable)
  proxy for a snapshot of your mutable state.  For ``MVar a``, the
  observation is probably a ``Maybe a``.

* ``x`` is the **seed type**, it's some pure value used to construct
  the initial mutable state.  For ``MVar a``, the seed is probably a
  ``Maybe a``.

* ``ConcIO`` is just one of the instances of ``MonadConc`` 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 self-explanatory, 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:

.. code-block:: haskell

  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 side-effects on the
state.  The ``interfere`` function can do just about anything [#]_,
but a poor one may result in the property-checker being unable to
distinguish between atomic and nonatomic expressions.

.. [#] There are probably some concrete rules for a good function, but
       I haven't figured them out yet.


Properties
----------

A property is a pair of signatures linked by one of three provided
functions.  These functions are:

.. csv-table::
   :header: "Function", "Operator", "Checks that..."

   "``refines``",         "``=>=``", "...the left is equivalent to, or strictly refines, the right"
   "``strictlyRefines``", "``->-``", "...the left has strictly fewer behaviours than the right"
   "``equivalentTo``",    "``===``", "...the left and right have exactly the same behaviours"

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:

.. code-block:: haskell

  check $ \a b c -> sig1 ... `op` sig2 ...

Under the hood, seed and parameter values are generated using the
LeanCheck_ package, an enumerative property-based testing library.
This means that any types you use will need to have a ``Listable``
instance.

.. _LeanCheck: https://hackage.haskell.org/package/leancheck

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.

.. csv-table::
   :header: "Function", "Result-set operation"

   "``refines``",         "For all seed and parameter assignments, subset-or-equal"
   "``strictlyRefines``", "For at least one seed and parameter assignment, proper subset; for all others, subset-or-equal"
   "``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.

.. __: https://github.com/barrucadu/dejafu/blob/2a15549d97c2fa12f5e8b92ab918fdb34da78281/dejafu-tests/Cases/Refinement.hs


Using HUnit and Tasty
---------------------

As for unit testing, HUnit_ and tasty_ integration is provided for
refinement testing in the hunit-dejafu_ and tasty-dejafu_ packages.

.. _HUnit: https://hackage.haskell.org/package/HUnit
.. _Tasty: https://hackage.haskell.org/package/tasty

.. _hunit-dejafu: https://hackage.haskell.org/package/hunit-dejafu
.. _tasty-dejafu: https://hackage.haskell.org/package/tasty-dejafu

The ``testProperty`` function is used to check properties.  Our example from the start becomes:

.. code-block:: haskell

  testProperty "Read is equivalent to Take then Put" prop_mvar_read_take_put