Copyright	(c) 2017--2021 Michael Walker
License	MIT
Maintainer	Michael Walker <mike@barrucadu.co.uk>
Stability	experimental
Portability	FlexibleContexts, FlexibleInstances, GADTs, MultiWayIf, TupleSections, TypeFamilies
Safe Haskell	Safe-Inferred
Language	Haskell2010

Test.DejaFu.Refinement

Contents

Defining properties
Testing properties
Re-exports

Description

Properties about the side-effects of concurrent functions on some shared state.

Consider this statement about MVars: "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:

>>> import Control.Monad (void)
>>> :{
let sig e = Sig
      { initialise = maybe newEmptyMVar newMVar
      , observe    = \v _ -> tryReadMVar v
      , interfere  = \v _ -> putMVar v 42
      , expression = void . e
      }
:}

>>> check $ sig readMVar === sig (\v -> takeMVar v >>= putMVar v)
*** Failure: (seed Just 0)
    left:  [(Nothing,Just 0)]
    right: [(Nothing,Just 0),(Just Deadlock,Just 42)]
False

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 by check. In this case the seed is of type Maybe a and the state MVar 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 type Maybe a.
The interference (interfere) function says what sort of concurrent interference can happen. In this case we just try to set the MVar 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.

Synopsis

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 Condition, o)
  - rightResults :: Set (Maybe Condition, o)
  }
- | NoExpectedFailure
class Testable a where
- type O a :: Type
- type X a :: Type
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
- tiers :: [[a]]
- list :: [a]

Defining properties

data Sig s o x Source #

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

Constructors

Sig
Fields initialise :: x -> ConcIO s Create a new instance of the state variable. observe :: s -> x -> ConcIO o The observation to make. interfere :: s -> x -> ConcIO () Set the state value. This doesn't need to be atomic, or even guaranteed to work, its purpose is to cause interference. expression :: s -> ConcIO () The expression to evaluate.

data RefinementProperty o x Source #

A property which can be given to check.

Since: 0.7.0.0

Instances

Instances details

Testable (RefinementProperty o x) Source #
Instance details Defined in Test.DejaFu.Refinement Associated Types type O (RefinementProperty o x) Source # type X (RefinementProperty o x) Source # Methods rpropTiers :: RefinementProperty o x -> [[([String], RefinementProperty (O (RefinementProperty o x)) (X (RefinementProperty o x)))]]
type O (RefinementProperty o x) Source #
Instance details Defined in Test.DejaFu.Refinement type O (RefinementProperty o x) = o
type X (RefinementProperty o x) Source #
Instance details Defined in Test.DejaFu.Refinement type X (RefinementProperty o x) = x

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 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: 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 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: 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 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: 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 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: 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

Constructors

CounterExample
Fields failingSeed :: x The seed for this set of executions. failingArgs :: [String] The values of free variables, as strings. leftResults :: Set (Maybe Condition, o) The set of results of the left signature. rightResults :: Set (Maybe Condition, o) The set of results of the right signature.
NoExpectedFailure

Instances

Instances details

(Show x, Show o) => Show (FailedProperty o x) Source #
Instance details Defined in Test.DejaFu.Refinement Methods showsPrec :: Int -> FailedProperty o x -> ShowS # show :: FailedProperty o x -> String # showList :: [FailedProperty o x] -> ShowS #

class Testable a Source #

Things which can be tested.

Since: 0.7.0.0

Minimal complete definition

rpropTiers

Associated Types

type O a :: Type Source #

The observation value type. This is used to compare the results.

type X a :: Type Source #

The seed value type. This is used to construct the concurrent states.

Instances

Instances details

Testable (RefinementProperty o x) Source #
Instance details Defined in Test.DejaFu.Refinement Associated Types type O (RefinementProperty o x) Source # type X (RefinementProperty o x) Source # Methods rpropTiers :: RefinementProperty o x -> [[([String], RefinementProperty (O (RefinementProperty o x)) (X (RefinementProperty o x)))]]
(Listable a, Show a, Testable b) => Testable (a -> b) Source #
Instance details Defined in Test.DejaFu.Refinement Associated Types type O (a -> b) Source # type X (a -> b) Source # Methods rpropTiers :: (a -> b) -> [[([String], RefinementProperty (O (a -> b)) (X (a -> b)))]]

check Source #

Arguments

:: (Testable p, Listable (X p), Show (X p), Show (O p))
=> p	The property to check.
-> IO Bool

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

Since: 0.7.0.0

check' Source #

Arguments

:: (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

checkFor Source #

Arguments

:: (Testable p, Listable (X p))
=> Int	Number of seed values per variable-assignment.
-> 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

counterExamples Source #

Arguments

:: (Testable p, Listable (X p))
=> Int	Number of seed values per variable-assignment.
-> 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

Re-exports

class Listable a where #

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.

Minimal complete definition

list | tiers

Methods

tiers :: [[a]] #

list :: [a] #

Instances

Instances details

Listable Ordering	list :: [Ordering] = [LT, EQ, GT]
Instance details Defined in Test.LeanCheck.Core Methods tiers :: [[Ordering]] # list :: [Ordering] #
Listable Integer	list :: [Int] = [0, 1, -1, 2, -2, 3, -3, 4, -4, 5, -5, 6, ...]
Instance details Defined in Test.LeanCheck.Core Methods tiers :: [[Integer]] # list :: [Integer] #
Listable ()	list :: [()] = [()] tiers :: [[()]] = [[()]]
Instance details Defined in Test.LeanCheck.Core Methods tiers :: [[()]] # list :: [()] #
Listable Bool	tiers :: [[Bool]] = [[False,True]] list :: [[Bool]] = [False,True]
Instance details Defined in Test.LeanCheck.Core Methods tiers :: [[Bool]] # list :: [Bool] #
Listable Char	list :: [Char] = ['a', ' ', 'b', 'A', 'c', '\', 'n', 'd', ...]
Instance details Defined in Test.LeanCheck.Core Methods tiers :: [[Char]] # list :: [Char] #
Listable Double	`NaN` and `-0` are not included in the list of `Double`s. list :: [Double] = [0.0, 1.0, -1.0, Infinity, 0.5, 2.0, ...]
Instance details Defined in Test.LeanCheck.Core Methods tiers :: [[Double]] # list :: [Double] #
Listable Float	`NaN` and `-0` are not included in the list of `Float`s. list :: [Float] = [ 0.0 , 1.0, -1.0, Infinity , 0.5, 2.0, -Infinity, -0.5, -2.0 , 0.33333334, 3.0, -0.33333334, -3.0 , 0.25, 0.6666667, 1.5, 4.0, -0.25, -0.6666667, -1.5, -4.0 , ... ]
Instance details Defined in Test.LeanCheck.Core Methods tiers :: [[Float]] # list :: [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, ...]
Instance details Defined in Test.LeanCheck.Core Methods tiers :: [[Int]] # list :: [Int] #
Listable a => Listable (Maybe a)	tiers :: [[Maybe Int]] = [[Nothing], [Just 0], [Just 1], ...] tiers :: [[Maybe Bool]] = [[Nothing], [Just False, Just True]]
Instance details Defined in Test.LeanCheck.Core Methods tiers :: [[Maybe a]] # list :: [Maybe a] #
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], ... ]
Instance details Defined in Test.LeanCheck.Core Methods tiers :: [[[a]]] # list :: [[a]] #
(Listable a, Listable b) => Listable (Either a b)	tiers :: [[Either Bool Bool]] = [[Left False, Right False, Left True, Right True]] tiers :: [[Either Int Int]] = [ [Left 0, Right 0] , [Left 1, Right 1] , [Left (-1), Right (-1)] , [Left 2, Right 2] , ... ]
Instance details Defined in Test.LeanCheck.Core Methods tiers :: [[Either a b]] # list :: [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), ...]
Instance details Defined in Test.LeanCheck.Core Methods tiers :: [[(a, b)]] # list :: [(a, b)] #
(Listable a, Listable b, Listable c) => Listable (a, b, c)	list :: [(Int,Int,Int)] = [ (0,0,0), (0,0,1), (0,1,0), ...]
Instance details Defined in Test.LeanCheck.Core Methods tiers :: [[(a, b, c)]] # list :: [(a, b, c)] #
(Listable a, Listable b, Listable c, Listable d) => Listable (a, b, c, d)
Instance details Defined in Test.LeanCheck.Core Methods tiers :: [[(a, b, c, d)]] # list :: [(a, b, c, d)] #
(Listable a, Listable b, Listable c, Listable d, Listable e) => Listable (a, b, c, d, e)
Instance details Defined in Test.LeanCheck.Core Methods tiers :: [[(a, b, c, d, e)]] # list :: [(a, b, c, d, e)] #