Copyright | (c) 2016-2017 Rudy Matela |
---|---|
License | 3-Clause BSD (see the file LICENSE) |
Maintainer | Rudy Matela <rudy@matela.com.br> |
Safe Haskell | None |
Language | Haskell2010 |
Speculate: discovery of properties by reasoning from test results
Speculate automatically discovers laws about Haskell functions. Those laws involve:
- equations, such as
id x == x
; - inequalities, such as
0 <= x * x
; - conditional equations, such as
x <= 0 ==> x + abs x == 0
.
_Example:_ the following program prints laws about 0
, 1
, +
and abs
.
import Test.Speculate main :: IO () main = speculate args { constants = [ showConstant (0::Int) , showConstant (1::Int) , constant "+" ((+) :: Int -> Int -> Int) , constant "abs" (abs :: Int -> Int) , background , constant "<=" ((<=) :: Int -> Int -> Bool) ] }
Synopsis
- speculate :: Args -> IO ()
- data Args = Args {
- maxSize :: Int
- maxTests :: Int
- constants :: [Expr]
- instances :: [Instances]
- maxSemiSize :: Int
- maxCondSize :: Int
- maxVars :: Int
- showConstants :: Bool
- showEquations :: Bool
- showSemiequations :: Bool
- showConditions :: Bool
- showConstantLaws :: Bool
- autoConstants :: Bool
- minTests :: Int -> Int
- maxConstants :: Maybe Int
- maxDepth :: Maybe Int
- showCounts :: Bool
- showTheory :: Bool
- showArgs :: Bool
- showHelp :: Bool
- evalTimeout :: Maybe Double
- force :: Bool
- extra :: [String]
- exclude :: [String]
- onlyTypes :: [String]
- showClassesFor :: [Int]
- showDot :: Bool
- quietDot :: Bool
- args :: Args
- data Expr
- constant :: Typeable a => String -> a -> Expr
- showConstant :: (Typeable a, Show a) => a -> Expr
- hole :: (Listable a, Typeable a) => a -> Expr
- foreground :: Expr
- background :: Expr
- type Instances = [Instance]
- ins :: (Typeable a, Listable a, Show a, Eq a, Ord a) => String -> a -> Instances
- eq :: (Typeable a, Eq a) => a -> Instances
- ord :: (Typeable a, Ord a) => a -> Instances
- eqWith :: (Typeable a, Eq a) => (a -> a -> Bool) -> Instances
- ordWith :: (Typeable a, Ord a) => (a -> a -> Bool) -> Instances
- names :: Instances -> TypeRep -> [String]
- report :: Args -> IO ()
- getArgs :: Args -> IO Args
- module Test.LeanCheck
- uint4 :: UInt4
- uint3 :: UInt3
- uint2 :: UInt2
- uint1 :: UInt1
- int4 :: Int4
- int3 :: Int3
- int2 :: Int2
- int1 :: Int1
- nat :: Nat
- eith :: a -> b -> Either a b
- mayb :: a -> Maybe a
- ordering :: Ordering
- string :: String
- char :: Char
- bool :: Bool
- rational :: Rational
- double :: Double
- float :: Float
- integer :: Integer
- int :: Int
- und :: a
- (>-) :: a -> b -> a -> b
- (->>>>>>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m) -> m -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m
- (->>>>>>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m) -> m -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m
- (->>>>>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l) -> l -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l
- (->>>>>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l) -> k -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l
- (->>>>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k) -> k -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k
- (->>>>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k) -> j -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k
- (->>>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> j -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j
- (->>>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> i -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j
- (->>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i) -> i -> a -> b -> c -> d -> e -> f -> g -> h -> i
- (->>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i) -> h -> a -> b -> c -> d -> e -> f -> g -> h -> i
- (->>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h) -> h -> a -> b -> c -> d -> e -> f -> g -> h
- (->>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h) -> g -> a -> b -> c -> d -> e -> f -> g -> h
- (->>>>>>:) :: (a -> b -> c -> d -> e -> f -> g) -> g -> a -> b -> c -> d -> e -> f -> g
- (->>>>>:>) :: (a -> b -> c -> d -> e -> f -> g) -> f -> a -> b -> c -> d -> e -> f -> g
- (->>>>>:) :: (a -> b -> c -> d -> e -> f) -> f -> a -> b -> c -> d -> e -> f
- (->>>>:>) :: (a -> b -> c -> d -> e -> f) -> e -> a -> b -> c -> d -> e -> f
- (->>>>:) :: (a -> b -> c -> d -> e) -> e -> a -> b -> c -> d -> e
- (->>>:>) :: (a -> b -> c -> d -> e) -> d -> a -> b -> c -> d -> e
- (->>>:) :: (a -> b -> c -> d) -> d -> a -> b -> c -> d
- (->>:>) :: (a -> b -> c -> d) -> c -> a -> b -> c -> d
- (->>:) :: (a -> b -> c) -> c -> a -> b -> c
- (->:>) :: (a -> b -> c) -> b -> a -> b -> c
- (->:) :: (a -> b) -> b -> a -> b
- (-:>) :: (a -> b) -> a -> a -> b
- (-:) :: a -> a -> a
- newtype Int1 = Int1 {}
- newtype Int2 = Int2 {}
- newtype Int3 = Int3 {}
- newtype Int4 = Int4 {}
- newtype Word1 = Word1 {}
- newtype Word2 = Word2 {}
- newtype Word3 = Word3 {}
- newtype Word4 = Word4 {}
- newtype Nat = Nat {}
- newtype Nat1 = Nat1 {}
- newtype Nat2 = Nat2 {}
- newtype Nat3 = Nat3 {}
- newtype Nat4 = Nat4 {}
- newtype Nat5 = Nat5 {}
- newtype Nat6 = Nat6 {}
- newtype Nat7 = Nat7 {}
- type UInt1 = Word1
- type UInt2 = Word2
- type UInt3 = Word3
- type UInt4 = Word4
- newtype NoDup a = NoDup [a]
- newtype Bag a = Bag [a]
- newtype Set a = Set [a]
- newtype Map a b = Map [(a, b)]
- newtype X a = X {
- unX :: a
- newtype Xs a = Xs {
- unXs :: [a]
- (|=) :: (a -> Bool) -> a -> Bool
- (=|) :: Eq a => [a] -> Int -> [a] -> Bool
- ($=) :: (a -> Bool) -> a -> Bool
- (=$) :: Eq b => a -> (a -> b) -> a -> Bool
- okNum :: (Eq a, Num a) => a -> a -> a -> Bool
- okEqOrd :: (Eq a, Ord a) => a -> a -> a -> Bool
- okOrd :: Ord a => a -> a -> a -> Bool
- okEq :: Eq a => a -> a -> a -> Bool
- neverIdentity :: Eq a => (a -> a) -> a -> Bool
- identity :: Eq a => (a -> a) -> a -> Bool
- idempotent :: Eq a => (a -> a) -> a -> Bool
- strictTotalOrder :: Eq a => (a -> a -> Bool) -> a -> a -> a -> Bool
- totalOrder :: Eq a => (a -> a -> Bool) -> a -> a -> a -> Bool
- strictPartialOrder :: (a -> a -> Bool) -> a -> a -> a -> Bool
- partialOrder :: Eq a => (a -> a -> Bool) -> a -> a -> a -> Bool
- equivalence :: (a -> a -> Bool) -> a -> a -> a -> Bool
- asymmetric :: (a -> a -> Bool) -> a -> a -> Bool
- antisymmetric :: Eq a => (a -> a -> Bool) -> a -> a -> Bool
- symmetric :: (a -> a -> Bool) -> a -> a -> Bool
- irreflexive :: (a -> a -> Bool) -> a -> Bool
- reflexive :: (a -> a -> Bool) -> a -> Bool
- transitive :: (a -> a -> Bool) -> a -> a -> a -> Bool
- symmetric2 :: Eq b => (a -> a -> b) -> (a -> a -> b) -> a -> a -> Bool
- distributive :: Eq a => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool
- associative :: Eq a => (a -> a -> a) -> a -> a -> a -> Bool
- commutative :: Eq b => (a -> a -> b) -> a -> a -> Bool
- (||||) :: (a -> b -> Bool) -> (a -> b -> Bool) -> a -> b -> Bool
- (|||) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
- (&&&&) :: (a -> b -> Bool) -> (a -> b -> Bool) -> a -> b -> Bool
- (&&&) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
- (====) :: Eq c => (a -> b -> c) -> (a -> b -> c) -> a -> b -> Bool
- (===) :: Eq b => (a -> b) -> (a -> b) -> a -> Bool
- countsOn :: Eq b => (a -> b) -> [a] -> [(b, Int)]
- countsBy :: (a -> a -> Bool) -> [a] -> [(a, Int)]
- counts :: Eq a => [a] -> [(a, Int)]
- classifyOn :: Eq b => (a -> b) -> [a] -> [[a]]
- classifyBy :: (a -> a -> Bool) -> [a] -> [[a]]
- classify :: Eq a => [a] -> [[a]]
- conditionStatsT :: Listable a => Int -> [(String, a -> Bool)] -> IO ()
- conditionStats :: Listable a => Int -> [(String, a -> Bool)] -> IO ()
- classStatsT :: (Listable a, Show b) => Int -> (a -> b) -> IO ()
- classStats :: (Listable a, Show b) => Int -> (a -> b) -> IO ()
- module Data.Typeable
Documentation
speculate :: Args -> IO () Source #
Calls Speculate. See the example above (at the top of the file).
Its only argument is an Args
structure.
Arguments to Speculate
Args | |
|
The constants list
An encoded Haskell functional-application expression for use by Speculate.
constant :: Typeable a => String -> a -> Expr Source #
Encode a constant Haskell expression for use by Speculate.
It takes a string representation of a value and a value, returning an
Expr
. Examples:
constant "0" 0 constant "'a'" 'a' constant "True" True constant "id" (id :: Int -> Int) constant "(+)" ((+) :: Int -> Int -> Int) constant "sort" (sort :: [Bool] -> [Bool])
hole :: (Listable a, Typeable a) => a -> Expr Source #
(intended for advanced users)
hole (undefined :: Ty)
returns a hole of type Ty
By convention, a Hole is a variable named with the empty string.
foreground :: Expr Source #
A special Expr
value.
When provided on the constants
list,
makes all the following constants foreground
constants.
background :: Expr Source #
A special Expr
value.
When provided on the constants
list,
makes all the following constants background
constants.
Background constants can appear in laws about other constants, but not by
themselves.
The instances list
Misc.
module Test.LeanCheck
(>-) :: a -> b -> a -> b infixr 9 #
Returns an undefined functional value that takes an argument of the type of its first argument and return a value of the type of its second argument.
ty >- ty = (undefined :: Ty -> Ty)
Examples:
'a' >- 'b' = char >- char = (undefined :: Char -> Char) int >- bool >- int = undefined :: Int -> Bool -> Int
(->>>>>>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m) -> m -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m infixl 1 #
(->>>>>>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m) -> m -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l -> m infixl 1 #
(->>>>>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l) -> l -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l infixl 1 #
(->>>>>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l) -> k -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k -> l infixl 1 #
(->>>>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k) -> k -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k infixl 1 #
(->>>>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k) -> j -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j -> k infixl 1 #
(->>>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> j -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j infixl 1 #
(->>>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i -> j) -> i -> a -> b -> c -> d -> e -> f -> g -> h -> i -> j infixl 1 #
(->>>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h -> i) -> i -> a -> b -> c -> d -> e -> f -> g -> h -> i infixl 1 #
(->>>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h -> i) -> h -> a -> b -> c -> d -> e -> f -> g -> h -> i infixl 1 #
(->>>>>>>:) :: (a -> b -> c -> d -> e -> f -> g -> h) -> h -> a -> b -> c -> d -> e -> f -> g -> h infixl 1 #
(->>>>>>:>) :: (a -> b -> c -> d -> e -> f -> g -> h) -> g -> a -> b -> c -> d -> e -> f -> g -> h infixl 1 #
(->>>>>>:) :: (a -> b -> c -> d -> e -> f -> g) -> g -> a -> b -> c -> d -> e -> f -> g infixl 1 #
(->>>>>:>) :: (a -> b -> c -> d -> e -> f -> g) -> f -> a -> b -> c -> d -> e -> f -> g infixl 1 #
(->>>:) :: (a -> b -> c -> d) -> d -> a -> b -> c -> d infixl 1 #
Type restricted version of const that forces the result of the result of the result of its first argument to have the same type as the second.
(->>:>) :: (a -> b -> c -> d) -> c -> a -> b -> c -> d infixl 1 #
Type restricted version of const that forces the third argument of its first argument to have the same type as the second.
(->>:) :: (a -> b -> c) -> c -> a -> b -> c infixl 1 #
Type restricted version of const that forces the result of the result of its first argument to have the same type as the second.
f ->>: ty = f -: und -> und -> ty = f :: a -> b -> Ty
(->:>) :: (a -> b -> c) -> b -> a -> b -> c infixl 1 #
Type restricted version of const that forces the second argument of its first argument to have the same type as the second.
f ->:> ty = f -: und -> ty -> und = f :: a -> Ty -> b
(->:) :: (a -> b) -> b -> a -> b infixl 1 #
Type restricted version of const that forces the result of its first argument to have the same type as the second.
f ->: ty = f -: und >- ty = f :: a -> Ty
(-:>) :: (a -> b) -> a -> a -> b infixl 1 #
Type restricted version of const that forces the argument of its first argument to have the same type as the second:
f -:> ty = f -: ty >- und = f :: Ty -> a
Example:
abs -:> int = abs -: int >- und = abs :: Int -> Int
(-:) :: a -> a -> a infixl 1 #
Type restricted version of const
that forces its first argument
to have the same type as the second.
A symnonym to asTypeOf
:
value -: ty = value :: Ty
Examples:
10 -: int = 10 :: Int undefined -: 'a' >- 'b' = undefined :: Char -> Char
Single-bit signed integers: -1, 0
Two-bit signed integers: -2, -1, 0, 1
Three-bit signed integers: -4, -3, -2, -1, 0, 1, 2, 3
Four-bit signed integers: -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7
Single-bit unsigned integer: 0, 1
Two-bit unsigned integers: 0, 1, 2, 3
Three-bit unsigned integers: 0, 1, 2, 3, 4, 5, 6, 7
Four-bit unsigned integers: 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15
Natural numbers (including 0): 0, 1, 2, 3, 4, 5, 6, 7, ...
Internally, this type is represented as an Int
.
So, it is limited by the maxBound
of Int
.
Natural numbers modulo 1: 0
Natural numbers modulo 2: 0, 1
Natural numbers modulo 3: 0, 1, 2
Natural numbers modulo 4: 0, 1, 2, 3
Natural numbers modulo 5: 0, 1, 2, 3, 4
Natural numbers modulo 6: 0, 1, 2, 3, 4, 5
Natural numbers modulo 7: 0, 1, 2, 3, 4, 5, 6
NoDup [a] |
Bag [a] |
Set [a] |
Map [(a, b)] |
X
type to be wrapped around integer types for an e-X
-treme integer
enumeration. See the Listable
instance for X
. Use X
when
testing properties about overflows and the like:
> check $ \x -> x + 1 > (x :: Int) +++ OK, passed 200 tests.
> check $ \(X x) -> x + 1 > (x :: Int) +++ Failed! Falsifiable (after 4 tests): 9223372036854775807
(=|) :: Eq a => [a] -> Int -> [a] -> Bool infixl 4 #
Check if two lists are equal for n
values.
This operator has the same fixity of ==
.
xs =| n |= ys = take n xs == take n ys
[1,2,3,4,5] =| 2 |= [1,2,4,8,16] -- > True [1,2,3,4,5] =| 3 |= [1,2,4,8,16] -- > False
(=$) :: Eq b => a -> (a -> b) -> a -> Bool infixl 4 #
Equal under, a ternary operator with the same fixity as ==
.
x =$ f $= y = f x = f y
[1,2,3,4,5] =$ take 2 $= [1,2,4,8,16] -- > True [1,2,3,4,5] =$ take 3 $= [1,2,4,8,16] -- > False [1,2,3] =$ sort $= [3,2,1] -- > True 42 =$ (`mod` 10) $= 16842 -- > True 42 =$ (`mod` 9) $= 16842 -- > False 'a' =$ isLetter $= 'b' -- > True 'a' =$ isLetter $= '1' -- > False
neverIdentity :: Eq a => (a -> a) -> a -> Bool #
Is the given function never an identity? f x /= x
holds n $ neverIdentity not
fails n $ neverIdentity negate -- yes, fails: negate 0 == 0, hah!
Note: this is not the same as not being an identity.
identity :: Eq a => (a -> a) -> a -> Bool #
Is the given function an identity? f x == x
holds n $ identity (+0) holds n $ identity (sort :: [()]) holds n $ identity (not . not)
idempotent :: Eq a => (a -> a) -> a -> Bool #
Is the given function idempotent? f (f x) == x
holds n $ idempotent abs holds n $ idempotent sort
fails n $ idempotent negate
strictTotalOrder :: Eq a => (a -> a -> Bool) -> a -> a -> a -> Bool #
totalOrder :: Eq a => (a -> a -> Bool) -> a -> a -> a -> Bool #
strictPartialOrder :: (a -> a -> Bool) -> a -> a -> a -> Bool #
partialOrder :: Eq a => (a -> a -> Bool) -> a -> a -> a -> Bool #
equivalence :: (a -> a -> Bool) -> a -> a -> a -> Bool #
asymmetric :: (a -> a -> Bool) -> a -> a -> Bool #
Is a given relation asymmetric? Not to be confused with "not symmetric" and "antissymetric".
antisymmetric :: Eq a => (a -> a -> Bool) -> a -> a -> Bool #
Is a given relation antisymmetric? Not to be confused with "not symmetric" and "assymetric".
symmetric :: (a -> a -> Bool) -> a -> a -> Bool #
Is a given relation symmetric?
This is a type-restricted version of commutative
.
irreflexive :: (a -> a -> Bool) -> a -> Bool #
An element is never related to itself.
transitive :: (a -> a -> Bool) -> a -> a -> a -> Bool #
Is a given relation transitive?
symmetric2 :: Eq b => (a -> a -> b) -> (a -> a -> b) -> a -> a -> Bool #
Are two operators flipped versions of each other?
holds n $ (<) `symmetric2` (>) -:> int holds n $ (<=) `symmetric2` (>=) -:> int
fails n $ (<) `symmetric2` (>=) -:> int fails n $ (<=) `symmetric2` (>) -:> int
distributive :: Eq a => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool #
Does the first operator, distributes over the second?
associative :: Eq a => (a -> a -> a) -> a -> a -> a -> Bool #
Is a given operator associative? x + (y + z) = (x + y) + z
commutative :: Eq b => (a -> a -> b) -> a -> a -> Bool #
Is a given operator commutative? x + y = y + x
holds n $ commutative (+)
fails n $ commutative union -- union [] [0,0] = [0]
classifyOn :: Eq b => (a -> b) -> [a] -> [[a]] #
classifyBy :: (a -> a -> Bool) -> [a] -> [[a]] #
module Data.Typeable