JCheck.jl: Randomized Property Testing Made Easy


JuliaCon 2022

July 2022



Act of validating a software
Unit Test
Partial test of a software (part tested \( \Leftrightarrow \) unit)
  • Usually, output of test is compared against correct one \( \Rightarrow \) has to be known beforehand

Example: Unit Test in Julia

julia> using Test: @test

julia> arg_is42(x) = x == 42
arg_is42 (generic function with 1 method)

julia> @test arg_is42(41) == false
Test Passed
  Expression: arg_is42(41) == false
   Evaluated: false == false

Property-Based Testing

  • Specify properties instead of output
  • Often relies on random input generation
  • Closely related to fuzzing

Example: Free group on \( S \)

  • Generating set \( S = \left\{ a, b, c, \ldots \right\} \)
  • Inverse set \( S^{-1} = \left\{ x^{-1} : x \in S \right\}\)
  • A word on \( S \) is any written product of symbols of \( S \cup S^{-1} \)
$$ \begin{align*} S &= \left\{ a, b, c \right\}\\ S^{-1} &= \left\{ a^{-1}, b^{-1}, c^{-1} \right\}\\ W_0 &= accb^{-1} \textcolor{#9558b2}{\overbrace{c c^{-1}}^{\mathclap{\text{reduction}}}} c b\\ &= \textcolor{#4d7e65}{\underbrace{accb^{-1} c b}_{\mathclap{\text{reduced form}}}} \end{align*} $$

\( F_S \) is the group formed by \(\left\{ \text{reduced words on } S \right\}\) together with concatenation, meaning:

  • concatenation is associative (obviously 🤷)
  • there is an identity element (the empty word)
  • each element has an inverse (\( \omega \omega^{-1} = \omega^{-1} \omega = \text{empty word} \))

Property testing with JCheck.jl

Free Group in Julia

Complete code available on GitHub.

struct Symb

function reduce end # Reduces a vector of `Symb`.

struct Word

    Word(w) = new(reduce(w))

function concat end # Concatenates `Word`s.
macro word end # Convenience macro to construct `Word`s.
function Base.one end # Empty `Word` (identity element).

Generating Inputs

As easy as overloading the generate method!

import JCheck: generate

function generate(rng, ::Type{Word}, n)
    lens = rand(rng, 1:100, n)

    symbols_vec = map(lens) do len
        Symbol.(rand(rng, 'a':'c', len))
    inverses_vec = map(len -> rand(rng, Bool, len), lens)

    map(symbols_vec, inverses_vec) do symbols, inverses
        Word(map(Symb, symbols, inverses))

Group Properties

Is our implementation a group? Let's try to disprove it with JCheck.jl!

julia> using JCheck: Quickcheck

julia> qc = Quickcheck("Free Group Over {a, b, c}")
Free Group over {a, b, c}: 0 predicate and 0 free variable.

Adding Predicates

function Base.inv(word::Word)
    ret_vec = map(inv, word.w)


pred_inverse(word) =
    concat(word, inv(word)) ==
    concat(inv(word), word) ==

julia> using JCheck: @add_predicate

julia> @add_predicate(qc,
                      word::Word -> pred_inverse(word))
Free Group over {a, b, c}: 1 predicate and 1 free variable.

Running the Tests

julia> using JCheck: @quickcheck

julia> @quickcheck qc
Test Summary: | Pass  Total
Test Inverse  |    1      1
  • Integrates seamlessly with Julia's Test module

using Test: @test, @testset

@testset "Group Properties" begin
    @test (@word a b) == (@word a b b-1 b)

    @quickcheck qc

Test Summary:    | Pass  Total
Group Properties |    2      2

Failing Predicate

\( F_S \) is not commutative in general 😟

pred_commute(w1, w2) = concat(w1, w2) == concat(w2, w1)

julia> @add_predicate(qc,
                      (word::Word, word2::Word) ->
                          pred_commute(word, word2))
Free Group Over {a, b, c}: 2 predicates and 2 free variables:

Failing Predicate — Test Output

┌ Warning: Predicate "Commutativity" does not hold for
|          valuation (word = a-1 b a-1 b c-1 , word2 = c b-1 a )
└ @ JCheck [...]/Quickcheck.jl:310
Some predicates do not hold for some valuations; they have been saved to
JCheck_YYY-MM-DD_HH-MM-SS.jchk. Use function load and macro @getcases to explore problematic cases.

Test Summary:        | Pass  Fail  Total
Group Properties     |    2     1      3
  Test Inverse       |    1            1
  Test Commutativity |          1      1
ERROR: Some tests did not pass: 2 passed, 1 failed, 0 errored, 0 broken.

Other Features

Special Cases

  • Often useful to test a few non-random inputs (limiting cases, ...)
  • Can easily be done without JCheck, but might be more convenient (Cartesian product of inputs, ...)

using JCheck: specialcases

specialcases(::Type{Word}) = [one(Word)]


  • Often easier to find problems with short/simple failing cases
  • Possible to implement a simplification procedure
  • Applied recursively by JCheck until input is non-failing

Shrinkage — Example

import JCheck: shrink, shrinkable

shrinkable(word::Word) = length(word) > 2

function shrink(word::Word)
    shrinkable(word) || return [word]

    n = length(word) ÷ 2
    [word[1:n], word[(n+1):end]]

┌ Warning: Predicate "Commutativity" does not hold for
|          valuation (word = c-1 , word2 = a b-1 )
└ @ JCheck [...]/Quickcheck.jl:310
┌ Warning: Predicate "Commutativity" does not hold for
|          valuation (word = a c-1 , word2 = a-1 )
└ @ JCheck ~/Projets/JCheck/src/Quickcheck.jl:310

Much easier to analyze 😀