Basic Usage

At its core, property based testing (PBT) is about having a function (or set of functions) to test and a set of properties that should hold on that function. If you're already familiar with PBT, this basic example will be familiar to you already.

Consider this add function, which simply forwards to +:

function add(a,b)
    a + b
end

add (generic function with 1 method)

How can we test that this function truly is the same as +? First, we have to decide what input we want to test with. In Supposition.jl, this is done through the use of Possibilitiy objects, which represent an entire set of objects of a shared type. In other frameworks like Hypothesis, this is known as a strategy. In our case, we are mostly interested in integers, so the generator Data.Integers{UInt} is what we're going to use:

using Supposition, Supposition.Data

intgen = Data.Integers{UInt}()

Supposition.Data.Integers{UInt64, UInt64}(0x0000000000000000, 0xffffffffffffffff)

Now that we have our input generator, we have to decide on the properties we want to enforce. Here, we simply want to check the mathematical properties of addition, so let's start with commutativity:

Supposition.@check function commutative(a=intgen, b=intgen)
    add(a,b) == add(b,a)
end

Test Summary: | Pass  Total  Time
commutative   |    1      1  0.1s

@check takes a function definition where each argument is given a Possibility, runs those generators, feeds the generated values into the given function and shrinks any failing examples. Note that the name given in the arguments is the same as used in the function.

Here's an example for a failing property:

Supposition.@check function failprop(x=intgen)
    add(x, one(x)) < x
end

┌ Error: Property doesn't hold!
│   Description = "failprop"
│   Example = (x = 0x0000000000000000,)
└ @ Supposition ~/work/Supposition.jl/Supposition.jl/src/testset.jl:292
Test Summary: | Fail  Total  Time
failprop      |    1      1  0.1s

Supposition.jl successfully found a counterexample and reduced it to a more minimal counterexample, in this case just UInt(0).

We've still got three more properties to test, taking two or three arguments each. Since these properties are fairly universal, we can also write them out like so, passing a function of interest:

associative(f, a, b, c) = f(f(a,b), c) == f(a, f(b,c))
identity_add(f, a) = f(a,zero(a)) == a
function successor(a, b)
    a,b = minmax(a,b)
    sumres = a
    for _ in one(b):b
        sumres = add(sumres, one(b))
    end

    sumres == add(a, b)
end

successor (generic function with 1 method)

And check that they hold like so. Of course, we can also test the property implicitly defined by @check earlier:

using Test

Supposition.@check associative(Data.Just(add), intgen, intgen, intgen)
Supposition.@check identity_add(Data.Just(add), intgen)
Supposition.@check successor(intgen, intgen)
Supposition.@check commutative(intgen, intgen)

Test Summary: | Pass  Total  Time
associative   |    1      1  0.0s
Test Summary: | Pass  Total  Time
identity_add  |    1      1  0.0s
Test Summary: | Pass  Total  Time
successor     |    1      1  0.0s
Test Summary: | Pass  Total  Time
commutative   |    1      1  0.0s

In this way, we can even reuse properties from other invocations of @check with new, perhaps more specialized, inputs. For generalization, we can use Data.Just to pass our add function to the generalized properties.

Be aware that while all checks pass, we do not have a guarantee that our code is correct for all cases. Sampling elements to test is a statistical process and as such we can only gain confidence that our code is correct. You may view this in the light of Bayesian statistics, where we update our prior that the code is correct as we run our testsuite more often. This is also true were we not using property based testing or Supposition.jl at all - with traditional testing approaches, only the values we've actually run the code with can be said to be tested.