basic.md

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

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}()

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

@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:

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

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

!!! note "Overflow" There is a subtle bug here - if x+1 overflows when x == typemax(UInt), the resulting comparison is true: typemin(UInt) < typemax(UInt) after all. It's important to keep these kinds of subtleties, as well as the invariants the datatype guarantees, in mind when choosing a generator and writing properties to check the datatype and its functions for.

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

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

using Test

show(stdout, MIME"text/plain"(), # hide
Supposition.@check associative(Data.Just(add), intgen, intgen, intgen)
); println(); show(stdout, MIME"text/plain"(), # hide
Supposition.@check identity_add(Data.Just(add), intgen)
); println(); show(stdout, MIME"text/plain"(), # hide
Supposition.@check successor(intgen, intgen)
); println(); show(stdout, MIME"text/plain"(), # hide
Supposition.@check commutative(intgen, intgen)
) # hide
nothing # hide

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.

!!! note "Nesting @testset" From Julia 1.11 onwards, @check can also report its own results as part of a parent @testset. This is unfortunately unsupported on 1.10 and earlier.

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.