Definitions

Test

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

Free Group in Julia

Complete code available on GitHub.

struct Symb
    symb::Symbol
    inverse::Bool
end

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

struct Word
    w::Vector{Symb}

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

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))
    end
    inverses_vec = map(len -> rand(rng, Bool, len), lens)

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

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)

    Word(reverse!(ret_vec))
end

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

julia> using JCheck: @add_predicate

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

Running the Tests

julia> using JCheck: @quickcheck

julia> @quickcheck qc
Test Summary: | Pass  Total
Test Inverse  |    1      1
                        

using Test: @test, @testset

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

    @quickcheck qc
end
                            

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,
                      "Commutativity",
                      (word::Word, word2::Word) ->
                          pred_commute(word, word2))
Free Group Over {a, b, c}: 2 predicates and 2 free variables:
word::Word
word2::Word
                        

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.
                        

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)]
                        

Shrinkage

• 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