diff --git a/doc/refinement_testing.rst b/doc/refinement_testing.rst index 2958261..8ff21fc 100644 --- a/doc/refinement_testing.rst +++ b/doc/refinement_testing.rst @@ -1,5 +1,159 @@ 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