Copyright  (c) 2017 Michael Walker 

License  MIT 
Maintainer  Michael Walker <mike@barrucadu.co.uk> 
Stability  experimental 
Portability  FlexibleContexts, FlexibleInstances, GADTs, MultiWayIf, TupleSections, TypeFamilies 
Safe Haskell  None 
Language  Haskell2010 
Properties about the sideeffects of concurrent functions on some shared state.
Consider this statement about MVar
s: "using readMVar
is better
than takeMVar
followed by putMVar
because the former is atomic
but the latter is not."
This module can test properties like that:
sig e = Sig { initialise = maybe newEmptyMVar newMVar , observe = \v _ > tryReadMVar v , interfere = \v s > tryTakeMVar v >> maybe (pure ()) (void . tryPutMVar v) s , expression = e } > check $ sig (void . readMVar) `equivalentTo` sig (\v > takeMVar v >>= putMVar v) *** Failure: (seed Just ()) left: [(Nothing,Just ())] right: [(Nothing,Just ()),(Just Deadlock,Just ())]
The two expressions are not equivalent, and we get given the counterexample!
There are quite a few things going on here, so let's unpack this:
 Properties are specified in terms of an initialisation function, an observation function, an interference function, and the expression of interest.
 The initialisation function (
initialise
) says how to construct some state value from a seed value, which is supplied bycheck
. In this case the seed is of typeMaybe a
and the stateMVar ConcIO a
.  The observation (
observe
) function says how to take the state and the seed, and produce some value which will be used to compare the expressions. In this case the observation value is of typeMaybe a
.  The interference (
interfere
) function says what sort of concurrent interference can happen. In this case we just try to set theMVar
to its original value.
The check
function takes a property, consisting of two signatures
and a way to compare them, evaluates all the results of each
signature, and then compares them in the appropriate way.
See the sections later in the documentation for what "refinement", "strict refinement", and "equivalence" mean exactly.
 data Sig s o x = Sig {
 initialise :: x > ConcIO s
 observe :: s > x > ConcIO o
 interfere :: s > x > ConcIO ()
 expression :: s > ConcIO ()
 data RefinementProperty o x
 expectFailure :: RefinementProperty o x > RefinementProperty o x
 refines :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x
 (=>=) :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x
 strictlyRefines :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x
 (>) :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x
 equivalentTo :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x
 (===) :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x
 data FailedProperty o x
 = CounterExample {
 failingSeed :: x
 failingArgs :: [String]
 leftResults :: Set (Maybe Failure, o)
 rightResults :: Set (Maybe Failure, o)
  NoExpectedFailure
 = CounterExample {
 class Testable a where
 check :: (Testable p, Listable (X p), Show (X p), Show (O p)) => p > IO Bool
 check' :: (Testable p, Listable (X p)) => p > IO (Maybe (FailedProperty (O p) (X p)))
 checkFor :: (Testable p, Listable (X p)) => Int > Int > p > IO (Maybe (FailedProperty (O p) (X p)))
 counterExamples :: (Testable p, Listable (X p)) => Int > Int > p > IO [FailedProperty (O p) (X p)]
 class Listable a where
Defining properties
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: 0.7.0.0
Sig  

data RefinementProperty o x Source #
A property which can be given to check
.
Since: 0.7.0.0
Testable (RefinementProperty o x) Source #  
type O (RefinementProperty o x) Source #  
type X (RefinementProperty o x) Source #  
expectFailure :: RefinementProperty o x > RefinementProperty o x Source #
Indicates that the property is supposed to fail.
A refines B
Refinement (or "weak refinement") means that all of the results of the left are also results of the right. If you think in terms of sets of results, refinement is subset.
refines :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x Source #
Observational refinement.
True iff the resultset of the left expression is a subset (not necessarily proper) of the resultset 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: 0.7.0.0
(=>=) :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x Source #
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 resultset of A
is a subset of the resultset 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: 0.7.0.0
A strictly refines B
Strict refinement means that the left refines the right, but the right does not refine the left. If you think in terms of sets of results, strict refinement is proper subset.
strictlyRefines :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x Source #
Strict observational refinement.
True iff the resultset of the left expression is a proper subset of the resultset 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: 0.7.0.0
(>) :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x Source #
Infix synonym for strictlyRefines
Since: 0.7.0.0
A is equivalent to B
Equivalence means that the left and right refine each other. If you think in terms of sets of results, equivalence is equality.
equivalentTo :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x Source #
Observational equivalence.
True iff the resultset of the left expression is equal to the resultset 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: 0.7.0.0
(===) :: Ord o => Sig s1 o x > Sig s2 o x > RefinementProperty o x Source #
Infix synonym for equivalentTo
.
Since: 0.7.0.0
Testing properties
data FailedProperty o x Source #
A counter example is a seed value and a list of variable assignments.
Since: 0.7.0.0
CounterExample  
 
NoExpectedFailure 
Things which can be tested.
Since: 0.7.0.0
rpropTiers
The observation value type. This is used to compare the results.
The seed value type. This is used to construct the concurrent states.
Check a refinement property with a variety of seed values and variable assignments.
Since: 0.7.0.0
:: (Testable p, Listable (X p))  
=> p  The property to check. 
> IO (Maybe (FailedProperty (O p) (X p))) 
A version of check
that doesn't print, and returns the
counterexample.
Since: 0.7.0.0
:: (Testable p, Listable (X p))  
=> Int  Number of seed values per variableassignment. 
> Int  Number of variable assignments. 
> p  The property to check. 
> IO (Maybe (FailedProperty (O p) (X p))) 
Like check
, but take a number of cases to try, also returns the
counter example found rather than printing it.
If multiple counterexamples exist, this will be faster than
listToMaybe
composed with counterExamples
.
Since: 0.7.0.0
:: (Testable p, Listable (X p))  
=> Int  Number of seed values per variableassignment. 
> Int  Number of variable assignments 
> p  The property to check. 
> IO [FailedProperty (O p) (X p)] 
Find all counterexamples up to a limit.
Since: 0.7.0.0
Reexports
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 sublists (tiers):
the first sublist contains elements of size 0,
the second sublist contains elements of size 1
and so on.
Size here is defined by the implementor of the typeclass 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
.
Instances can be alternatively defined by list
.
In this case, each sublist 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 higherorder
properties.
Listable Bool  tiers :: [[Bool]] = [[False,True]] list :: [[Bool]] = [False,True] 
Listable Char  
Listable Double  
Listable 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, ...] 
Listable Integer  
Listable Ordering  
Listable ()  
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], ... ] 
Listable a => Listable (Maybe a)  tiers :: [[Maybe Int]] = [[Nothing], [Just 0], [Just 1], ...] tiers :: [[Maybe Bool]] = [[Nothing], [Just False, Just True]] 
(Listable a, Listable b) => Listable (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), ...] 
(Listable a, Listable b, Listable c) => Listable (a, b, c)  
(Listable a, Listable b, Listable c, Listable d) => Listable (a, b, c, d)  
(Listable a, Listable b, Listable c, Listable d, Listable e) => Listable (a, b, c, d, e)  Instances for 