Obtain the Juvix compiler at https://github.com/anoma/juvix
Here's an example module that defines and tests a property.
module Example;
import Stdlib.Prelude open;
import Stdlib.Data.Nat.Ord open;
import Test.QuickCheckTest as QC;
propReverseReverseIsIdentity (xs : List Int) : Bool :=
Eq.eq xs (reverse (reverse xs));
reverseTest : QC.Test :=
QC.mkTest
"reverse of reverse is identity"
propReverseReverseIsIdentity;
main : IO :=
readLn
\ {seed :=
QC.runTestsIO 100 (stringToNat seed) [reverseTest]};
To run this you need to pass a random seed to the runner:
$ juvix compile Example.juvix
$ od -An -N2 -t u2 /dev/urandom | xargs | ./Example
'reverse of reverse is identity': success
All tests passed
For a larger example see Example.juvix and you can run this using:
make run-quickcheck