Supposition.jl
Hello everyone! I am very excited to announce Supposition.jl, a property based testing/fuzzing framework using choice sequences, inspired by the Python framework Hypothesis. It supports Julia version 1.8 and up. The package uses ScopedValues.jl internally, so older versions can’t be supported - sorry!
Please do check out the documentation to get a taste for how to use the package. In particular, the section about Aligning Behavior & Documentation of functions is bound to be insightful 
On a high level, Supposition.jl has these capabilities:
- Minimization of generated examples
- Targeted exploration of the search space, to help prevent the fuzzer getting stuck
- Barring reflection on actual code coverage information, this works a form of coverage tracking (more & better things are planned though)
- Shrinking of encountered errors to the minimal input producing that specific error
- Targeted exploration of the search space, to help prevent the fuzzer getting stuck
- Powerful combination of existing generators into new ones
- Fuzzing of stateful datastructures & statemachines, with operations on them
- Deterministic replaying of previously seen failures
and these goals:
- Performance - a test framework should not be the bottleneck of a testsuite; avoidable bad performance is considered a bug, and has its own label on the issue tracker
- Ease of Use - bad UX is considered a bug, and has its own label on the issue tracker
- High Quality Documentation - bad Docs are considered a bug, and have their own label on the issue tracker
You’ll be the judge of whether Supposition.jl achieves them!
For more specific questions, feature requests and design ideas, please don’t hesitate to share them on the Discussions tab of the repository! Feel free to browse there too, there’s already a bunch of things I’d like to add on there. Most of them also already have a plan for how to implement them, so getting them done is mostly a question of time & budget.
Without further ado, here’s a short usage example:
julia> using Test, Supposition
julia> @testset "Examples" begin
# Get a generator for `Int8`
intgen = Data.Integers{Int8}()
# Define a property `foo` and feed it `Int8` from that generator
@check function foo(i=intgen)
i isa Int
end
# Define & run another property, reusing the generator
@check function bar(i=intgen)
i isa Int8
end
# Define a property that can error
@check function baba(i=intgen)
i < -5 || error()
end
# Feed a new generator to an existing property
@check bar(Data.Floats{Float16}())
# Mark properties as broken
@check broken=true function broke(b=Data.Booleans())
b isa String
end
# ...and lots more, so check out the docs!
end
┌ Error: Property doesn't hold!
│ Description = "foo"
│ Example = (i = -128,)
└ @ Supposition ~/Documents/projects/Supposition.jl/src/testset.jl:280
┌ Error: Property errored!
│ Description = "baba"
│ Example = (i = -5,)
│ exception =
│
│ Stacktrace:
│ [1] error()
│ @ Base ./error.jl:44
│ [2] (::var"#baba#11")(i::Int8)
│ @ Main ./REPL[2]:18
└ @ Supposition ~/Documents/projects/Supposition.jl/src/testset.jl:275
┌ Error: Property doesn't hold!
│ Description = "bar"
│ Example = (Float16(0.0),)
└ @ Supposition ~/Documents/projects/Supposition.jl/src/testset.jl:280
Test Summary: | Pass Fail Error Broken Total Time
Examples | 1 2 1 1 5 2.5s
foo | 1 1 1.0s
bar | 1 1 0.0s
baba | 1 1 0.2s
bar | 1 1 0.0s
broke | 1 1 0.0s
ERROR: Some tests did not pass: 1 passed, 2 failed, 1 errored, 1 broken.
FAQ
What is property based testing?
In a nutshell, property based testing (PBT) is a testing philosophy where instead of testing your code with individual minimal inputs, you instead define various properties that you’d like your code to have (such as - “serialize and deserialize should be the inverse of each other”), generate random inputs to your functions and ultimately test whether your code upholds the properties you want it to have when presented with that random input.
This approach can be much more fruitful in ensuring the API surface of a project doesn’t drift & stays aligned with the documentation, because the random input ensures your tests don’t stay green by chance. At the same time, the random nature of fuzzing helps exercise more distinct code paths than would otherwise be reached, resulting in higher coverage. Quite often, unusual combinations of arguments that are forgotten with manual example based unit testing are found immediately with fuzzing.
Why a new package?
Some people may remember my last package in this direction, PropCheck.jl, and may rightly wonder why I’m writing a new one. The reasons are simple:
PropCheck.jlwas (comparatively) slow.Supposition.jlis, in some circumstances, up to 1000x times faster while using 200x less memory than PropCheck. For other situations,PropCheck.jlfails completely due to overreliance on deeply nested functions that make the compiler give up when trying to infer a result type.Supposition.jlcan still easily handle these cases; for more information check out these comparison benchmarks from the documentation.- The architecture of
PropCheck.jlwas heavily inspired by Hedgehog, a property based testing framework for Haskell. While very powerful & type oriented, the heavy reliance on function-based abstractions makes this kind of architecture not a good fit for Julia. The inner workings are hard to follow, and I still (after more than 4 years of working on it) get lost in the inner details ofPropCheck.jl. In contrast, I can still easily holdSupposition.jlin my head. In addition, the web of functions & forced lazy abstractions made debugging internals quite painful - which is not the case inSupposition.jl(I’ve successfully usedSupposition.jlto debug itself, and a large portion of the testsuite is just dogfooding its own API). PropCheck.jlwasn’t able to minimize errors, and retrofitting that capability would have meant rewriting the entirety of the package anyway. Pretty much the same is true for replaying of failure cases and steering shrinking withtarget!, as can be done inSupposition.jlwithout much difficulty at all.PropCheck.jlhas a very clear distinction between “generation” and “execution” of a property; you cannot mix the two, and cannot have new data produced as part of the “execution” step that subsequently also shrinks together with the data from the “generation” step. This is trivial forSupposition.jl, and is supported out of the box (adding that feature once the core ofSupposition.jlwas done was literally a 12 line diff).
So while the core of PropCheck.jl is, for its purpose, very solid, it’s not easy to work on its internals at all and it can’t (with reasonable effort) support many of the features I ultimately wanted to support (as well as quite a number of additional ones that are not in this initial release of Supposition.jl yet ).
Can I use this for formal verification?
TL;DR:
No.
A bit longer:
As was the case with PropCheck.jl, Supposition.jl is not a tool for formal verification work, and I still firmly believe that we’re VERY far away from having that sort of capability in Julia. Most interfaces from Base or the ecosystem are very loosely defined, and few (if any) actually give hard guarantees over the datastructure & algorithms in question, making formal verification extremely difficult. Multiple dispatch only makes this more difficult, since anyone can just redefine a function to mean something entirely different on their particular object. Any formal guarantees must thus be made on a per-method basis, and there hasn’t been any progress on that front as far as I’m aware.
This is not to say that formal verification of Julia code will never be a thing - I just happen to think that before we as a community can run, we need to learn how to walk 
Supposition.jl is an attempt to help with that, by providing a tool that assists with finding the actual API boundary of any given function/datastructure.
I’ve already said it in the announcement of PropCheck.jl, but I’ll repeat it here: if this package becomes obsolete due to tremendous advances in formal methods & verification in Julia, I’ll happily retire this package to the annals of history
