Sign in

    quickcheck

    Automatic testing of MoonBit programs

    property-based-testing
    quickcheck
    Download zip
    Version
    0.13.0
    License
    Apache-2.0
    Last updated
    6 months ago
    Downloads
    193K

    No dependencies

    #MoonBit QuickCheck

    #Introduction

    The idea of QuickCheck was originally introduced in John's paper QuickCheck: a lightweight tool for random testing of Haskell programs and its Haskell derivation QuickCheck, which aimed at simplifying the writing of tests by generating them. The core is to automatically generate tests based on a the signature of the specification / theorem (i.e. properties which functions should satisfy) and QuickCheck then tests that the properties hold. The idea spread to other languages and is now implemented in MoonBit. Because of the differences in type systems between Haskell and MoonBit, the original idea morphed into something different. There are several differences to this approach:

    • We have discarded many ideas in Haskell QuickCheck that have been proven inappropriate by time.
    • Some features requiring a very fancy type system were removed (or not considered currently). For instance, the generation of functions requires GADTs, which MoonBit does not support.
    • MoonBit QuickCheck brings many modern academic ideas into industrial practice (listed below).


    #Table of Contents

    #Quick Start

    #Installation

    Firstly, you need to install the MoonBit QuickCheck library. You can do this by executing the following command:

    moon add moonbitlang/quickcheck moon install

    To use the library, import the root package as qc and the generator subpackage as gen in your moon.pkg.json file:

    import { "moonbitlang/quickcheck" @qc "moonbitlang/quickcheck/gen" @gen } import { "moonbitlang/quickcheck" } for "test" // for test

    #First Look

    Let's start with something very simple. Suppose that we just wrote a function rev which takes an array as argument and returns its reverse. We want to test its functionality by writing unit tests:

    ///|
    test "reverse" {
    inspect(([] : Array[Int]).rev(), content="[]")
    inspect([1, 2, 3].rev(), content="[3, 2, 1]")
    }

    Is this enough to prove that this function is correct? No, the bugs may lie in the remaining untested code. But if we want more rigorous verification, we may need to write more test cases. For a complicated program, there would never be time to do so. How can we reduce the cost of testing? The key to doing so must be to generalize the test functions, so that each function covers not only one test case, but many. This is where QuickCheck comes in. We can write a property of reverse that should hold for any array, and QuickCheck will generate a large number of random array and check that the property holds for all of them.

    But what property should we write? We may notice that the reverse of the reverse of an array is the original array. So we can write a property (you can roughly think of it as a function (T) -> Bool) that reverse should have for any array:

    ///|
    fn prop_reverse_identity(arr : Array[Int]) -> Bool {
    arr.rev().rev() == arr
    }

    We may consider the code logically as:

    Looks good, now we can use QuickCheck to test this property, this is easily archived by the quick_check_fn function:

    ///|
    test {
    @qc.quick_check_fn(prop_reverse_identity)
    // equivalent to
    // @qc.quick_check(@qc.Arrow(prop_reverse_identity))

    }

    The quick_check_fn function takes a f: (T) -> Bool, where T satisfies some constraints (We will discuss this later), the function first generates a bunch of random values with type T and then calling the property function f with these values. The results are then collected and will be reported later. In this example, the input value T = Array[Int] and the boolean value true imply that the property holds for some particular values, and the false implies that the property does not hold for some values. When finding a counterexample, QuickCheck will try to simplify it and then print it to the console. If all the tests passed, the following sentence will be printed to the console:

    +++ [100/0/100] Ok, passed!

    The three number in the brackets are the number of passed, discarded and total tests (the default value of total tests is 100).

    #Failure Diagnosis

    Now let's see another example: suppose we want to write a function remove(arr : Array[Int], x : Int) -> Array[Int] that takes an array and an element and returns a new array with all occurrences of x removed. The intuitive implementation is to search for x in the array and remove it if found:

    ///|
    fn remove(arr : Array[Int], x : Int) -> Array[Int] {
    match arr.search(x) {
    Some(i) => arr.remove(i) |> ignore
    None => ()
    }
    arr
    }

    Now let's use QuickCheck to test this function. The first thing we need to do is to write a property. We may consider the following properties:

    • If an element was removed from the array, the length of the array should be less than or equal to the original array

    • If an element was removed from the array, the element should not exist in the array anymore

    Now we translate the first property into a MoonBit function (Note that the property function should have exactly one argument, but we can use a tuple to pass multiple arguments):

    ///|
    fn prop_length_is_not_greater(iarr : (Int, Array[Int])) -> Bool {
    let (x, arr) = iarr
    let len = arr.length()
    remove(arr, x).length() <= len
    }

    Run QuickCheck, all tests passed. However, this property is not considered a good property because it can be fulfilled easily and hence the test is not very meaningful. Bugs may still exist in the function.

    ///|
    test {
    @qc.quick_check_fn(prop_length_is_not_greater)
    }

    // +++ [100/0/100] Ok, passed!

    The later property is considered better, similarly we implement it in MoonBit:

    ///|
    fn prop_removed_not_present(iarr : (Int, Array[Int])) -> Bool {
    let (x, arr) = iarr
    !remove(arr, x).contains(x)
    }

    ///|
    test {
    @qc.quick_check_fn(prop_removed_not_present, expect=Fail)
    }

    The QuickCheck test reports a failure with a counterexample in the second line after 8 tests:

    *** [8/0/100] Failed! Falsified. (0, [0, 0])

    When x = 0 and arr = [0, 0] the property does not hold. The remove function should remove all occurrences of x in the array, but it only removes the first one. QuickCheck finds us a succinct counterexample that directly reveals the core of the problem. How does it do this? In practice QuickCheck generates a lot of complex samples and inputs them into the property function to test them, and if it finds a counterexample it doesn't report it immediately, but shrinks accordingly to try to find a simpler counterexample. In this example, as in many cases, the randomly generated test case contains junk values that have nothing to do with the test failure itself. When the counterexample is found, qc will apply some predefined shrinkers to this counterexample and try to explore downwards for smaller counterexamples.

    #Traits

    We've already discussed generation and shrinking, and this section will discuss how these functions are attached to a type. Recall the quick_check_fn function we used before. It is defined as follows in the MoonBit QuickCheck library:

    ///|
    /// path: src/driver.mbt
    pub fn[A : @coreqc.Arbitrary + Shrink + Show, B : Testable] quick_check_fn(
    f : (A) -> B,
    max_shrinks? : Int,
    max_success? : Int,
    max_size? : Int,
    discard_ratio? : Int,
    expect? : Expected = Success,
    abort? : Bool = false,
    ) -> Unit raise Failure {
    quick_check(
    Arrow(f),
    max_shrink?=max_shrinks,
    max_success?,
    max_size?,
    discard_ratio?,
    expect~,
    abort~,
    )
    }

    Let's look at the type signature first. The quick_check_fn function takes a function f: (A) -> B as argument, where A should have implemented the Arbitrary, Shrink and Show traits, and B should have implemented the Testable trait. In our examples B is fixed to a Bool, this is because Booleans implement the Testable trait, which can actually be more flexible, we will discuss this later, for now we focus on the constraints of A:

    • Arbitrary is a trait that generates random values of a type.
    • Shrink is a trait that allows a value of particular type to be shrunk to simpler ones.
    • Show is used for printing the counterexample when a test fails.

    Now let's look at the function body. It takes a value of type that implemented Testable as argument and runs the test. This is an effectful function that may throw an error to the MoonBit test driver when a test fails (or give up). On success, it simply returns Unit with the sentence Ok, passed! printed to the console.

    The body of the function contains a call to quick_check and wraps f in Arrow. According to the definition of quick_check, it requires a value prop of a type P that implements Testable as an argument, and under certain conditions: For any type P implementing Testable, and A implementing Arbitrary, Shrink and Show, the Arrow[A, P] type can be implemented as Testable as well. The reader may wonder why we don't directly implement (A) -> P as Testable but instead use Arrow[A, P] as a wrapper. The reason is simple: The MoonBit type system does not allow us to do so.

    pub fn quick_check[P : @qc.Testable](prop : P) -> Unit raise Failure

    pub(all) struct Arrow[A, P]((A) -> P)

    pub impl[P : Testable, A : Arbitrary + Shrink + Show] Testable for Arrow[A, P]

    #Testable

    Another advantage of using Arrow is that it constructs a Testable, and QuickCheck provides a number of Testable combinators that can be used to modify a test's properties, such as with_max_success to modify the maximum number of successes:

    ///|
    fn prop_remove_not_presence(iarr : (Int, Array[Int])) -> Bool {
    let (x, arr) = iarr
    !remove(arr, x).contains(x)
    }

    ///|
    test {
    @qc.quick_check(
    @qc.Arrow(prop_remove_not_presence),
    max_shrink=1000,
    expect=Fail,
    )
    }

    There are many other combinators that can be used to modify the properties of a test, check the document for src/testable.mbt for more details.

    #Arbitrary

    Arbitrary is a trait indicating that a type has the ability to generate random values for given size and random number generator, which is defined in the MoonBit Core library with compiler level support. It has a method arbitrary that takes a size and a random number generator and then returns a random value of the type.

    ///|
    pub trait Arbitrary {
    arbitrary(Int, @splitmix.RandomState) -> Self
    }

    The vast majority of types in the core library already implement the Arbitrary trait, and users can also write specific instance for their own defined types or use the compiler's automatic derivation. For example, we can derive the Arbitrary trait for our own Nat type:

    ///|
    enum Nat {
    Zero
    Succ(Nat)
    } derive(Arbitrary)

    ///|
    impl Show for Nat with output(self, logger) {
    match self {
    Zero => logger.write_string("Zero")
    Succ(n) => {
    logger.write_string("Succ(")
    n.output(logger)
    logger.write_string(")")
    }
    }
    }

    ///|
    test {
    let nat_gen : @gen.Gen[Nat] = @gen.Gen::spawn()
    let nats = nat_gen.samples(size=4)
    inspect(
    nats,
    content="[Succ(Succ(Succ(Zero))), Succ(Succ(Succ(Succ(Zero)))), Succ(Zero), Succ(Succ(Succ(Zero)))]",
    )
    }

    For any type that implements Arbitrary, you can use the Gen::spawn function to get its generator. Calling the generator's method samples will generate some values of that type. Note that Gen is an internal type of QuickCheck, which will be automatically called by the quick_check function, but normally the user is not required to access it. Here we use it to show the behavior of Arbitrary.

    #Shrink

    Shrink is a trait that shrinks a value to a simpler one. It has a method shrink that takes a value and returns an Iter of simpler values (lazily).

    ///|
    pub trait Shrink {
    shrink(Self) -> Iter[Self]
    }

    If QuickCheck finds a set of values that fails a given property, it will try to make that value simpler than the original value by getting the shrunken versions of the value and trying each one in turn to check that the property is still false. If it is, the smaller value becomes the new counterexample and the shrinking process continues with that value.

    #Advanced Topics

    #QuickCheck Invalid Cases

    This section summarizes some common mistakes in using QuickCheck:

    • Testing with external effects: If a property requires an external state, for example, the user's input, the global mutable and etc, you should pass the state as an argument to the property function. Otherwise, the property is not a pure function and the test is not repeatable.
    • Mutable argument was unexpectedly modified: You should keep the arguments immutable in the property function. If you need to modify the arguments, you should make a copy of them.

    #Generators

    Test data is produced by test data generators. QuickCheck defines default generators for some often used types, but you can roll your own, and will need to define your own generators for any new types you introduce (Or for simple types we can use the trivial definition by derive(Arbitrary)).

    Generators have types of the form Gen[T], which is a generator for values of type T. It was defined as a struct, it contains a single field named gen, with type (Int, RandomState) -> T (The first parameter is the size of the generated value, and the second is the random number generator), notice that this is similar to the arbitrary method in the Arbitrary trait:

    ///|
    struct Gen[T] {
    gen : (Int, @splitmix.RandomState) -> T
    }

    QuickCheck defines a series of useful methods for Gen[T], for the most basic ones, we can use the Gen(f: (Int, RandomState) -> T) constructor to create a generator from a function and run it by invoking the run method:

    ///|
    let g : @gen.Gen[Int] = {
    ...
    } // Suppose we have a generator for Int

    ///|
    let _x : Int = g.run(100, @splitmix.new()) // Generate a random Int at size 100

    Gen[T] was implemented as functor, applicative and monad which means you can compose it in many ways.

    fn pure[T](val : T) -> Gen[T]
    fn fmap[T, U](self : Gen[T], f : (T) -> U) -> Gen[U]
    fn ap[T, U](self : Gen[(T) -> U], v : Gen[T]) -> Gen[U]
    fn bind[T, U](self : Gen[T], f : (T) -> Gen[U]) -> Gen[U]

    For instance, you can use the fmap method to transform the generated value:

    ///|
    let g1 : @gen.Gen[Int] = @gen.Gen(
    {
    ...
    },
    )

    ///|
    let _g2 : @gen.Gen[Int] = g1.fmap(x => x + 1)

    ///|
    let _g3 : @gen.Gen[String] = g1.fmap(x => x.to_string())

    Or create a dependent generator:

    ///|
    let dg1 : @gen.Gen[Int] = @gen.Gen(
    {
    ...
    },
    )

    ///|
    let _dg2 : @gen.Gen[Int] = dg1.bind(x => {
    // TODO(upstream) <| does not work here
    if x == 0 {
    @gen.pure(100)
    } else {
    @gen.pure(200)
    }
    })

    The following documents explains some useful combinators for Gen[T].

    #Choosing Between Alternatives

    A generator may take the form one_of which chooses among the generators in the array with equal probability. For example, this generates a random boolean which is true with probability one half:

    ///|
    let _gen_bool : @gen.Gen[Bool] = @gen.one_of([@gen.pure(true), @gen.pure(false)])

    If you want to control the distribution of results using frequency instead. We have frequency which chooses a generator from the array randomly, but weighs the probability of choosing each alternative by the factor given. For example, this generates true in the probability of .

    ///|
    let _gen_freq : @gen.Gen[Bool] = @gen.frequency([
    (4, @gen.pure(true)),
    (1, @gen.pure(false)),
    ])

    #Size parameter

    We have pointed out that test data generators have an size parameter. QuickCheck begins by generating small test cases, and gradually increases the size as testing progresses. Different test data generators interpret the size parameter in different ways: some ignore it, some interpret it as an upper bound on the size of containers. Most generators defined in the Arbitrary trait depend on the size parameter but most separate generator combinators do not.

    You can obtain the value of the size parameter using sized combinator.

    pub fn sized[T](f : (Int) -> @gen.Gen[T]) -> @gen.Gen[T]

    For example, we can make a trivial generator for a list of integers with a given length:

    ///|
    let gen : @gen.Gen[Int] = @gen.sized(@gen.pure)

    ///|
    let arr : Array[Int] = Array::makei(20, i => gen.sample(size=i))

    ///|
    test "sized" {
    debug_inspect(
    arr,
    content="[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19]",
    )
    }

    The purpose of size control is to ensure that test cases are large enough to reveal errors, while remaining small enough to test fast. Sometimes the default size control does not achieve this. So we have provided some tool functions like resize and scale (check the document for details) for this purpose.

    #Default Generators

    QuickCheck defines default test data generators and shrinkers for some often used types (By trait Arbitrary and Shrink). You do not need to define or apply these explicitly for every property because QuickCheck can provide a property with appropriate generators and shrinkers for the property's arguments. But if you are required to do so, you can use the forall for explicit universal quantification.

    ///|
    using @list {type List}

    ///|
    let prop_rev : (List[Int]) -> Bool = (x : List[Int]) => x.rev().rev() == x

    ///|
    test "List reverse" {
    @qc.quick_check(@qc.forall(@gen.Gen::spawn(), prop_rev))
    }

    Note that the spawn function is useful for creating Gen[T] from its arbitrary instance. In this example the type checker infers the type of the first argument in forall to be Gen[List[T]] from the type of the property function.

    fn Gen::spawn[T : Arbitrary]() -> Gen[T]

    #Custom Generator

    Recall the remove function we wanted to test before. The QuickCheck do report an error for us, but the generator is quite random and the tuple element (x, arr): (Int, Array[Int]) is independent. In most cases, x is not in the array, so the test is not very meaningful (falls to the branch None => ()). Now we use the one_of_array combinator to generate a random element from a generated non-empty array, which makes the test more meaningful.

    ///|
    test {
    @qc.quick_check(
    @qc.forall(@gen.Gen::spawn(), (a : Array[Int]) => {
    @qc.filter(
    @qc.forall(@gen.one_of_array(a), y => !remove(a, y).contains(y)),
    a.length() != 0,
    )
    }),
    expect=Fail,
    // We expect this test to fail because of the bug in the remove function
    )
    }

    We admit the following facts:

    • The first spawn evaluates to a generator of Array[Int].
    • The forall function can be nested.
    • There is a filter function that filters out the test cases that do not satisfy the condition. A non-empty array is required in this case.
    • The one_of_array function selects a random element from a non-empty array.

    *** [4/33/100] Failed! Falsified. [0, 0] 0

    We find that there are 33 cases that do not satisfy the condition, and the counterexample is [0, 0] and 0, which points out the issue clearly. The one_of_array function selects a random element from the array, so the y is always 0 in this case. The remove function only removes the first one, so the property does not hold.

    #Conditional Properties

    Now let's further verify our hypothesis: The function remove only removes the first one but not all. So if we instead formulate a conditional property which restricts the input array to contain no duplicated elements, then our tests should pass. Using the function filter can filter out unwanted test cases:

    ///|
    test {
    fn no_duplicate(x : Array[Int]) -> Bool {
    @sorted_set.from_iter(x.iter()).length() == x.length()
    }

    @qc.quick_check(
    @qc.forall(@gen.Gen::spawn(), (iarr : (Int, Array[Int])) => {
    let (x, arr) = iarr
    @qc.filter(!remove(arr.copy(), x).contains(x), no_duplicate(arr))
    }),
    max_size=50,
    discard_ratio=20,
    max_success=100,
    )
    }

    • Notice that we use arr.copy() to make a copy of the array, because the remove function may modify the argument array.
    • The no_duplicate function checks whether the input array contains no duplicated elements.
    • As discussed above, the filter combinator filters out the test cases that do not satisfy the condition.

    Running this test, we find that all tests passed. Now we have strong evidence that the remove function only removes the first one but not all.

    #Classifying Data

    We may also be interested in the distribution of the generated data: sometimes the generator may produce trivial data that does not help us to find the bugs. We want to find out what data is generated and how often in order to improve the generator. QuickCheck provides functions like label, collect and classify to achieve this.

    ///|
    test "classes" {
    @qc.quick_check_fn((x : List[Int]) => {
    prop_rev(x)
    |> @qc.classify(x.length() > 5, "long list")
    |> @qc.classify(x.length() <= 5, "short list")
    })
    }

    One caution: @qc.Arrow(...) always introduces a fresh generated sample. So inside a property that already bound x, writing @qc.Arrow(prop_rev) would quantify a second list instead of reusing x. In that case the labels would describe x, but the property would run on a different value. When you want to classify the current sample, call the property directly on x and then pipe into classify or label.

    The classify function takes a boolean and a string, and if the boolean is true, the test case is classified with the string.

    +++ [100/0/100] Ok, passed! 22% : short list 78% : long list

    The label function takes a string and classifies the test case with the string.

    ///|
    test "label" {
    @qc.quick_check_fn((x : List[Int]) => {
    prop_rev(x)
    |> @qc.label(if x.is_empty() { "trivial" } else { "non-trivial" })
    })
    }

    The result is as follows:

    +++ [100/0/100] Ok, passed! 8% : trivial 92% : non-trivial

    The collect function is a generalization of label. The difference is that the collect takes an argument implementing the Show trait, and the label takes a string directly. The collect function is useful when you want to classify the test case with a complex value.

    #Application

    We have applied MoonBit QuickCheck to test the correctness of the MoonBit core. For now we have found several bugs in the core, including:

    #Roadmap and Future Work

    #Data Generation

    • Currently use the SplitMix algorithms

    #Property Verification

    #Shrinking

    #References

    Shrink

    pub(open) trait Shrink {
    shrink(Self) -> Iter[Self] = _
    }

    Types that can enumerate "smaller" variants of a given value for the classical QuickCheck shrinker. Each call to shrink(x) returns an Iter[Self] of candidates strictly simpler than x; the driver walks these candidates after a failure, keeping the first one that still falsifies the property.

    The return type is Iter[Self] rather than Array[Self] so large or recursive shrink spaces stay lazy. The default body (= _) means "no shrinks" — a conservative starting point for types where shrinking isn't meaningful.

    test {
    // `Int` has a built-in Shrink instance that walks toward 0.
    let candidates : Array[Int] = Shrink::shrink(100).collect()
    assert_true(candidates.contains(0))
    assert_true(candidates.length() > 0)
    // `Bool` shrinks `true` to `false`, and `false` has no shrinks.
    assert_eq(Shrink::shrink(true).collect(), [false])
    assert_eq(Shrink::shrink(false).collect(), [])
    }
    impl Shrink for Unit
    impl Shrink for Bool
    impl Shrink for Char
    impl Shrink for Int
    impl Shrink for Int64
    impl Shrink for UInt
    impl Shrink for UInt64
    impl Shrink for Float
    impl Shrink for Double
    impl Shrink for String
    impl Shrink for Option[T]
    impl Shrink for Result[T, E]
    impl Shrink for Bytes
    impl Shrink for Array[X]
    impl Shrink for Iter[X]
    impl Shrink for Tuple2[A, B]
    impl Shrink for Tuple3[A, B, C]
    impl Shrink for Tuple4[A, B, C, D]
    impl Shrink for Tuple5[A, B, C, D, E]
    impl Shrink for Tuple6[A, B, C, D, E, F]

    Testable

    pub(open) trait Testable {
    property(Self) -> Property
    }

    Anything that can be handed to the quick_check driver.

    Implementors turn themselves into a Property — a Gen of a Rose of per-run outcomes — which the driver then evaluates. Built-in instances exist for Bool (treated as pass/fail) and for Arrow[A, P] / ArrowError[A, P] when A : Arbitrary + Shrink + Show and P : Testable.

    The ArrowAsync[A, P] newtype exists but no Testable impl is provided yet — async property testing is planned but not wired up.
    impl Testable for Unit
    impl Testable for Bool
    impl Testable for Option[P]
    impl Testable for Result[P, E]
    impl Testable for Gen[P]

    Arrow

    pub(all) struct Arrow[A, B]((A) -> B)

    Arrow[A, B] is a newtype wrapper around a pure, total function (A) -> B. Wrapping is what lets us write

    pub impl[P : Testable, A : Arbitrary + Shrink + Show] Testable for Arrow[A, P]

    — MoonBit does not let us implement a trait directly on the bare function type (A) -> B, so Arrow is the obligatory detour.

    For the user this shows up as @qc.Arrow(prop) at the driver boundary:

    @qc.quick_check(@qc.Arrow((x : Int) => x == x))

    Most users never see Arrow directly because quick_check_fn wraps the function for them. Reach for the explicit form only when you need to hand a Testable-wrapped property to a combinator that takes Testable values (e.g. classify, label).

    See also: ArrowError (for properties that may raise) and ArrowAsync (for properties that are async).

    ArrowAsync

    pub(all) struct ArrowAsync[A, B](async (A) -> B)

    Same role as Arrow, but the wrapped function is async. The async driver in the main package (see driver.mbt) awaits the inner coroutine and threads it through the same shrink loop as the synchronous path.

    ArrowError

    pub(all) struct ArrowError[A, B]((A) -> B raise)

    Same role as Arrow, but the wrapped function may raise an error. Use this when your property calls into code that throws and you want the driver to treat a raised exception as a test failure with the captured error as the counterexample's reason.

    Under the hood it's identical to Arrow plus a raise clause.
    impl Testable for ArrowError[A, P]

    Callback

    type Callback

    TODO: determine the execution of callback by kind

    Discard

    type Discard derive(Default)

    impl Testable for Discard

    Expected

    pub(all) enum Expected {
    Fail
    Success
    GaveUp
    }

    What the author of a property expects to happen. This is the knob behind quick_check_fn(..., expect=Fail) and friends: if the driver's actual verdict matches Expected, the check is considered a pass even when the property raises.

    Use cases:

    • Success (the default) — property must hold on every generated input.
    • Fail — the property should fail; useful when you want to demonstrate a known bug or lock in a regression check. The test fails if the driver can't find a counterexample.
    • GaveUp — the property is expected to discard too many cases. Rarely useful in isolation; handy for testing the driver itself.

    Property

    type Property

    Replay

    pub(all) struct Replay {
    rand_state :
    RandomState

    size : Int
    }

    A snapshot of the RNG state and size parameter sufficient to rerun a property on the exact same input sequence.

    Every failing report in the driver carries a Replay inside its counterexample record — copy it into a test, pass it back via the driver's replay hook, and you will deterministically reproduce the failure on any machine. This is how the project's test suite pins previously-found counterexamples.

    Fields:
    • rand_state: SplitMix seed captured just before the offending sample was drawn.
    • size: the size parameter the property was running at (the same value threaded through @gen.sized / @gen.Gen::scale).

    Constructor: Replay::new(rand_state, size) (see result.mbt).

    Replay::new

    Capture the current RNG state and size parameter as a Replay so that a failing test can be rerun deterministically. Typically used inside the driver — the Replay record also surfaces in the counter-example reported by a failing check.

    callback

    fn[P : Testable] callback(p : P, cb : Callback) -> Property

    Attach a post-test (or post-final-failure) callback to p. The callback receives the driver state and result; typical use is to print diagnostics on a shrunk counter-example.

    classify

    fn[P : Testable] classify(p : P, cond : Bool, s : String) -> Property

    Classifies a test case based on a condition

    collect

    fn[P : Testable, T : Show] collect(p : P, t : T) -> Property

    Attaches a label (Show) to a test case

    counterexample

    fn[P : Testable] counterexample(p : P, s : String) -> Property

    Adds a string to the counterexample if the property fails

    filter

    fn[P : Testable] filter(p : P, cond : Bool) -> Property

    Filters a property based on a condition

    forall

    fn[T : Testable, A : Show] forall(gen :
    Gen
    [A], f : (A) -> T) -> Property

    Run with an explicit generator

    forall_shrink

    fn[T : Testable, A : Show] forall_shrink(gen :
    Gen
    [A], shrinker : (A) -> Iter[A], f : (A) -> T) -> Property

    Run a property with an explicit generator and shrinker. forall is a convenience that passes _ => Iter::empty() — use this version when you want a hand-rolled shrinker without going through the Shrink trait.

    if_fail

    fn[P : Testable] if_fail(p : P, f : () -> Unit) -> Property

    Adds a callback that will be called if the property fails

    label

    fn[P : Testable] label(p : P, s : String) -> Property

    Attaches a label to a test case

    map_size

    fn[P : Testable] map_size(p : P, f : (Int) -> Int) -> Property

    Adjust the size parameter before running p. Equivalent to Gen::scale(f) but lifted to the Testable level.

    quick_check

    fn[P : Testable] quick_check(prop : P, max_shrink? : Int, max_success? : Int, max_size? : Int, discard_ratio? : Int, expect? : Expected, abort? : Bool, verbose? : Bool) -> Unit raise Failure

    Run a Testable property against randomly-generated inputs and print the outcome. The driver runs up to max_success successful tests, trying increasingly large inputs up to max_size, and discarding no more than max_success × discard_ratio inputs before giving up. On failure it shrinks for up to max_shrink steps before reporting.

    expect asserts the expected outcome (Success by default); the driver flips the verdict accordingly (a failing property with expect=Fail is a pass). abort=true short-circuits the outer loop after the first test result is processed — note that a failing result still goes through the full shrink search before returning.

    Raises Failure on mismatch with expect — so it's the drop-in entry point inside test "…" blocks.

    quick_check_fn

    fn[A :
    Arbitrary
    + Shrink + Show, B : Testable] quick_check_fn(f : (A) -> B, max_shrinks? : Int, max_success? : Int, max_size? : Int, discard_ratio? : Int, expect? : Expected, abort? : Bool, verbose? : Bool) -> Unit raise Failure

    Thin sugar over quick_check: accept a plain (A) -> B property function, wrap it in Arrow, and run. The shortest path from a user-written property to a full QuickCheck run.

    quick_check_fn_error

    fn[A :
    Arbitrary
    + Shrink + Show, B : Testable] quick_check_fn_error(f : (A) -> B raise, max_shrinks? : Int, max_success? : Int, max_size? : Int, discard_ratio? : Int, expect? : Expected, abort? : Bool, verbose? : Bool) -> Unit raise Failure

    quick_check_fn for properties that may raise. A raised error is treated as a counter-example with the error captured as the reason.

    quick_check_fn_error_silence

    fn[A :
    Arbitrary
    + Shrink + Show, B : Testable] quick_check_fn_error_silence(f : (A) -> B raise, max_shrinks? : Int, max_success? : Int, max_size? : Int, discard_ratio? : Int, expect? : Expected, abort? : Bool, verbose? : Bool) -> String

    quick_check_fn_error silent variant that returns the formatted outcome as a String.

    quick_check_fn_silence

    fn[A :
    Arbitrary
    + Shrink + Show, B : Testable] quick_check_fn_silence(f : (A) -> B, max_shrinks? : Int, max_success? : Int, max_size? : Int, discard_ratio? : Int, expect? : Expected, abort? : Bool, verbose? : Bool) -> String

    quick_check_fn variant that returns the formatted outcome as a String instead of raising / printing.

    quick_check_silence

    fn[P : Testable] quick_check_silence(prop : P, max_shrink? : Int, max_success? : Int, max_size? : Int, discard_ratio? : Int, expect? : Expected, abort? : Bool, verbose? : Bool) -> String

    Like quick_check but returns the formatted outcome as a String instead of printing it or raising. Useful in tests that want to pin the driver's output with inspect(..., content=...).

    shrink_distinct_array

    fn[X : Shrink + Eq] shrink_distinct_array(xs : Array[X]) -> Iter[Array[X]]

    Shrink distinct array, requires all elements of the Array[X] to be distinct.

    shrink_non_empty_array

    fn[X : Shrink] shrink_non_empty_array(xs : Array[X]) -> Iter[Array[X]]

    Shrink non-empty array without producing the empty array.

    test {
    assert_true(shrink_non_empty_array([1, 2, 3]).all(ys => ys.length() > 0))
    }

    shrink_non_empty_list

    fn[T : Shrink] shrink_non_empty_list(xs :
    List
    [T]) -> Iter[
    List
    [T]]

    Shrink non-empty list without producing the empty list.

    test {
    let xs : @list.List[Int] = @list.from_array([5])
    // Default list shrink would produce [], which is filtered out here.
    assert_true(shrink_non_empty_list(xs).all(ys => !ys.is_empty()))
    }

    shrink_sorted_array

    fn[T : Shrink + Compare + Eq] shrink_sorted_array(xs : Array[T], lo~ : T, hi~ : T) -> Iter[Array[T]]

    Shrink sorted array, requires the Array[T] to be sorted.

    shrink_sorted_distinct_array

    fn[T : Shrink + Compare + Eq] shrink_sorted_distinct_array(xs : Array[T], lo~ : T, hi~ : T) -> Iter[Array[T]]

    Shrink sorted distinct array, requires the Array[T] to be sorted and distinct.

    shrink_sorted_list

    fn[T : Shrink + Compare + Eq] shrink_sorted_list(xs :
    List
    [T], lo~ : T, hi~ : T) -> Iter[
    List
    [T]]

    Shrink sorted list, requires the List[T] to be sorted.

    shrinking

    fn[P : Testable, T] shrinking(shrinker : (T) -> Iter[T], x0 : T, pf : (T) -> P) -> Property

    Manually drive shrinking: given a user-supplied shrinker and a starting value x0, build a Property whose Rose branches mirror the shrink tree produced by shrinker. Rarely needed in user code — the Shrink trait instances drive this automatically — but useful when a one-off custom shrink sequence is required.

    small_check

    fn[A :
    Enumerable
    + Show, B : Testable] small_check(f : (A) -> B, max_size? : Int, expect? : Expected, abort? : Bool, verbose? : Bool) -> Unit raise Failure

    Exhaustive-ish testing via the feat enumeration: walk values of A in ascending size order, checking each one against f, up to at most max_size total test cases (not all values of size ≤ max_size — that would usually be combinatorially huge). So small_check is "enumerate prefix by size, check the first max_size values"; pick max_size large enough to cover the interesting sizes for your type.

    Complements quick_check: use small_check when you want deterministic, size-indexed coverage rather than random sampling.

    small_check_error

    fn[A :
    Enumerable
    + Show, B : Testable] small_check_error(f : (A) -> B raise, max_size? : Int, expect? : Expected, abort? : Bool, verbose? : Bool) -> Unit raise Failure

    small_check variant that accepts a property that may raise. A raised error is treated as a counter-example.

    small_check_error_silence

    fn[A :
    Enumerable
    + Show, B : Testable] small_check_error_silence(f : (A) -> B raise, max_size? : Int, expect? : Expected, abort? : Bool, verbose? : Bool) -> String

    Silent variant of small_check_error: returns the formatted outcome as a String instead of raising.

    small_check_silence

    fn[A :
    Enumerable
    + Show, B : Testable] small_check_silence(f : (A) -> B, max_size? : Int, expect? : Expected, abort? : Bool, verbose? : Bool) -> String

    small_check silent variant: returns the formatted outcome as a String.