Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
LeanCheck is a simple enumerative property-based testing library.
This is the core module of the library, with the most basic definitions. If you are looking just to use the library, import and see Test.LeanCheck.
If you want to understand how the code works, this is the place to start reading.
Other important modules:
- Test.LeanCheck.Basic exports:
Test.LeanCheck.Core,
additional
tiers
constructors (cons6
...cons12
) andListable
tuple instances. - Test.LeanCheck.Tiers exports: functions for advanced Listable definitions.
- Test.LeanCheck exports:
Test.LeanCheck.Basic,
most of Test.LeanCheck.Tiers and
deriveListable
.
- holds :: Testable a => Int -> a -> Bool
- fails :: Testable a => Int -> a -> Bool
- exists :: Testable a => Int -> a -> Bool
- counterExample :: Testable a => Int -> a -> Maybe [String]
- counterExamples :: Testable a => Int -> a -> [[String]]
- witness :: Testable a => Int -> a -> Maybe [String]
- witnesses :: Testable a => Int -> a -> [[String]]
- class Testable a
- results :: Testable a => a -> [([String], Bool)]
- class Listable a where
- cons0 :: a -> [[a]]
- cons1 :: Listable a => (a -> b) -> [[b]]
- cons2 :: (Listable a, Listable b) => (a -> b -> c) -> [[c]]
- cons3 :: (Listable a, Listable b, Listable c) => (a -> b -> c -> d) -> [[d]]
- cons4 :: (Listable a, Listable b, Listable c, Listable d) => (a -> b -> c -> d -> e) -> [[e]]
- cons5 :: (Listable a, Listable b, Listable c, Listable d, Listable e) => (a -> b -> c -> d -> e -> f) -> [[f]]
- ofWeight :: [[a]] -> Int -> [[a]]
- addWeight :: [[a]] -> Int -> [[a]]
- suchThat :: [[a]] -> (a -> Bool) -> [[a]]
- (\/) :: [[a]] -> [[a]] -> [[a]]
- (\\//) :: [[a]] -> [[a]] -> [[a]]
- (><) :: [[a]] -> [[b]] -> [[(a, b)]]
- productWith :: (a -> b -> c) -> [[a]] -> [[b]] -> [[c]]
- mapT :: (a -> b) -> [[a]] -> [[b]]
- filterT :: (a -> Bool) -> [[a]] -> [[a]]
- concatT :: [[[[a]]]] -> [[a]]
- concatMapT :: (a -> [[b]]) -> [[a]] -> [[b]]
- toTiers :: [a] -> [[a]]
- (==>) :: Bool -> Bool -> Bool
- (+|) :: [a] -> [a] -> [a]
- listIntegral :: (Enum a, Num a) => [a]
- tiersFractional :: Fractional a => [[a]]
Checking and testing
holds :: Testable a => Int -> a -> Bool Source #
Does a property hold up to a number of test values?
holds 1000 $ \xs -> length (sort xs) == length xs
fails :: Testable a => Int -> a -> Bool Source #
Does a property fail for a number of test values?
fails 1000 $ \xs -> xs ++ ys == ys ++ xs
exists :: Testable a => Int -> a -> Bool Source #
There exists an assignment of values that satisfies a property up to a number of test values?
exists 1000 $ \x -> x > 10
counterExamples :: Testable a => Int -> a -> [[String]] Source #
Lists all counter-examples for a number of tests to a property,
witnesses :: Testable a => Int -> a -> [[String]] Source #
Lists all witnesses up to a number of tests to a property,
Testable
values are functions
of Listable
arguments that return boolean values,
e.g.:
Bool
Listable a => a -> Bool
Listable a => a -> a -> Bool
Int -> Bool
String -> [Int] -> Bool
resultiers
results :: Testable a => a -> [([String], Bool)] Source #
List all results of a Testable
property.
Each result is a pair of a list of strings and a boolean.
The list of strings is a printable representation of one possible choice of
argument values for the property. Each boolean paired with such a list
indicates whether the property holds for this choice. The outer list is
potentially infinite and lazily evaluated.
Listing test values
class Listable a where Source #
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
.
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.
Constructing lists of tiers
Given a constructor with no arguments,
returns tiers
of all possible applications of this constructor.
Since in this case there is only one possible application (to no
arguments), only a single value, of size/weight 0, will be present in the
resulting list of tiers.
cons3 :: (Listable a, Listable b, Listable c) => (a -> b -> c -> d) -> [[d]] Source #
Returns tiers of applications of a 3-argument constructor.
cons4 :: (Listable a, Listable b, Listable c, Listable d) => (a -> b -> c -> d -> e) -> [[e]] Source #
Returns tiers of applications of a 4-argument constructor.
cons5 :: (Listable a, Listable b, Listable c, Listable d, Listable e) => (a -> b -> c -> d -> e -> f) -> [[f]] Source #
Returns tiers of applications of a 5-argument constructor.
Test.LeanCheck.Basic defines
cons6
up to cons12
.
Those are exported by default from Test.LeanCheck,
but are hidden from the Haddock documentation.
ofWeight :: [[a]] -> Int -> [[a]] Source #
Resets the weight of a constructor (or tiers) Typically used as an infix constructor when defining Listable instances:
cons<N> `ofWeight` <W>
Be careful: do not apply
to recursive data structure
constructors. In general this will make the list of size 0 infinite,
breaking the tier invariant (each tier must be finite).ofWeight
0
suchThat :: [[a]] -> (a -> Bool) -> [[a]] Source #
Tiers of values that follow a property
cons<N> `suchThat` condition
Combining lists of tiers
(\/) :: [[a]] -> [[a]] -> [[a]] infixr 7 Source #
Append tiers --- sum of two tiers enumerations.
[xs,ys,zs,...] \/ [as,bs,cs,...] = [xs++as,ys++bs,zs++cs,...]
(\\//) :: [[a]] -> [[a]] -> [[a]] infixr 7 Source #
Interleave tiers --- sum of two tiers enumerations.
When in doubt, use \/
instead.
[xs,ys,zs,...] \/ [as,bs,cs,...] = [xs+|as,ys+|bs,zs+|cs,...]
(><) :: [[a]] -> [[b]] -> [[(a, b)]] infixr 8 Source #
Take a tiered product of lists of tiers.
[t0,t1,t2,...] >< [u0,u1,u2,...] = [ t0**u0 , t0**u1 ++ t1**u0 , t0**u2 ++ t1**u1 ++ t2**u0 , ... ... ... ... ] where xs ** ys = [(x,y) | x <- xs, y <- ys]
Example:
[[0],[1],[2],...] >< [[0],[1],[2],...] == [ [(0,0)] , [(1,0),(0,1)] , [(2,0),(1,1),(0,2)] , [(3,0),(2,1),(1,2),(0,3)] ... ]
productWith :: (a -> b -> c) -> [[a]] -> [[b]] -> [[c]] Source #
Take a tiered product of lists of tiers.
productWith
can be defined by ><
, as:
productWith f xss yss = map (uncurry f) $ xss >< yss
Manipulating lists of tiers
concatMapT :: (a -> [[b]]) -> [[a]] -> [[b]] Source #
concatMap
over tiers
toTiers :: [a] -> [[a]] Source #
Takes a list of values xs
and transform it into tiers on which each
tier is occupied by a single element from xs
.
To convert back to a list, just concat
.
Boolean (property) operators
(==>) :: Bool -> Bool -> Bool infixr 0 Source #
Boolean implication operator. Useful for defining conditional properties:
prop_something x y = condition x y ==> something x y
Misc utilities
(+|) :: [a] -> [a] -> [a] infixr 5 Source #
Lazily interleaves two lists, switching between elements of the two. Union/sum of the elements in the lists.
[x,y,z] +| [a,b,c] == [x,a,y,b,z,c]
listIntegral :: (Enum a, Num a) => [a] Source #
tiersFractional :: Fractional a => [[a]] Source #
Tiers of Fractional
values.
This can be used as the implementation of tiers
for Fractional
types.