Target is a library for testing Haskell functions based on
properties encoded as refinement types.
The programmer specifies the expected behavior of a
function with a refinement type, and Target then checks
that the function satisfies the specification by
enumerating valid inputs up to some size, calling the
function, and validating the output. Target excels when the
space of valid inputs is a sparse subset of all possible
inputs, e.g. when dealing with dataypes with complex
invariants like red-black trees.
Test.Target
is the main entry point and should contain
everything you need to use Target with types from the
Prelude
. Test.Target.Targetable
will also be useful if
you want to test functions that use other types.
For information on how to specify interesting properties
with refinement types, we have a series of
blog posts
as well as an
evolving tutorial.
Target uses the same specification language as LiquidHaskell,
so the examples should carry over.
Finally, Target requires either Z3
(>=4.3
) or CVC4 (>=1.4
) to
be present in your PATH
.