diff --git a/dev/.documenter-siteinfo.json b/dev/.documenter-siteinfo.json index e27c456..e082b83 100644 --- a/dev/.documenter-siteinfo.json +++ b/dev/.documenter-siteinfo.json @@ -1 +1 @@ -{"documenter":{"julia_version":"1.10.2","generation_timestamp":"2024-03-14T17:35:36","documenter_version":"1.3.0"}} \ No newline at end of file +{"documenter":{"julia_version":"1.10.2","generation_timestamp":"2024-03-14T17:41:06","documenter_version":"1.3.0"}} \ No newline at end of file diff --git a/dev/Examples/basic.html b/dev/Examples/basic.html index 738b671..dcdfa64 100644 --- a/dev/Examples/basic.html +++ b/dev/Examples/basic.html @@ -35,4 +35,4 @@ 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.

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.

+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.

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.

diff --git a/dev/Examples/composition.html b/dev/Examples/composition.html index 5ed33c6..bac36d9 100644 --- a/dev/Examples/composition.html +++ b/dev/Examples/composition.html @@ -11,11 +11,11 @@ a + b*im end example(even_complex, 5)
5-element Vector{Complex{Int64}}:
-  4330504481792362756 + 991526633369953466im
- -5937152989431779906 - 14515684493316442im
- -1190139771756737034 - 1024001723129802114im
-  5857427233037395864 + 4334958247935356272im
- -3138609724702571308 - 8036647154652251224im

In essence, @composed takes a function that is given some generators, and ultimately returns a generator that runs the function on those given generators. As a full-fledged Possibility, you can of course do everything you'd expect to do with other Possibility objects from Supposition.jl, including using them as input to other @composed! This makes them a powerful tool for composing custom generators.

@check function all_complex_even(c=even_complex)
+  6783286361161715046 - 5684948202049968822im
+ -5759171981357965212 - 1967184722379113890im
+ -1140949718046290508 + 7068748584123091430im
+   898864789436359740 - 8246398294077639548im
+  4574817186779362426 + 4159963392733398680im

In essence, @composed takes a function that is given some generators, and ultimately returns a generator that runs the function on those given generators. As a full-fledged Possibility, you can of course do everything you'd expect to do with other Possibility objects from Supposition.jl, including using them as input to other @composed! This makes them a powerful tool for composing custom generators.

@check function all_complex_even(c=even_complex)
     iseven(real(c)) && iseven(imag(c))
 end
Test Summary:    | Pass  Total  Time
 all_complex_even |    1      1  0.0s
Type stability

The inferred type of objects created by a generator from @composed is a best effort and may be wider than expected. E.g. if the input generators are non-const globals, it can easily happen that type inference falls back to Any. The same goes for other type instabilities and the usual best-practices surrounding type stability.

In addition, @composed defines the function given to it as well as a regular function, which means that you can call & reuse it however you like:

complex_even(1.0,2.0)
0.0 + 2.0im

Filtering, mapping, and other combinators

filter

Of course, manually marking, mapping or filtering inside of @composed is sometimes a bit too much. For these cases, all Possibility support filter and map, returning a new Data.Satisfying or Data.Map Possibility respectively:

using Supposition
@@ -25,16 +25,16 @@
 f = filter(iseven, intgen)
 
 example(f, 10)
10-element Vector{UInt8}:
- 0x8e
- 0xf0
- 0x36
- 0x38
- 0xa6
- 0xd0
- 0xe0
- 0x9e
- 0x96
- 0xaa

Note that filtering is, in almost all cases, strictly worse than constructing the desired objects directly. For example, if the filtering predicate rejects too many examples from the input space, it can easily happen that no suitable examples can be found:

g = filter(>(typemax(UInt8)), intgen)
+ 0x0a
+ 0x10
+ 0xb8
+ 0x80
+ 0x5a
+ 0x5a
+ 0x0e
+ 0x0e
+ 0x12
+ 0xdc

Note that filtering is, in almost all cases, strictly worse than constructing the desired objects directly. For example, if the filtering predicate rejects too many examples from the input space, it can easily happen that no suitable examples can be found:

g = filter(>(typemax(UInt8)), intgen)
 example(g, 10)
ERROR: Tried sampling 100000 times, without getting a result. Perhaps you're filtering out too many examples?

It is best to only filter when you're certain that the part of the state space you're filtering out is not substantial.

map

In order to make it easier to directly construct conforming instances, you can use map, transforming the output of one Possibility into a different object:

using Supposition
 
 intgen = Data.Integers{UInt8}()
@@ -42,13 +42,13 @@
 m = map(makeeven, intgen)
 
 example(m, 10)
10-element Vector{UInt8}:
- 0xaa
- 0x8a
- 0x70
- 0x3a
+ 0x60
+ 0x60
+ 0x72
+ 0x80
+ 0x4a
+ 0x40
  0xce
- 0x6a
- 0xf6
- 0x1e
- 0xc0
- 0x8c
Type stability

The inferred type of objects created by a generator from map is a best effort and may be wider than expected. Ensure your function f is easily inferrable to have good chances for mapping it to be inferable as well.

+ 0xa4 + 0xa0 + 0x8c
Type stability

The inferred type of objects created by a generator from map is a best effort and may be wider than expected. Ensure your function f is easily inferrable to have good chances for mapping it to be inferable as well.

diff --git a/dev/Examples/docalignment.html b/dev/Examples/docalignment.html index fcc5d43..c1748ea 100644 --- a/dev/Examples/docalignment.html +++ b/dev/Examples/docalignment.html @@ -102,7 +102,7 @@ end end
┌ Error: Property doesn't hold!
 │   Description = "sin_offset"
-│   Example = (a = 1.43e-322, b = 4.070952988028544e144)
+│   Example = (a = 1.43e-322, b = -3.0569214950521665e62)
 └ @ Supposition ~/work/Supposition.jl/Supposition.jl/src/testset.jl:280
 Test Summary:   |Time
 offset identity | None  0.1s

We have to make do with a subset of all properties then, such as "the output of sincos should == the outputs of sin and cos on their own", or properties that avoid addition & subtraction.

@testset "sincos properties" begin
@@ -136,4 +136,4 @@
   !!! compat "Julia 1.3"
       This function requires at least Julia 1.3.
   """
-  sincosd

We've now not only documented the erroring behavior of sincosd, but also special values and their special behavior. In the process we've also found that for this particular function, not everything we might expect actually can hold true in general - and documenting that has good chances to be a helpful improvement for anyone stumbling over trigonometric functions for the first time (in the long run, most developers are newbies; experts are rare!)

At the end of this process, a developer should now have

Of course, there could be numerous other properties we'd like to test. For example, we may want to confirm that the output of sincos is always a 2-Tuple, or that if the input was non-NaN, the output values are in the closed interval [-1, 1], or that the output values are evenly distributed in that interval (up to a point - this is surprisingly difficult to do for large inputs!)

Interactions between functions

Once the general knowledge about single functions has been expanded and appropriately documented, it's time to ask the bigger question - how do these functions interact, and do they interact in a way that a developer would expect them to? Since this is more involved, I've dedicated an entire section to this: Stateful Testing.

These three sections present a natural progression from writing your first test with Supposition.jl, over documenting guarantees of single functions to finally investigating interactions between functions and the effect they have on the datastructures of day-to-day use.

+ sincosd

We've now not only documented the erroring behavior of sincosd, but also special values and their special behavior. In the process we've also found that for this particular function, not everything we might expect actually can hold true in general - and documenting that has good chances to be a helpful improvement for anyone stumbling over trigonometric functions for the first time (in the long run, most developers are newbies; experts are rare!)

At the end of this process, a developer should now have

Of course, there could be numerous other properties we'd like to test. For example, we may want to confirm that the output of sincos is always a 2-Tuple, or that if the input was non-NaN, the output values are in the closed interval [-1, 1], or that the output values are evenly distributed in that interval (up to a point - this is surprisingly difficult to do for large inputs!)

Interactions between functions

Once the general knowledge about single functions has been expanded and appropriately documented, it's time to ask the bigger question - how do these functions interact, and do they interact in a way that a developer would expect them to? Since this is more involved, I've dedicated an entire section to this: Stateful Testing.

These three sections present a natural progression from writing your first test with Supposition.jl, over documenting guarantees of single functions to finally investigating interactions between functions and the effect they have on the datastructures of day-to-day use.

diff --git a/dev/Examples/fuzzing.html b/dev/Examples/fuzzing.html index b616e27..8a1e20f 100644 --- a/dev/Examples/fuzzing.html +++ b/dev/Examples/fuzzing.html @@ -1,2 +1,2 @@ -- · Supposition.jl Documentation
GitHub
+- · Supposition.jl Documentation
GitHub
diff --git a/dev/Examples/recursive.html b/dev/Examples/recursive.html index ac72787..a05e07b 100644 --- a/dev/Examples/recursive.html +++ b/dev/Examples/recursive.html @@ -15,4 +15,4 @@ "\e^Y\x1cq\bEj8" => -4.31286e-135 "^" => Union{Nothing, Bool, Float64, String}[false] "\x0f \t;lgC\e\x15" => nothing - "Y266uYkn6" => -5.68895e-145 + "Y266uYkn6" => -5.68895e-145 diff --git a/dev/Examples/stateful.html b/dev/Examples/stateful.html index 688b463..95104be 100644 --- a/dev/Examples/stateful.html +++ b/dev/Examples/stateful.html @@ -33,11 +33,13 @@ raw_ops = (fill_small, fill_large, empty_small, empty_large, pour_small_into_large, pour_large_into_small) gen_ops = Data.Vectors(Data.SampledFrom(raw_ops)) -example(gen_ops)
5-element Vector{Function}:
- empty_large (generic function with 1 method)
- empty_large (generic function with 1 method)
- pour_large_into_small (generic function with 1 method)
+example(gen_ops)
7-element Vector{Function}:
+ fill_small (generic function with 1 method)
+ fill_small (generic function with 1 method)
  fill_large (generic function with 1 method)
+ pour_large_into_small (generic function with 1 method)
+ fill_small (generic function with 1 method)
+ pour_small_into_large (generic function with 1 method)
  empty_small (generic function with 1 method)

Generating a sequence of operations is simply generating a vector from all possible ones! This is the input to our property. We declare that for all sequences of operations we can do with a Jug, all invariants we expect must hold true.

Speaking of invariants, we need three of them that must be preserved at all times:

  1. The small jug must ALWAYS have a fill level between 0 and 3 (inclusive).
  2. The large jug must ALWAYS have a fill level between 0 and 5 (inclusive).
  3. The large just must NEVER have a fill level of exactly 4.

The last invariant may look a bit odd, but remember that Supposition.jl is trying to find a falsifying example. The first two invariants are sanity checks to make sure that our pouring functions are well behaved; the last invariant is the solution we want to find, by combining the operations above in an arbitrary order. Let's translate these into functions as well:

small_jug_invariant(j::Jugs) = 0 <= j.small <= 3
 large_jug_invariant(j::Jugs) = 0 <= j.large <= 5
 level_invariant(j::Jugs) = j.large != 4
@@ -57,10 +59,10 @@
     return true
 end
┌ Error: Property doesn't hold!
 │   Description = "solve_die_hard"
-│   Example = (ops = Function[Main.fill_large, Main.pour_large_into_small, Main.empty_small, Main.pour_large_into_small, Main.fill_large, Main.pour_large_into_small],)
+│   Example = (ops = Function[Main.fill_small, Main.pour_small_into_large, Main.fill_small, Main.pour_small_into_large, Main.empty_large, Main.pour_small_into_large, Main.fill_small, Main.pour_small_into_large],)
 └ @ Supposition ~/work/Supposition.jl/Supposition.jl/src/testset.jl:280
-Test Summary:  | Fail  Total  Time
-solve_die_hard |    1      1  0.1s

This pattern is very extensible, and a good candidate for the next UX overhaul (getting a reported failure for the target we actually want to find is quite bad UX). Nevertheless, it already works right now!

Balancing a heap

The previous example showed how we can check these kinds of operations based invariants on an immutable struct. There is no reason why we can't do the same with a mutable struct (or at least, a struct containing a mutable object) though, so let's look at another example: ensuring a heap observes its heap property. As a quick reminder, the heap property for a binary heap is that each child of a node is <= than that node, resulting in what's called a "Max-Heap" (due to the maximum being at the root). Similarly, if the property for children is >=, we get a "Min-Heap". Here, we're going to implement a Min-Heap.

First, we need to define our datastructure:

struct Heap{T}
+Test Summary:  | Fail  Total     Time
+solve_die_hard |    1      1  1m12.5s

This pattern is very extensible, and a good candidate for the next UX overhaul (getting a reported failure for the target we actually want to find is quite bad UX). Nevertheless, it already works right now!

Balancing a heap

The previous example showed how we can check these kinds of operations based invariants on an immutable struct. There is no reason why we can't do the same with a mutable struct (or at least, a struct containing a mutable object) though, so let's look at another example: ensuring a heap observes its heap property. As a quick reminder, the heap property for a binary heap is that each child of a node is <= than that node, resulting in what's called a "Max-Heap" (due to the maximum being at the root). Similarly, if the property for children is >=, we get a "Min-Heap". Here, we're going to implement a Min-Heap.

First, we need to define our datastructure:

struct Heap{T}
     data::Vector{T}
 end
 Heap{T}() where T = Heap{T}(T[])

as well as the usual operations (isempty, push!, pop!) on that heap:

Written in code, this might look like this:

Base.isempty(heap::Heap) = isempty(heap.data)
@@ -163,7 +165,7 @@
     return true
 end
┌ Error: Property doesn't hold!
 │   Description = "test_heap"
-│   Example = (ops = Union{Tuple{typeof(pop!), Nothing}, Tuple{typeof(push!), UInt64}}[(push!, 0x0000000000000001), (push!, 0x0000000000000000), (push!, 0x0000000000000000), (pop!, nothing), (pop!, nothing)],)
+│   Example = (ops = Union{Tuple{typeof(pop!), Nothing}, Tuple{typeof(push!), UInt64}}[(push!, 0x0000000000000001), (push!, 0x0000000000000000), (pop!, nothing), (push!, 0x0000000000000000), (push!, 0x0000000000000000), (pop!, nothing), (pop!, nothing)],)
 └ @ Supposition ~/work/Supposition.jl/Supposition.jl/src/testset.jl:280
 Test Summary: | Fail  Total  Time
 test_heap     |    1      1  0.2s

Once again, we find our familiar example UInt[0x0, 0x1, 0x0], though this time in the form of operations done on the heap:

ops = Union{Tuple{typeof(pop!), Nothing}, Tuple{typeof(push!), UInt64}}[
@@ -176,4 +178,4 @@
 gen_fixed_ops = Data.Vectors(Data.OneOf(gen_push, gen_fixed_pop); max_size=10_000)
 
 @check test_heap(gen_fixed_ops)
Test Summary: | Pass  Total   Time
-test_heap     |    1      1  26.5s

Now this is much more thorough testing!

+test_heap | 1 1 25.8s

Now this is much more thorough testing!

diff --git a/dev/Examples/target.html b/dev/Examples/target.html index 15bbb43..d070b57 100644 --- a/dev/Examples/target.html +++ b/dev/Examples/target.html @@ -10,16 +10,16 @@ @check rng=Xoshiro(1) function israndgoal(f=Data.Floats{Float64}()) f != rand_goal end
┌ Info: Our random goal is:
-└   Goal = 0.5250656715501921
+└   Goal = 0.12877769667827643
 Test Summary: | Pass  Total  Time
 israndgoal    |    1      1  0.0s

The default for the number of attempts @check tries to feed to israndgoal is 10_000; the test still passes, which means Supposition.jl was unable to find the number we claim can't be generated. We can increase this by an almost arbitrary amount, without having the test fail:

@check max_examples=1_000_000 rng=Xoshiro(1) israndgoal(Data.Floats{Float64}())
Test Summary: | Pass  Total  Time
-israndgoal    |    1      1  2.5s

Clearly, there needs to be something done so that we can hint to Supposition.jl what we consider to be "better" inputs, so that Supposition.jl can focus on them. This functionality is target!. target! takes a number and records it as the score for the given generated inputs. During the generation phase, Supposition.jl tracks which example was considered "the best", i.e. which had the highest score, and subsequently attempts to find further examples that further increase this score, hopefully finding a maximum. For our example here, we can simply use the absolute distance from our input to the artificial goal as a score:

sr = @check rng=Xoshiro(1) function israndgoal(f=Data.Floats{Float64}())
+israndgoal    |    1      1  2.6s

Clearly, there needs to be something done so that we can hint to Supposition.jl what we consider to be "better" inputs, so that Supposition.jl can focus on them. This functionality is target!. target! takes a number and records it as the score for the given generated inputs. During the generation phase, Supposition.jl tracks which example was considered "the best", i.e. which had the highest score, and subsequently attempts to find further examples that further increase this score, hopefully finding a maximum. For our example here, we can simply use the absolute distance from our input to the artificial goal as a score:

sr = @check rng=Xoshiro(1) function israndgoal(f=Data.Floats{Float64}())
     # negative absolute distance, because we want to _minimize_ the distance
     target!(-abs(rand_goal - f))
     f != rand_goal
 end
┌ Error: Property doesn't hold!
 │   Description = "israndgoal"
-│   Example = (f = 0.5250656715501921,)
+│   Example = (f = 0.12877769667827643,)
 └ @ Supposition ~/work/Supposition.jl/Supposition.jl/src/testset.jl:280
 Test Summary: | Fail  Total  Time
-israndgoal    |    1      1  0.1s

which results in Supposition.jl finding the sole counterexample in a comparatively very small number of inputs:

Supposition.num_testcases(sr)
6102

In more complex situations where you don't have a very clear goal to minimize or maximize, target! can be very useful as a guiding force, as long as the metric you're using is good. I don't have a proof for it, but in general, you'll probably want the metric to be admissible.

+israndgoal | 1 1 0.1s

which results in Supposition.jl finding the sole counterexample in a comparatively very small number of inputs:

Supposition.num_testcases(sr)
6244

In more complex situations where you don't have a very clear goal to minimize or maximize, target! can be very useful as a guiding force, as long as the metric you're using is good. I don't have a proof for it, but in general, you'll probably want the metric to be admissible.

diff --git a/dev/api.html b/dev/api.html index 1e4599a..2874d9b 100644 --- a/dev/api.html +++ b/dev/api.html @@ -1,5 +1,5 @@ -API Reference · Supposition.jl Documentation
GitHub

Documentation Reference

This section contains a complete reference of everything Supposition.jl contains, on one page. This is not a devdocs section, but a reference, for quick lookups of what something does, without having to hunt for the exact definition in the source code. A proper devdocs section with a high level introduction will be added at a later date.

Stability

The entries written on this page are automatically generated and DO NOT represent the currently supported API surface. Feel free to use anything you can find here, but be aware that just because it's listed here, does not mean it's covered under semver (though it may be - check Userfacing API if you're unsure).

Data reference

The Data module contains most everyday objects you're going to use when writing property based tests with Supposition.jl. For example, the basic generators for integers, strings, floating point values etc. are defined here. Everything listed in this section is considered supported under semver.

Functions

Base.:| — Method
|(::Possibility{T}, ::Possibility{S}) where {T,S} -> OneOf{Union{T,S}}

Combine two Possibility into one, sampling uniformly from either.

If either of the two arguments is a OneOf, the resulting object acts as if all original non-OneOf had be given to OneOf instead. That is, e.g. OneOf(a, b) | c will act like OneOf(a,b,c).

See also OneOf.

source
Base.filter — Method
filter(f, pos::Possibility)

Filter the output of produce! on pos by applying the predicate f.

No stalling

In order not to stall generation of values, this will not try to produce a value from pos forever, but reject the testcase after some attempts.

source
Base.map — Method
map(f, pos::Possibility)

Apply f to the result of calling produce! on pos (lazy mapping).

Equivalent to calling Map(pos, f).

See also Map.

source
Supposition.Data.BitIntegers — Method
BitIntegers() <: Possibility{Union{Int128, Int16, Int32, Int64, Int8, UInt128, UInt16, UInt32, UInt64, UInt8}}

A Possibility for generating all possible bitintegers with fixed size.

source
Supposition.Data.bind — Method
bind(f, pos::Possibility)

Maps the output of produce! on pos through f, and calls produce! on the result again. f is expected to take a value and return a Possibility.

Equivalent to calling Bind(pos, f).

See also Bind.

source
Supposition.Data.produce! — Function
produce!(tc::TestCase, pos::Possibility{T}) -> T

Produces a value from the given Possibility, recording the required choices in the TestCase tc.

This needs to be implemented for custom Possibility objects, passing the given tc to any inner requirements directly.

See also Supposition.produce!

Examples

You should not call this function when you have a Possibility and want to inspect what an object produced by that Possibility looks like - use example for that instead.

source
Supposition.Data.recursive — Method
recursive(f, pos::Possibility; max_layers=5)

Recursively expand pos into deeper nested Possibility by repeatedly passing pos itself to f. f returns a new Possibility, which is then passed into f again until the maximum depth is achieved.

Equivalent to calling Recursive(pos, f).

See also Recursive.

source
Supposition.Data.AsciiCharacters — Type
AsciiCharacters() <: Possibility{Char}

A Possibility of producing arbitrary Char instances that are isascii. More efficient than filtering Characters.

julia> using Supposition
+API Reference · Supposition.jl Documentation
GitHub
Documentation Reference
This section contains a complete reference of everything Supposition.jl contains, on one page. This is not a devdocs section, but a reference, for quick lookups of what something does, without having to hunt for the exact definition in the source code. A proper devdocs section with a high level introduction will be added at a later date.
Stability
The entries written on this page are automatically generated and DO NOT represent the currently supported API surface. Feel free to use anything you can find here, but be aware that just because it's listed here, does not mean it's covered under semver (though it may be - check Userfacing API if you're unsure).
Data reference
The Data module contains most everyday objects you're going to use when writing property based tests with Supposition.jl. For example, the basic generators for integers, strings, floating point values etc. are defined here. Everything listed in this section is considered supported under semver.
Functions
Base.:| — Method
|(::Possibility{T}, ::Possibility{S}) where {T,S} -> OneOf{Union{T,S}}
Combine two Possibility into one, sampling uniformly from either.
If either of the two arguments is a OneOf, the resulting object acts as if all original non-OneOf had be given to OneOf instead. That is, e.g. OneOf(a, b) | c will act like OneOf(a,b,c).
See also OneOf.
source
Base.filter — Method
filter(f, pos::Possibility)
Filter the output of produce! on pos by applying the predicate f.
No stalling
In order not to stall generation of values, this will not try to produce a value from pos forever, but reject the testcase after some attempts.
source
Base.map — Method
map(f, pos::Possibility)
Apply f to the result of calling produce! on pos (lazy mapping).
Equivalent to calling Map(pos, f).
See also Map.
source
Supposition.Data.BitIntegers — Method
BitIntegers() <: Possibility{Union{Int128, Int16, Int32, Int64, Int8, UInt128, UInt16, UInt32, UInt64, UInt8}}
A Possibility for generating all possible bitintegers with fixed size.
source
Supposition.Data.bind — Method
bind(f, pos::Possibility)
Maps the output of produce! on pos through f, and calls produce! on the result again. f is expected to take a value and return a Possibility.
Equivalent to calling Bind(pos, f).
See also Bind.
source
Supposition.Data.produce! — Function
produce!(tc::TestCase, pos::Possibility{T}) -> T
Produces a value from the given Possibility, recording the required choices in the TestCase tc.
This needs to be implemented for custom Possibility objects, passing the given tc to any inner requirements directly.
See also Supposition.produce!
Examples
You should not call this function when you have a Possibility and want to inspect what an object produced by that Possibility looks like - use example for that instead.
source
Supposition.Data.recursive — Method
recursive(f, pos::Possibility; max_layers=5)
Recursively expand pos into deeper nested Possibility by repeatedly passing pos itself to f. f returns a new Possibility, which is then passed into f again until the maximum depth is achieved.
Equivalent to calling Recursive(pos, f).
See also Recursive.
source
Supposition.Data.AsciiCharacters — Type
AsciiCharacters() <: Possibility{Char}
A Possibility of producing arbitrary Char instances that are isascii. More efficient than filtering Characters.
julia> using Supposition
 
 julia> ascii = Data.AsciiCharacters()
 
@@ -9,7 +9,7 @@
  'i': ASCII/Unicode U+0069 (category Ll: Letter, lowercase)
  'R': ASCII/Unicode U+0052 (category Lu: Letter, uppercase)
  '\f': ASCII/Unicode U+000C (category Cc: Other, control)
- '>': ASCII/Unicode U+003E (category Sm: Symbol, math)
source
Supposition.Data.Bind — Type
Bind(source::Possibility, f)
Binds f to source, i.e., on produce!(::Bind, ::TestCase) this calls produce! on source, the result of which is passed to f, the output of which will be used as input to produce! again.
In other words, f takes a value produce!d by source and gives back a Possibility that is then immediately produce!d from.
Equivalent to bind(f, source).
source
Supposition.Data.Booleans — Type
Booleans() <: Possibility{Bool}
A Possibility for sampling boolean values.
julia> using Supposition
+ '>': ASCII/Unicode U+003E (category Sm: Symbol, math)
source
Supposition.Data.Bind — Type
Bind(source::Possibility, f)
Binds f to source, i.e., on produce!(::Bind, ::TestCase) this calls produce! on source, the result of which is passed to f, the output of which will be used as input to produce! again.
In other words, f takes a value produce!d by source and gives back a Possibility that is then immediately produce!d from.
Equivalent to bind(f, source).
source
Supposition.Data.Booleans — Type
Booleans() <: Possibility{Bool}
A Possibility for sampling boolean values.
julia> using Supposition
 
 julia> bools = Data.Booleans()
 
@@ -18,7 +18,7 @@
  0
  1
  0
- 1
source
Supposition.Data.Characters — Type
Characters(;valid::Bool = false) <: Possibility{Char}
A Possibility of producing arbitrary Char instances.
Unicode
This will produce! ANY possible Char by default, not just valid unicode codepoints! To only produce valid unicode codepoints, pass valid=true as a keyword argument.
julia> using Supposition
+ 1
source
Supposition.Data.Characters — Type
Characters(;valid::Bool = false) <: Possibility{Char}
A Possibility of producing arbitrary Char instances.
Unicode
This will produce! ANY possible Char by default, not just valid unicode codepoints! To only produce valid unicode codepoints, pass valid=true as a keyword argument.
julia> using Supposition
 
 julia> chars = Data.Characters()
 
@@ -28,12 +28,12 @@
  '𰳍': Unicode U+30CCD (category Lo: Letter, other)
  '\U6ec9c': Unicode U+6EC9C (category Cn: Other, not assigned)
  '\U1a05c5': Unicode U+1A05C5 (category In: Invalid, too high)
- '𓂫': Unicode U+130AB (category Lo: Letter, other)
source
Supposition.Data.Dicts — Type
Dicts(keys::Possibility, values::Possibility; min_size=0, max_size=10_000)
A Possibility for generating Dict objects. The keys are drawn from keys,     while the values are drawn from values. min_size/max_size control     the number of objects placed into the resulting Dict, respectively.
julia> dicts = Data.Dicts(Data.Integers{UInt8}(), Data.Integers{Int8}(); max_size=3);
+ '𓂫': Unicode U+130AB (category Lo: Letter, other)
source
Supposition.Data.Dicts — Type
Dicts(keys::Possibility, values::Possibility; min_size=0, max_size=10_000)
A Possibility for generating Dict objects. The keys are drawn from keys,     while the values are drawn from values. min_size/max_size control     the number of objects placed into the resulting Dict, respectively.
julia> dicts = Data.Dicts(Data.Integers{UInt8}(), Data.Integers{Int8}(); max_size=3);
 
 julia> example(dicts)
 Dict{UInt8, Int8} with 2 entries:
   0x54 => -29
-  0x1f => -28
source
Supposition.Data.Floats — Method
Floats(;nans=true, infs=true) <: Possibility{Union{Float64,Float32,Float16}}
A catch-all for generating instances of all three IEEE floating point types.
source
Supposition.Data.Floats — Type
Floats{T <: Union{Float16,Float32,Float64}}(;infs=true, nans=true) <: Possibility{T}
A Possibility for sampling floating point values.
The keyword infs controls whether infinities can be generated. nans controls whether     any NaN (signaling & quiet) will be generated.
Inf, Nan
This possibility will generate any valid instance, including positive and negative infinities, signaling and quiet NaNs and every possible float.
julia> using Supposition
+  0x1f => -28
source
Supposition.Data.Floats — Method
Floats(;nans=true, infs=true) <: Possibility{Union{Float64,Float32,Float16}}
A catch-all for generating instances of all three IEEE floating point types.
source
Supposition.Data.Floats — Type
Floats{T <: Union{Float16,Float32,Float64}}(;infs=true, nans=true) <: Possibility{T}
A Possibility for sampling floating point values.
The keyword infs controls whether infinities can be generated. nans controls whether     any NaN (signaling & quiet) will be generated.
Inf, Nan
This possibility will generate any valid instance, including positive and negative infinities, signaling and quiet NaNs and every possible float.
julia> using Supposition
 
 julia> floats = Data.Floats{Float16}()
 
@@ -43,7 +43,7 @@
    1.459e4
    3.277
  NaN
-  -0.0001688
source
Supposition.Data.Integers — Type
Integers(minimum::T, maximum::T) <: Possibility{T <: Integer}
 Integers{T}() <: Possibility{T <: Integer}
A Possibility representing drawing integers from [minimum, maximum]. The second constructors draws from the entirety of T.
Produced values are of type T.
julia> using Supposition
 
 julia> is = Data.Integers{Int}()
@@ -54,7 +54,7 @@
   4430062772779972974
     -9995351034504801
   2894734754389242339
- -6640496903289665416
source
Supposition.Data.Just — Type
Just(value::T) <: Possibility{T}
A Possibility that always produces value.
Mutable Data
The source object given to this Just is not copied when produce! is called. Be careful with mutable data!
julia> using Supposition
+ -6640496903289665416
source
Supposition.Data.Just — Type
Just(value::T) <: Possibility{T}
A Possibility that always produces value.
Mutable Data
The source object given to this Just is not copied when produce! is called. Be careful with mutable data!
julia> using Supposition
 
 julia> three = Data.Just(3)
 
@@ -62,14 +62,14 @@
 3-element Vector{Int64}:
  3
  3
- 3
source
Supposition.Data.Map — Type
Map(source::Possibility, f) <: Possibility
A Possibility representing mapping values from source through f.
Equivalent to calling map(f, source).
The pre-calculated return type of Map is a best effort and may be wider than necessary.
julia> using Supposition
+ 3
source
Supposition.Data.Map — Type
Map(source::Possibility, f) <: Possibility
A Possibility representing mapping values from source through f.
Equivalent to calling map(f, source).
The pre-calculated return type of Map is a best effort and may be wider than necessary.
julia> using Supposition
 
 julia> makeeven(x) = (x ÷ 2) * 2
 
 julia> pos = map(makeeven, Data.Integers{Int8}())
 
 julia> all(iseven, example(pos, 10_000))
-true
source
Supposition.Data.OneOf — Type
OneOf(pos::Possibility...) <: Possibility
A Possibility able to generate any of the examples one of the given Possibility can produce. The given Possibility are sampled from uniformly.
At least one Possibility needs to be given to OneOf.
postype(::OneOf) is inferred as a best effort, and may be wider than necessary.
OneOf can also be constructed through use of a | b on Possibility. Constructed in this way, if either a or b is already a OneOf, the resulting OneOf acts as if it had been given the original Possibility objects in the first place. That is, OneOf(a, b) | c acts like OneOf(a, b, c).
julia> of = Data.OneOf(Data.Integers{Int8}(), Data.Integers{UInt8}());
+true
source
Supposition.Data.OneOf — Type
OneOf(pos::Possibility...) <: Possibility
A Possibility able to generate any of the examples one of the given Possibility can produce. The given Possibility are sampled from uniformly.
At least one Possibility needs to be given to OneOf.
postype(::OneOf) is inferred as a best effort, and may be wider than necessary.
OneOf can also be constructed through use of a | b on Possibility. Constructed in this way, if either a or b is already a OneOf, the resulting OneOf acts as if it had been given the original Possibility objects in the first place. That is, OneOf(a, b) | c acts like OneOf(a, b, c).
julia> of = Data.OneOf(Data.Integers{Int8}(), Data.Integers{UInt8}());
 
 julia> Data.postype(of)
 Union{Int8, UInt8}
@@ -82,14 +82,14 @@
 (-83, Int8)
 
 julia> example(ex)
-(0x9f, UInt8)
source
Supposition.Data.Pairs — Type
Pairs(first::Possibility{T}, second::Possibility{S}) where {T,S} <: Possibility{Pair{T,S}}
A Possibility for producing a => b pairs. a is produced by first, b is produced by second.
julia> p = Data.Pairs(Data.Integers{UInt8}(), Data.Floats{Float64}());
+(0x9f, UInt8)
source
Supposition.Data.Pairs — Type
Pairs(first::Possibility{T}, second::Possibility{S}) where {T,S} <: Possibility{Pair{T,S}}
A Possibility for producing a => b pairs. a is produced by first, b is produced by second.
julia> p = Data.Pairs(Data.Integers{UInt8}(), Data.Floats{Float64}());
 
 julia> example(p, 4)
 4-element Vector{Pair{UInt8, Float64}}:
  0x41 => 4.1183566661848205e-230
  0x48 => -2.2653631095108555e-119
  0x2a => -6.564396855333643e224
- 0xec => 1.9330751262581671e-53
source
Supposition.Data.Recursive — Type
Recursive(base::Possibility, extend; max_layers::Int=5) <: Possibility{T}
A Possibility for generating recursive data structures. base is the basecase of the recursion. extend is a function returning a new Possibility when given a Possibility, called to recursively expand a tree starting from base. The returned Possibility is fed back into extend again, expanding the recursion by one layer.
max_layers designates the maximum number of times extend will be used to wrap base in new layers. This must be at least 1, so that at least the base case can always be generated.
Equivalent to calling recursive(extend, base).
Examples
julia> base = Data.Integers{UInt8}()
+ 0xec => 1.9330751262581671e-53
source
Supposition.Data.Recursive — Type
Recursive(base::Possibility, extend; max_layers::Int=5) <: Possibility{T}
A Possibility for generating recursive data structures. base is the basecase of the recursion. extend is a function returning a new Possibility when given a Possibility, called to recursively expand a tree starting from base. The returned Possibility is fed back into extend again, expanding the recursion by one layer.
max_layers designates the maximum number of times extend will be used to wrap base in new layers. This must be at least 1, so that at least the base case can always be generated.
Equivalent to calling recursive(extend, base).
Examples
julia> base = Data.Integers{UInt8}()
 
 julia> wrap(pos) = Data.Vectors(pos; min_size=2, max_size=3)
 
@@ -112,7 +112,7 @@
 julia> example(rec)
 2-element Vector{UInt8}:
  0xbd
- 0x25
source
Supposition.Data.SampledFrom — Type
SampledFrom(collection) <: Possibility{eltype(collection)}
A Possibility for sampling uniformly from collection.
collection, as well as its eachindex, is assumed to be indexable.
Mutable Data
The source objects from the collection given to this SampledFrom is not copied when produce! is called. Be careful with mutable data!
julia> using Supposition
+ 0x25
source
Supposition.Data.SampledFrom — Type
SampledFrom(collection) <: Possibility{eltype(collection)}
A Possibility for sampling uniformly from collection.
collection, as well as its eachindex, is assumed to be indexable.
Mutable Data
The source objects from the collection given to this SampledFrom is not copied when produce! is called. Be careful with mutable data!
julia> using Supposition
 
 julia> sampler = Data.SampledFrom([1, 1, 1, 2])
 
@@ -121,12 +121,12 @@
  1
  1
  2
- 1
source
Supposition.Data.Satisfying — Type
Satisfying(source::Possibility, pred) <: Possibility
A Possibility representing values from source fulfilling pred.
Equivalent to calling filter(f, source).
julia> using Supposition
+ 1
source
Supposition.Data.Satisfying — Type
Satisfying(source::Possibility, pred) <: Possibility
A Possibility representing values from source fulfilling pred.
Equivalent to calling filter(f, source).
julia> using Supposition
 
 julia> pos = filter(iseven, Data.Integers{Int8}())
 
 julia> all(iseven, example(pos, 10_000))
-true
source
Supposition.Data.Text — Type
Text(alphabet::Possibility{Char}; min_len=0, max_len=10_000) <: Possibility{String}
A Possibility for producing Strings containing Chars of a given alphabet.
julia> using Supposition
+true
source
Supposition.Data.Text — Type
Text(alphabet::Possibility{Char}; min_len=0, max_len=10_000) <: Possibility{String}
A Possibility for producing Strings containing Chars of a given alphabet.
julia> using Supposition
 
 julia> text = Data.Text(Data.AsciiCharacters(); max_len=15)
 
@@ -136,7 +136,7 @@
  "hm\x172SJ-("
  "h`\x03\0\x01[[il"
  "\x0ep4"
- "9+Hk3 ii\x1eT"
source
Supposition.Data.Vectors — Type
Vectors(elements::Possibility{T}; min_size=0, max_size=10_000) <: Possibility{Vector{T}}
A Possibility representing drawing vectors with length l in min_size <= l <= max_size, holding elements of type T.
min_size and max_size must be positive numbers, with min_size <= max_size.
julia> using Supposition
+ "9+Hk3 ii\x1eT"
source
Supposition.Data.Vectors — Type
Vectors(elements::Possibility{T}; min_size=0, max_size=10_000) <: Possibility{Vector{T}}
A Possibility representing drawing vectors with length l in min_size <= l <= max_size, holding elements of type T.
min_size and max_size must be positive numbers, with min_size <= max_size.
julia> using Supposition
 
 julia> vs = Data.Vectors(Data.Floats{Float16}(); max_size=5)
 
@@ -144,7 +144,7 @@
 3-element Vector{Vector{Float16}}:
  [9.64e-5, 9.03e3, 0.04172, -0.0003352]
  [9.793e-5, -2.893, 62.62, 0.0001961]
- [-0.007023, NaN, 3.805, 0.1943]
source
Supposition reference
Supposition.@check — Macro
@check [key=val]... function...
The main way to declare & run a property based test. Called like so:
julia> using Supposition, Supposition.Data
+ [-0.007023, NaN, 3.805, 0.1943]
source
Supposition reference
Supposition.@check — Macro
@check [key=val]... function...
The main way to declare & run a property based test. Called like so:
julia> using Supposition, Supposition.Data
 
 julia> Supposition.@check [options...] function foo(a = Data.Text(Data.Characters(); max_len=10))
           length(a) > 8
@@ -159,7 +159,7 @@
 # use a custom Xoshiro instance
 julia> Supposition.@check rng=Xoshiro(1234) function foo(a = Data.Text(Data.Characters(); max_len=10))
           length(a) > 8
-       end
Hardware RNG
Be aware that you cannot pass a hardware RNG to @check directly. If you want to randomize based on hardware entropy, seed a copyable RNG like Xoshiro from your hardware RNG and pass that to @check instead. The RNG needs to be copyable for reproducibility.
source
Supposition.@composed — Macro
@composed
A way to compose multiple Possibility into one, by applying a function.
The return type is inferred as a best-effort!
Used like so:
julia> using Supposition, Supposition.Data
+       end
Hardware RNG
Be aware that you cannot pass a hardware RNG to @check directly. If you want to randomize based on hardware entropy, seed a copyable RNG like Xoshiro from your hardware RNG and pass that to @check instead. The RNG needs to be copyable for reproducibility.
source
Supposition.@composed — Macro
@composed
A way to compose multiple Possibility into one, by applying a function.
The return type is inferred as a best-effort!
Used like so:
julia> using Supposition, Supposition.Data
 
 julia> text = Data.Text(Data.AsciiCharacters(); max_len=10)
 
@@ -168,10 +168,10 @@
        end
 
 julia> example(gen)
-" 8:  giR2YL\rl"
source
Supposition.Data.produce! — Method
produce!(p::Possibility{T}) -> T
Produces a value from the given Possibility, recording the required choices in the currently active TestCase.
Callability
This can only be called while a testcase is currently being examined or an example for a Possibility is being actively generated. It is ok to call this inside of @composed or @check, as well as any functions only intended to be called from one of those places.
source
Supposition.adjust — Method
adjust(ts::TestState, attempt)
Adjust ts by testing for the choices given by attempt.
Returns whether attempt was by some measure better than the previously best attempt.
source
Supposition.assemble — Method
assemble(::T, sign::I, expo::I, frac::I) where {I, T <: Union{Float16, Float32, Float64}} -> T
Assembles sign, expo and frac arguments into the floating point number of type T it represents. sizeof(T) must match sizeof(I).
source
Supposition.assume! — Method
assume!(precondition::Bool)
If this precondition is not met, abort the test and mark the currently running testcase as invalid.
Callability
This can only be called while a testcase is currently being examined or an example for a Possibility is being actively generated. It is ok to call this inside of @composed or @check, as well as any functions only intended to be called from one of those places.
source
Supposition.choice! — Method
choice!(tc::TestCase, n)
Force a number of choices to occur, taking from the existing prefix first. If the prefix is exhausted, draw from [zero(n), n] instead.
source
Supposition.consider — Method
consider(ts::TestState, attempt::Attempt) -> Bool
Returns whether the given choices are a conceivable example for the testcase given by ts.
source
Supposition.err_less — Function
err_less(e1::E, e2::E) where E
A comparison function for exceptions, used when encountering an error in a property. Returns true if e1 is considered to be "easier" or "simpler" than e2. Only definable when both e1 and e2 have the same type.
This is optional to implement, but may be beneficial for shrinking counterexamples leading to an error with rich metadata, in which case err_less will be used to compare errors of the same type from different counterexamples. In particular, this function will likely be helpful for errors with metadata that is far removed from the input that caused the error itself, but would nevertheless be helpful when investigating the failure.
Coincidental Errors
There may also be situations where defining err_less won't help to find a smaller counterexample if the cause of the error is unrelated to the choices taken during generation. For instance, this is the case when there is no network connection and a Sockets.DNSError is thrown during the test, or there is a network connection but the host your program is trying to connect to does not have an entry in DNS.
source
Supposition.example — Method
example(pos::Possibility; tries=100_000, generation::Int)
Generate an example for the given Possibility.
example tries to have pos produce an example tries times and throws an error if pos doesn't produce one in that timeframe. generation indicates how "late" in a usual run of @check the example might have been generated.
Usage:
julia> using Supposition, Supposition.Data
+" 8:  giR2YL\rl"
source
Supposition.Data.produce! — Method
produce!(p::Possibility{T}) -> T
Produces a value from the given Possibility, recording the required choices in the currently active TestCase.
Callability
This can only be called while a testcase is currently being examined or an example for a Possibility is being actively generated. It is ok to call this inside of @composed or @check, as well as any functions only intended to be called from one of those places.
source
Supposition.adjust — Method
adjust(ts::TestState, attempt)
Adjust ts by testing for the choices given by attempt.
Returns whether attempt was by some measure better than the previously best attempt.
source
Supposition.assemble — Method
assemble(::T, sign::I, expo::I, frac::I) where {I, T <: Union{Float16, Float32, Float64}} -> T
Assembles sign, expo and frac arguments into the floating point number of type T it represents. sizeof(T) must match sizeof(I).
source
Supposition.assume! — Method
assume!(precondition::Bool)
If this precondition is not met, abort the test and mark the currently running testcase as invalid.
Callability
This can only be called while a testcase is currently being examined or an example for a Possibility is being actively generated. It is ok to call this inside of @composed or @check, as well as any functions only intended to be called from one of those places.
source
Supposition.choice! — Method
choice!(tc::TestCase, n)
Force a number of choices to occur, taking from the existing prefix first. If the prefix is exhausted, draw from [zero(n), n] instead.
source
Supposition.consider — Method
consider(ts::TestState, attempt::Attempt) -> Bool
Returns whether the given choices are a conceivable example for the testcase given by ts.
source
Supposition.err_less — Function
err_less(e1::E, e2::E) where E
A comparison function for exceptions, used when encountering an error in a property. Returns true if e1 is considered to be "easier" or "simpler" than e2. Only definable when both e1 and e2 have the same type.
This is optional to implement, but may be beneficial for shrinking counterexamples leading to an error with rich metadata, in which case err_less will be used to compare errors of the same type from different counterexamples. In particular, this function will likely be helpful for errors with metadata that is far removed from the input that caused the error itself, but would nevertheless be helpful when investigating the failure.
Coincidental Errors
There may also be situations where defining err_less won't help to find a smaller counterexample if the cause of the error is unrelated to the choices taken during generation. For instance, this is the case when there is no network connection and a Sockets.DNSError is thrown during the test, or there is a network connection but the host your program is trying to connect to does not have an entry in DNS.
source
Supposition.example — Method
example(pos::Possibility; tries=100_000, generation::Int)
Generate an example for the given Possibility.
example tries to have pos produce an example tries times and throws an error if pos doesn't produce one in that timeframe. generation indicates how "late" in a usual run of @check the example might have been generated.
Usage:
julia> using Supposition, Supposition.Data
 
 julia> example(Data.Integers(0, 10))
-7
source
Supposition.example — Method
example(gen::Possibility, n::Integer; tries=100_000)
Generate n examples for the given Possibility. Each example is given tries attempts to generate. If any fail, the entire process is aborted.
julia> using Supposition, Supposition.Data
+7
source
Supposition.example — Method
example(gen::Possibility, n::Integer; tries=100_000)
Generate n examples for the given Possibility. Each example is given tries attempts to generate. If any fail, the entire process is aborted.
julia> using Supposition, Supposition.Data
 
 julia> is = Data.Integers(0, 10);
 
@@ -186,4 +186,4 @@
   6
  10
   1
-  8
source
Supposition.find_user_error_frame — Function
find_user_error_frame(err, trace)
Try to heuristically guess where an error was actually coming from.
For example, ErrorException is (generally) thrown from the error function, which would always report the same location if we'd naively take the first frame of the trace. This tries to be a bit smarter (but still fairly conservative) and return something other than the first frame for a small number of known error-throwing functions.
source
Supposition.find_user_stack_depth — Method
find_user_stack_depth
Return a heuristic guess for how many functions deep in user code an error was thrown. Falls back to the full length of the stacktrace.
source
Supposition.forced_choice! — Method
forced_choice(tc::TestCase, n::UInt64)
Insert a definite choice in the choice sequence.
Note that all integrity checks happen here!
source
Supposition.reject! — Method
reject!()
Reject the current testcase as invalid, meaning the generated example should not be considered as producing a valid counterexample.
Callability
This can only be called while a testcase is currently being examined or an example for a Possibility is being actively generated. It is ok to call this inside of @composed or @check, as well as any functions only intended to be called from one of those places.
source
Supposition.run — Method
run(ts::TestState)
Run the checking algorithm on ts, generating values until we should stop, targeting the score we want to target on and finally shrinking the result.
source
Supposition.should_keep_generating — Method
should_keep_generating(ts::TestState)
Whether ts should keep generating new test cases, or whether ts is finished.
true returned here means that the given property is not trivial, there is no result yet and we have room for more examples.
source
Supposition.shrink_redistribute — Method
shrink_redistribute(ts::TestState, attempt::Attempt, k::UInt)
Try to shrink attempt by redistributing value between two elements length k apart.
source
Supposition.shrink_sort — Method
shrink_sort(::TestState, attempt::Attempt, k::UInt)
Try to shrink attempt by sorting k contiguous elements at a time.
source
Supposition.shrink_swap — Method
shrink_swap(::TestState, attempt::Attempt, k::UInt)
Try to shrink attempt by swapping two elements length k apart.
source
Supposition.shrink_zeros — Method
shrink_zeros(::TestSTate, attempt::Attempt, k::UInt)
Try to shrink attempt by setting k elements at a time to zero.
source
Supposition.target! — Method
target!(score)
Update the currently running testcase to track the given score as its target.
score must be convertible to a Float64.
Multiple Updates
This score can only be set once! Repeated calls will be ignored.
Callability
This can only be called while a testcase is currently being examined or an example for a Possibility is being actively generated. It is ok to call this inside of @composed or @check, as well as any functions only intended to be called from one of those places.
source
Supposition.target! — Method
target!(tc::TestCase, score::Float64)
Update tc to use score as the score this TestCase achieves during optimization.
Multiple Updates
This score can only be set once! Repeated calls will be ignored.
source
Supposition.target! — Method
target!(ts::TestState)
If ts has a target to go towards set, this will try to climb towards that target by adjusting the choice sequence until ts shouldn't generate anymore.
If ts is currently tracking an error it encountered, it will try to minimize the stacktrace there instead.
source
Supposition.tear — Method
tear(x::T) where T <: Union{Float16, Float32, Float64} -> Tuple{I, I, I}
Returns the sign, exponent and fractional parts of a floating point number. The returned tuple consists of three unsigned integer types I of the same bitwidth as T.
source
Supposition.test_function — Method
test_function(ts::TestState, tc::TestCase)
Test the function given to ts on the test case tc.
Returns a NTuple{Bool, 2} indicating whether tc is interesting and whether it is "better" than the previously best recorded example in ts.
source
Supposition.windows — Method
windows(array, a, b)
Split array into three windows, with split points at a and b. The split points belong to the middle window.
source
Supposition.BiasedNumbers — Type
BiasedNumbers(weights::Vector{Float64})
Sample the numbers from 1:length(weights), each with a weight of weights[i].
The weights may be any positive number.
source
Supposition.CheckConfig — Type
CheckConfig(;options...)
A struct holding the initial configuration for an invocation of @check.
Options:
  • rng: The initial RNG object given to @check. Defaults to a copyable Random.AbstractRNG.
  • max_examples: The maximum number of examples allowed to be drawn with this config. -1 means infinite drawing (careful!). Defaults to 10_000.
  • record: Whether the result should be recorded in the parent testset, if there is one. Defaults to true.
  • verbose: Whether the printing should be verbose, i.e. print even if it's a Pass. Defaults to false.
  • broken: Whether the invocation is expected to fail. Defaults to false.
  • buffer_size: The default maximum buffer size to use for a test case. Defaults to 100_000.
Buffer Size
At any one point, there may be more than one active buffer being worked on. You can try to increase this value when you encounter a lot of Overrun. Do not set this too large, or you're very likely to run out of memory; the default results in ~800kB worth of choices being possible, which should be plenty for most fuzzing tasks. It's generally unlikely that failures only occur with very large values here, and not with smaller ones.
source
Supposition.Composed — Type
Composed{S,T} <: Possibility{T}
A Possibility composed from multiple different Possibility through @composed. A tiny bit more fancy/convenient compared to map if multiple Possibility are required to be mapped over at the same time.
Should not be instantiated manually; keep the object returned by @composed around instead.
source
Supposition.Error — Type
Error
A result indicating that an error was encountered while generating or shrinking.
source
Supposition.TestCase — Type
TestCase
A struct representing a single (ongoing) test case.
  • prefix: A fixed set of choices that must be made first.
  • rng: The RNG this testcase ultimately uses to draw from. This is used to seed the        task-local RNG object before generating begins.
  • generation: The "generation" this TestCase was made in. Can be used for determining how far along in the generation process we are (higher is further).
  • max_generation: The maximum "generation" this TestCase could have been made in. Does not necessarily exist.
  • max_size: The maximum number of choices this TestCase is allowed to make.
  • choices: The binary choices made so far.
  • targeting_score: The score this TestCase attempts to maximize.
source
Supposition.TestState — Type
TestState
  • config: The configuration this TestState is running with
  • is_interesting: The user given property to investigate
  • rng: The currently used RNG
  • valid_test_cases: The count of (so far) valid encountered testcases
  • calls: The number of times is_interesting was called in total
  • result: The choice sequence leading to a non-throwing counterexample
  • best_scoring: The best scoring result that was encountered during targeting
  • target_err: The error this test has previously encountered and the smallest choice sequence leading to it
  • error_cache: A cache of errors encountered during shrinking that were not of the same type as the first found one, or are from a different location
  • test_is_trivial: Whether is_interesting is trivial, i.e. led to no choices being required
  • previous_example: The previously recorded attempt (if any).
source
Supposition.CURRENT_TESTCASE — Constant
CURRENT_TESTCASE
A ScopedValue containing the currently active test case. Intended for use in user-facing functions like target! or assume! that need access to the current testcase, but shouldn't require it as an argument to make the API more user friendly.
Not intended for user-side access, thus considered internal and not supported under semver.
source
Supposition.DEFAULT_CONFIG — Constant
DEFAULT_CONFIG
A ScopedValue holding the CheckConfig that will be used by default & as a fallback.
Currently uses these values:
  • rng: Random.Xoshiro(rand(Random.RandomDevice(), UInt))
  • max_examples: 10_000
  • record: true
  • verbose: false
  • broken: false
  • buffer_size: 100_000
@check will use a new instance of Random.Xoshiro by itself.
source
Supposition.MESSAGE_BASED_ERROR — Type
MESSAGE_BASED_ERROR
A Union of some some in Base that are known to contain only the field :msg.
If you're using one of these errors and require specialized shrinking on them, define a custom exception type and throw that instead of overriding err_less. The definition of err_less for these types is written for the most generality, not perfect accuracy.
Unstable
This heavily relies on internals of Base, and may break & change in future versions. THIS IS NOT SUPPORTED API.
source

+  8
source
Supposition.find_user_error_frame — Function
find_user_error_frame(err, trace)

Try to heuristically guess where an error was actually coming from.

For example, ErrorException is (generally) thrown from the error function, which would always report the same location if we'd naively take the first frame of the trace. This tries to be a bit smarter (but still fairly conservative) and return something other than the first frame for a small number of known error-throwing functions.

source
Supposition.find_user_stack_depth — Method
find_user_stack_depth

Return a heuristic guess for how many functions deep in user code an error was thrown. Falls back to the full length of the stacktrace.

source
Supposition.forced_choice! — Method
forced_choice(tc::TestCase, n::UInt64)

Insert a definite choice in the choice sequence.

Note that all integrity checks happen here!

source
Supposition.reject! — Method
reject!()

Reject the current testcase as invalid, meaning the generated example should not be considered as producing a valid counterexample.

Callability

This can only be called while a testcase is currently being examined or an example for a Possibility is being actively generated. It is ok to call this inside of @composed or @check, as well as any functions only intended to be called from one of those places.

source
Supposition.run — Method
run(ts::TestState)

Run the checking algorithm on ts, generating values until we should stop, targeting the score we want to target on and finally shrinking the result.

source
Supposition.should_keep_generating — Method
should_keep_generating(ts::TestState)

Whether ts should keep generating new test cases, or whether ts is finished.

true returned here means that the given property is not trivial, there is no result yet and we have room for more examples.

source
Supposition.shrink_redistribute — Method
shrink_redistribute(ts::TestState, attempt::Attempt, k::UInt)

Try to shrink attempt by redistributing value between two elements length k apart.

source
Supposition.shrink_sort — Method
shrink_sort(::TestState, attempt::Attempt, k::UInt)

Try to shrink attempt by sorting k contiguous elements at a time.

source
Supposition.shrink_swap — Method
shrink_swap(::TestState, attempt::Attempt, k::UInt)

Try to shrink attempt by swapping two elements length k apart.

source
Supposition.shrink_zeros — Method
shrink_zeros(::TestSTate, attempt::Attempt, k::UInt)

Try to shrink attempt by setting k elements at a time to zero.

source
Supposition.target! — Method
target!(score)

Update the currently running testcase to track the given score as its target.

score must be convertible to a Float64.

Multiple Updates

This score can only be set once! Repeated calls will be ignored.

Callability

This can only be called while a testcase is currently being examined or an example for a Possibility is being actively generated. It is ok to call this inside of @composed or @check, as well as any functions only intended to be called from one of those places.

source
Supposition.target! — Method
target!(tc::TestCase, score::Float64)

Update tc to use score as the score this TestCase achieves during optimization.

Multiple Updates

This score can only be set once! Repeated calls will be ignored.

source
Supposition.target! — Method
target!(ts::TestState)

If ts has a target to go towards set, this will try to climb towards that target by adjusting the choice sequence until ts shouldn't generate anymore.

If ts is currently tracking an error it encountered, it will try to minimize the stacktrace there instead.

source
Supposition.tear — Method
tear(x::T) where T <: Union{Float16, Float32, Float64} -> Tuple{I, I, I}

Returns the sign, exponent and fractional parts of a floating point number. The returned tuple consists of three unsigned integer types I of the same bitwidth as T.

source
Supposition.test_function — Method
test_function(ts::TestState, tc::TestCase)

Test the function given to ts on the test case tc.

Returns a NTuple{Bool, 2} indicating whether tc is interesting and whether it is "better" than the previously best recorded example in ts.

source
Supposition.windows — Method
windows(array, a, b)

Split array into three windows, with split points at a and b. The split points belong to the middle window.

source
Supposition.BiasedNumbers — Type
BiasedNumbers(weights::Vector{Float64})

Sample the numbers from 1:length(weights), each with a weight of weights[i].

The weights may be any positive number.

source
Supposition.CheckConfig — Type
CheckConfig(;options...)

A struct holding the initial configuration for an invocation of @check.

Options:

  • rng: The initial RNG object given to @check. Defaults to a copyable Random.AbstractRNG.
  • max_examples: The maximum number of examples allowed to be drawn with this config. -1 means infinite drawing (careful!). Defaults to 10_000.
  • record: Whether the result should be recorded in the parent testset, if there is one. Defaults to true.
  • verbose: Whether the printing should be verbose, i.e. print even if it's a Pass. Defaults to false.
  • broken: Whether the invocation is expected to fail. Defaults to false.
  • buffer_size: The default maximum buffer size to use for a test case. Defaults to 100_000.
Buffer Size

At any one point, there may be more than one active buffer being worked on. You can try to increase this value when you encounter a lot of Overrun. Do not set this too large, or you're very likely to run out of memory; the default results in ~800kB worth of choices being possible, which should be plenty for most fuzzing tasks. It's generally unlikely that failures only occur with very large values here, and not with smaller ones.

source
Supposition.Composed — Type
Composed{S,T} <: Possibility{T}

A Possibility composed from multiple different Possibility through @composed. A tiny bit more fancy/convenient compared to map if multiple Possibility are required to be mapped over at the same time.

Should not be instantiated manually; keep the object returned by @composed around instead.

source
Supposition.Error — Type
Error

A result indicating that an error was encountered while generating or shrinking.

source
Supposition.TestCase — Type
TestCase

A struct representing a single (ongoing) test case.

  • prefix: A fixed set of choices that must be made first.
  • rng: The RNG this testcase ultimately uses to draw from. This is used to seed the task-local RNG object before generating begins.
  • generation: The "generation" this TestCase was made in. Can be used for determining how far along in the generation process we are (higher is further).
  • max_generation: The maximum "generation" this TestCase could have been made in. Does not necessarily exist.
  • max_size: The maximum number of choices this TestCase is allowed to make.
  • choices: The binary choices made so far.
  • targeting_score: The score this TestCase attempts to maximize.
source
Supposition.TestState — Type
TestState
  • config: The configuration this TestState is running with
  • is_interesting: The user given property to investigate
  • rng: The currently used RNG
  • valid_test_cases: The count of (so far) valid encountered testcases
  • calls: The number of times is_interesting was called in total
  • result: The choice sequence leading to a non-throwing counterexample
  • best_scoring: The best scoring result that was encountered during targeting
  • target_err: The error this test has previously encountered and the smallest choice sequence leading to it
  • error_cache: A cache of errors encountered during shrinking that were not of the same type as the first found one, or are from a different location
  • test_is_trivial: Whether is_interesting is trivial, i.e. led to no choices being required
  • previous_example: The previously recorded attempt (if any).
source
Supposition.CURRENT_TESTCASE — Constant
CURRENT_TESTCASE

A ScopedValue containing the currently active test case. Intended for use in user-facing functions like target! or assume! that need access to the current testcase, but shouldn't require it as an argument to make the API more user friendly.

Not intended for user-side access, thus considered internal and not supported under semver.

source
Supposition.DEFAULT_CONFIG — Constant
DEFAULT_CONFIG

A ScopedValue holding the CheckConfig that will be used by default & as a fallback.

Currently uses these values:

  • rng: Random.Xoshiro(rand(Random.RandomDevice(), UInt))
  • max_examples: 10_000
  • record: true
  • verbose: false
  • broken: false
  • buffer_size: 100_000

@check will use a new instance of Random.Xoshiro by itself.

source
Supposition.MESSAGE_BASED_ERROR — Type
MESSAGE_BASED_ERROR

A Union of some some in Base that are known to contain only the field :msg.

If you're using one of these errors and require specialized shrinking on them, define a custom exception type and throw that instead of overriding err_less. The definition of err_less for these types is written for the most generality, not perfect accuracy.

Unstable

This heavily relies on internals of Base, and may break & change in future versions. THIS IS NOT SUPPORTED API.

source
diff --git a/dev/benchmarks.html b/dev/benchmarks.html index f838c12..087a601 100644 --- a/dev/benchmarks.html +++ b/dev/benchmarks.html @@ -199,4 +199,4 @@ └ @ Supposition ~/Documents/projects/Supposition.jl/src/testset.jl:280 Test Summary: | Fail Total isempty | 1 1 - 0.412517 seconds (562.41 k allocations: 658.063 MiB, 5.59% gc time, 4.44% compilation time: 2% of which was recompilation)

Conclusion

If you've read down to here, I don't think I even have to write it out - Supposition.jl is fast! I feel pretty confident saying that it's unlikely to be the bottleneck of a testsuite. All of that without even explicitly looking for places to optimize the package yet. Of course, this doesn't even touch cranking up the number of samples Supposition.jl tries, or any form of memoization on the property you could quite easily add. So there is potential for going faster in the future.

Go and incorporate fuzzing into your testsuite ;)

+ 0.412517 seconds (562.41 k allocations: 658.063 MiB, 5.59% gc time, 4.44% compilation time: 2% of which was recompilation)

Conclusion

If you've read down to here, I don't think I even have to write it out - Supposition.jl is fast! I feel pretty confident saying that it's unlikely to be the bottleneck of a testsuite. All of that without even explicitly looking for places to optimize the package yet. Of course, this doesn't even touch cranking up the number of samples Supposition.jl tries, or any form of memoization on the property you could quite easily add. So there is potential for going faster in the future.

Go and incorporate fuzzing into your testsuite ;)

diff --git a/dev/faq.html b/dev/faq.html index 2623c78..4fc0820 100644 --- a/dev/faq.html +++ b/dev/faq.html @@ -1,2 +1,2 @@ -FAQ · Supposition.jl Documentation
GitHub

FAQ

Why write a new package? What about PropCheck.jl?

PropCheck.jl is based on the Haskell library Hedgehog, while Supposition.jl is based on Hypothesis. For a detailed look into the differences between these (as well as QuickCheck), I've written up a small comparison on my blog. Some understanding of property based testing is required, but the TL;DR is that the approaches taken by these two frameworks are fundamentally different.

Originally, I was planning on only investigating what Hypothesis did differently from Hedgehog and incorporating the results of that investigation into PropCheck.jl, but once I learned how different the approaches truly are, I quickly realized that marrying the two would be more work and likely less fruitful than just porting Hypothesis directly. My resolve in that regard had only grown stronger after porting MiniThesis to Julia, which this package is ultimately also based on. So far, I have found the core of the package to be extremely solid, and I don't expect that to change.

Some of the upsides I've noticed while using Supposition.jl so far is that it's much, MUCH easier to wrap your head around than PropCheck.jl ever was. Even after working on & thinking about Hedgehog & PropCheck.jl for more than 4 years, I still get lost in its internals. I don't see that happening with Supposition.jl; I can confidently say that I am (for the moment) able to keep the entire package in my head. Another big upside is that, as far as I can tell, Supposition.jl is much faster than PropCheck.jl, even after the latter received extensive type stability analysis and performance improvements out of necessity. I haven't done the same for Supposition.jl so far - be sure to check out the Benchmarks section for a direct comparison. Of course, only part of this is due to the underlying approach of Hypothesis vs. Hedgehog. Sticking to a much more functional & function-based implementation with PropCheck.jl is sure to hold the package back, and perhaps the situation would be different with a more data-oriented approach.

What can Supposition.jl do that PropCheck.jl can't?

While there is a big overlap in capabilities between the two, there are a number of things that Supposition.jl can very easily do that would require a major rework of the internals of PropCheck.jl. Here's a small (incomplete) list:

  • Shrink examples that lead to an error
  • Easily use temporal & stateful property tests
  • Reproducibly replay previously found counterexamples (with caveats regarding external state)
  • Generate values based on the values that were put into a test, and have those values in turn shrink just as well as the values that were put in while preserving the invariants they were generated under.

What feature X of PropCheck.jl corresponds to feature Y of Supposition.jl?

The following is a short overview/feature comparison between PropCheck.jl and Supposition.jl. It may not be a perfect match for all functionality - be sure to check the documentation of each respective feature to learn about their minute differences!

FeaturePropCheck.jlSupposition.jl
Checking Interfacecheck(<prop>, <AbstractIntegrated>)@check prop(<Data.Possibility>) or @check function prop(arg=<Data.Possibility>, ...) # ...use args... end
mapmap(<func>, <AbstractIntegrated>)map(<func>, <Data.Possibility>)
filterfilter(<pred>, <AbstractIntegrated>)filter(<pred>, <Data.Possibility>)
composition through combinationinterleave(integ::AbstractIntegrated...)@composed function comp(a=<Data.Possibility>, ...) # ...use args... end
VectorsPropCheck.vector(len::AbstractIntegrated, objs::AbstractIntegrated)`Data.Vectors(objs::Data.Possibility; minsize=0, maxsize=...)
TuplesPropCheck.tuple(len::AbstractIntegrated, objs::AbstractIntegrated)Currently unsupported, but could be added in a PR
IntegersPropCheck.inegint/PropCheck.iposintData.Integers(min, max)
Floating pointPropCheck.ifloat(T) and its variantsData.Floats{T}(; infs=<Bool>, nans=<Bool>)
StringsPropCheck.str(len::AbstractIntegrated, alphabet::AbstractIntegrated)Data.Text(::Possibility{Char}; min_len=0, max_len=...)
Stateful generationIntegratedOnceUnsupported due to deterministic replaying of finite generators being tricky
IntegratedFiniteIteratorUnsupported due to deterministic replaying of finite generators being tricky
IntegratedLengthBoundedUnsupported due to deterministic replaying of finite generators being tricky
IntegratedChainUnsupported due to deterministic replaying of finite generators being tricky
PropCheck.iuniqueUnsupported due to deterministic replaying of finite generators being tricky
Generation of constant dataPropCheck.iconst(x)Data.Just(x)
Generation from CollectionsIntegratedRange(x)/PropCheck.isampleData.SampledFrom(x)
Generation of shrinkable constantsIntegratedVal(x)Unsupported until custom shrinking functions are added, see #25
Type-based generationPropCheck.itypeUnsupported for now, see #21 for more information (it's coming though! And smarter than PropCheck.jl too ;) ).
+FAQ · Supposition.jl Documentation
GitHub

FAQ

Why write a new package? What about PropCheck.jl?

PropCheck.jl is based on the Haskell library Hedgehog, while Supposition.jl is based on Hypothesis. For a detailed look into the differences between these (as well as QuickCheck), I've written up a small comparison on my blog. Some understanding of property based testing is required, but the TL;DR is that the approaches taken by these two frameworks are fundamentally different.

Originally, I was planning on only investigating what Hypothesis did differently from Hedgehog and incorporating the results of that investigation into PropCheck.jl, but once I learned how different the approaches truly are, I quickly realized that marrying the two would be more work and likely less fruitful than just porting Hypothesis directly. My resolve in that regard had only grown stronger after porting MiniThesis to Julia, which this package is ultimately also based on. So far, I have found the core of the package to be extremely solid, and I don't expect that to change.

Some of the upsides I've noticed while using Supposition.jl so far is that it's much, MUCH easier to wrap your head around than PropCheck.jl ever was. Even after working on & thinking about Hedgehog & PropCheck.jl for more than 4 years, I still get lost in its internals. I don't see that happening with Supposition.jl; I can confidently say that I am (for the moment) able to keep the entire package in my head. Another big upside is that, as far as I can tell, Supposition.jl is much faster than PropCheck.jl, even after the latter received extensive type stability analysis and performance improvements out of necessity. I haven't done the same for Supposition.jl so far - be sure to check out the Benchmarks section for a direct comparison. Of course, only part of this is due to the underlying approach of Hypothesis vs. Hedgehog. Sticking to a much more functional & function-based implementation with PropCheck.jl is sure to hold the package back, and perhaps the situation would be different with a more data-oriented approach.

What can Supposition.jl do that PropCheck.jl can't?

While there is a big overlap in capabilities between the two, there are a number of things that Supposition.jl can very easily do that would require a major rework of the internals of PropCheck.jl. Here's a small (incomplete) list:

  • Shrink examples that lead to an error
  • Easily use temporal & stateful property tests
  • Reproducibly replay previously found counterexamples (with caveats regarding external state)
  • Generate values based on the values that were put into a test, and have those values in turn shrink just as well as the values that were put in while preserving the invariants they were generated under.

What feature X of PropCheck.jl corresponds to feature Y of Supposition.jl?

The following is a short overview/feature comparison between PropCheck.jl and Supposition.jl. It may not be a perfect match for all functionality - be sure to check the documentation of each respective feature to learn about their minute differences!

FeaturePropCheck.jlSupposition.jl
Checking Interfacecheck(<prop>, <AbstractIntegrated>)@check prop(<Data.Possibility>) or @check function prop(arg=<Data.Possibility>, ...) # ...use args... end
mapmap(<func>, <AbstractIntegrated>)map(<func>, <Data.Possibility>)
filterfilter(<pred>, <AbstractIntegrated>)filter(<pred>, <Data.Possibility>)
composition through combinationinterleave(integ::AbstractIntegrated...)@composed function comp(a=<Data.Possibility>, ...) # ...use args... end
VectorsPropCheck.vector(len::AbstractIntegrated, objs::AbstractIntegrated)`Data.Vectors(objs::Data.Possibility; minsize=0, maxsize=...)
TuplesPropCheck.tuple(len::AbstractIntegrated, objs::AbstractIntegrated)Currently unsupported, but could be added in a PR
IntegersPropCheck.inegint/PropCheck.iposintData.Integers(min, max)
Floating pointPropCheck.ifloat(T) and its variantsData.Floats{T}(; infs=<Bool>, nans=<Bool>)
StringsPropCheck.str(len::AbstractIntegrated, alphabet::AbstractIntegrated)Data.Text(::Possibility{Char}; min_len=0, max_len=...)
Stateful generationIntegratedOnceUnsupported due to deterministic replaying of finite generators being tricky
IntegratedFiniteIteratorUnsupported due to deterministic replaying of finite generators being tricky
IntegratedLengthBoundedUnsupported due to deterministic replaying of finite generators being tricky
IntegratedChainUnsupported due to deterministic replaying of finite generators being tricky
PropCheck.iuniqueUnsupported due to deterministic replaying of finite generators being tricky
Generation of constant dataPropCheck.iconst(x)Data.Just(x)
Generation from CollectionsIntegratedRange(x)/PropCheck.isampleData.SampledFrom(x)
Generation of shrinkable constantsIntegratedVal(x)Unsupported until custom shrinking functions are added, see #25
Type-based generationPropCheck.itypeUnsupported for now, see #21 for more information (it's coming though! And smarter than PropCheck.jl too ;) ).
diff --git a/dev/index.html b/dev/index.html index f4fdac9..36a4969 100644 --- a/dev/index.html +++ b/dev/index.html @@ -1,2 +1,2 @@ -Main Page · Supposition.jl Documentation
GitHub

Supposition.jl Documentation

This is the documentation for Supposition.jl, a property based testing framework inspired by Hypothesis.

It features choice-sequence based generation & shrinking of examples, which can smartly shrink initial failures to smaller example while preserving the invariants the original input was generated under. It's also easy to combine generators into new generators.

Check out the Examples in the sidebar to get an introduction to property based testing and to learn how to write your own tests!

Here's also a sitemap for the rest of the documentation:

Goals

  • Good performance
    • A test framework should not be the bottleneck of the testsuite.
  • Composability
    • It should not be required to modify an existing codebase to accomodate Supposition.jl
    • However, for exploratory fuzzing it may be advantageous to insert small markers into a codebase
  • Reusability
    • It should be easily possible to reuse large parts of existing definitions (functions/structs) to build custom generators
  • Repeatability
    • It should be possible to replay previous (failing) examples and reproduce the sequence of steps taken exactly. The only cases where this isn't going to work is if your code relies on external state, such as querying a hardware RNG for random data or similar objects that are not under the control of the testing framework itself (such as the capacity of your harddrive, for example).
  • Discoverability (of API boundaries)
    • Supposition.jl should be easy to use to find the actual API boundaries of a given function, if that is not yet known or not sufficiently specified in the docstring of a function. It should be enough to know the argument types to start fuzzing a function (at least in the simplest sense of "does it error").
  • Ease of Use
    • It should be relatively straightforward to write custom generators.

Limitations

  • Due to its nature as a fuzzing framework and the (usually) huge associated statespace, Supposition.jl cannot give a formal proof of correctness. It's only an indicator (but a pretty good one).
+Main Page · Supposition.jl Documentation
GitHub

Supposition.jl Documentation

This is the documentation for Supposition.jl, a property based testing framework inspired by Hypothesis.

It features choice-sequence based generation & shrinking of examples, which can smartly shrink initial failures to smaller example while preserving the invariants the original input was generated under. It's also easy to combine generators into new generators.

Check out the Examples in the sidebar to get an introduction to property based testing and to learn how to write your own tests!

Here's also a sitemap for the rest of the documentation:

Goals

  • Good performance
    • A test framework should not be the bottleneck of the testsuite.
  • Composability
    • It should not be required to modify an existing codebase to accomodate Supposition.jl
    • However, for exploratory fuzzing it may be advantageous to insert small markers into a codebase
  • Reusability
    • It should be easily possible to reuse large parts of existing definitions (functions/structs) to build custom generators
  • Repeatability
    • It should be possible to replay previous (failing) examples and reproduce the sequence of steps taken exactly. The only cases where this isn't going to work is if your code relies on external state, such as querying a hardware RNG for random data or similar objects that are not under the control of the testing framework itself (such as the capacity of your harddrive, for example).
  • Discoverability (of API boundaries)
    • Supposition.jl should be easy to use to find the actual API boundaries of a given function, if that is not yet known or not sufficiently specified in the docstring of a function. It should be enough to know the argument types to start fuzzing a function (at least in the simplest sense of "does it error").
  • Ease of Use
    • It should be relatively straightforward to write custom generators.

Limitations

  • Due to its nature as a fuzzing framework and the (usually) huge associated statespace, Supposition.jl cannot give a formal proof of correctness. It's only an indicator (but a pretty good one).
diff --git a/dev/interfaces.html b/dev/interfaces.html index f955570..5a3e874 100644 --- a/dev/interfaces.html +++ b/dev/interfaces.html @@ -14,7 +14,7 @@ # use a custom Xoshiro instance julia> Supposition.@check rng=Xoshiro(1234) function foo(a = Data.Text(Data.Characters(); max_len=10)) length(a) > 8 - end
Hardware RNG

Be aware that you cannot pass a hardware RNG to @check directly. If you want to randomize based on hardware entropy, seed a copyable RNG like Xoshiro from your hardware RNG and pass that to @check instead. The RNG needs to be copyable for reproducibility.

source
Supposition.@composed — Macro
@composed

A way to compose multiple Possibility into one, by applying a function.

The return type is inferred as a best-effort!

Used like so:

julia> using Supposition, Supposition.Data
+       end
Hardware RNG

Be aware that you cannot pass a hardware RNG to @check directly. If you want to randomize based on hardware entropy, seed a copyable RNG like Xoshiro from your hardware RNG and pass that to @check instead. The RNG needs to be copyable for reproducibility.

source
Supposition.@composed — Macro
@composed

A way to compose multiple Possibility into one, by applying a function.

The return type is inferred as a best-effort!

Used like so:

julia> using Supposition, Supposition.Data
 
 julia> text = Data.Text(Data.AsciiCharacters(); max_len=10)
 
@@ -23,7 +23,7 @@
        end
 
 julia> example(gen)
-" 8:  giR2YL\rl"
source

API for controlling fuzzing

These functions are intended for usage while testing, having various effects on the shrinking/fuzzing process. They are not intended to be part of a codebase permanently/in production.

The trailing exclamation mark serves as a reminder that this will, under the hood, modify the currently running testcase.

Supposition.target! — Method
target!(score)

Update the currently running testcase to track the given score as its target.

score must be convertible to a Float64.

Multiple Updates

This score can only be set once! Repeated calls will be ignored.

Callability

This can only be called while a testcase is currently being examined or an example for a Possibility is being actively generated. It is ok to call this inside of @composed or @check, as well as any functions only intended to be called from one of those places.

source
Supposition.assume! — Method
assume!(precondition::Bool)

If this precondition is not met, abort the test and mark the currently running testcase as invalid.

Callability

This can only be called while a testcase is currently being examined or an example for a Possibility is being actively generated. It is ok to call this inside of @composed or @check, as well as any functions only intended to be called from one of those places.

source
Supposition.Data.produce! — Method
produce!(p::Possibility{T}) -> T

Produces a value from the given Possibility, recording the required choices in the currently active TestCase.

Callability

This can only be called while a testcase is currently being examined or an example for a Possibility is being actively generated. It is ok to call this inside of @composed or @check, as well as any functions only intended to be called from one of those places.

source
Supposition.reject! — Function
reject!()

Reject the current testcase as invalid, meaning the generated example should not be considered as producing a valid counterexample.

Callability

This can only be called while a testcase is currently being examined or an example for a Possibility is being actively generated. It is ok to call this inside of @composed or @check, as well as any functions only intended to be called from one of those places.

source
Supposition.err_less — Function
err_less(e1::E, e2::E) where E

A comparison function for exceptions, used when encountering an error in a property. Returns true if e1 is considered to be "easier" or "simpler" than e2. Only definable when both e1 and e2 have the same type.

This is optional to implement, but may be beneficial for shrinking counterexamples leading to an error with rich metadata, in which case err_less will be used to compare errors of the same type from different counterexamples. In particular, this function will likely be helpful for errors with metadata that is far removed from the input that caused the error itself, but would nevertheless be helpful when investigating the failure.

Coincidental Errors

There may also be situations where defining err_less won't help to find a smaller counterexample if the cause of the error is unrelated to the choices taken during generation. For instance, this is the case when there is no network connection and a Sockets.DNSError is thrown during the test, or there is a network connection but the host your program is trying to connect to does not have an entry in DNS.

source
Supposition.DEFAULT_CONFIG — Constant
DEFAULT_CONFIG

A ScopedValue holding the CheckConfig that will be used by default & as a fallback.

Currently uses these values:

  • rng: Random.Xoshiro(rand(Random.RandomDevice(), UInt))
  • max_examples: 10_000
  • record: true
  • verbose: false
  • broken: false
  • buffer_size: 100_000

@check will use a new instance of Random.Xoshiro by itself.

source

Available Possibility

The Data module contains most everyday objects you're going to use when writing property based tests with Supposition.jl. For example, the basic generators for integers, strings, floating point values etc. are defined here. Everything listed in this section is considered supported under semver.

Functions

Base.:| — Method
|(::Possibility{T}, ::Possibility{S}) where {T,S} -> OneOf{Union{T,S}}

Combine two Possibility into one, sampling uniformly from either.

If either of the two arguments is a OneOf, the resulting object acts as if all original non-OneOf had be given to OneOf instead. That is, e.g. OneOf(a, b) | c will act like OneOf(a,b,c).

See also OneOf.

source
Base.filter — Method
filter(f, pos::Possibility)

Filter the output of produce! on pos by applying the predicate f.

No stalling

In order not to stall generation of values, this will not try to produce a value from pos forever, but reject the testcase after some attempts.

source
Base.map — Method
map(f, pos::Possibility)

Apply f to the result of calling produce! on pos (lazy mapping).

Equivalent to calling Map(pos, f).

See also Map.

source
Supposition.Data.BitIntegers — Method
BitIntegers() <: Possibility{Union{Int128, Int16, Int32, Int64, Int8, UInt128, UInt16, UInt32, UInt64, UInt8}}

A Possibility for generating all possible bitintegers with fixed size.

source
Supposition.Data.bind — Method
bind(f, pos::Possibility)

Maps the output of produce! on pos through f, and calls produce! on the result again. f is expected to take a value and return a Possibility.

Equivalent to calling Bind(pos, f).

See also Bind.

source
Supposition.Data.postype — Method
postype(::P) where P <: Possibility

Gives the type of objects this Possibility object will generate.

source
Supposition.Data.postype — Method
postype(::Type{P<:Possibility})

Gives the type of objects this Possibility type will generate.

source
Supposition.Data.recursive — Method
recursive(f, pos::Possibility; max_layers=5)

Recursively expand pos into deeper nested Possibility by repeatedly passing pos itself to f. f returns a new Possibility, which is then passed into f again until the maximum depth is achieved.

Equivalent to calling Recursive(pos, f).

See also Recursive.

source

Types

Supposition.Data.AsciiCharacters — Type
AsciiCharacters() <: Possibility{Char}

A Possibility of producing arbitrary Char instances that are isascii. More efficient than filtering Characters.

julia> using Supposition
+" 8:  giR2YL\rl"
source

API for controlling fuzzing

These functions are intended for usage while testing, having various effects on the shrinking/fuzzing process. They are not intended to be part of a codebase permanently/in production.

The trailing exclamation mark serves as a reminder that this will, under the hood, modify the currently running testcase.

Supposition.target! — Method
target!(score)

Update the currently running testcase to track the given score as its target.

score must be convertible to a Float64.

Multiple Updates

This score can only be set once! Repeated calls will be ignored.

Callability

This can only be called while a testcase is currently being examined or an example for a Possibility is being actively generated. It is ok to call this inside of @composed or @check, as well as any functions only intended to be called from one of those places.

source
Supposition.assume! — Method
assume!(precondition::Bool)

If this precondition is not met, abort the test and mark the currently running testcase as invalid.

Callability

This can only be called while a testcase is currently being examined or an example for a Possibility is being actively generated. It is ok to call this inside of @composed or @check, as well as any functions only intended to be called from one of those places.

source
Supposition.Data.produce! — Method
produce!(p::Possibility{T}) -> T

Produces a value from the given Possibility, recording the required choices in the currently active TestCase.

Callability

This can only be called while a testcase is currently being examined or an example for a Possibility is being actively generated. It is ok to call this inside of @composed or @check, as well as any functions only intended to be called from one of those places.

source
Supposition.reject! — Function
reject!()

Reject the current testcase as invalid, meaning the generated example should not be considered as producing a valid counterexample.

Callability

This can only be called while a testcase is currently being examined or an example for a Possibility is being actively generated. It is ok to call this inside of @composed or @check, as well as any functions only intended to be called from one of those places.

source
Supposition.err_less — Function
err_less(e1::E, e2::E) where E

A comparison function for exceptions, used when encountering an error in a property. Returns true if e1 is considered to be "easier" or "simpler" than e2. Only definable when both e1 and e2 have the same type.

This is optional to implement, but may be beneficial for shrinking counterexamples leading to an error with rich metadata, in which case err_less will be used to compare errors of the same type from different counterexamples. In particular, this function will likely be helpful for errors with metadata that is far removed from the input that caused the error itself, but would nevertheless be helpful when investigating the failure.

Coincidental Errors

There may also be situations where defining err_less won't help to find a smaller counterexample if the cause of the error is unrelated to the choices taken during generation. For instance, this is the case when there is no network connection and a Sockets.DNSError is thrown during the test, or there is a network connection but the host your program is trying to connect to does not have an entry in DNS.

source
Supposition.DEFAULT_CONFIG — Constant
DEFAULT_CONFIG

A ScopedValue holding the CheckConfig that will be used by default & as a fallback.

Currently uses these values:

  • rng: Random.Xoshiro(rand(Random.RandomDevice(), UInt))
  • max_examples: 10_000
  • record: true
  • verbose: false
  • broken: false
  • buffer_size: 100_000

@check will use a new instance of Random.Xoshiro by itself.

source

Available Possibility

The Data module contains most everyday objects you're going to use when writing property based tests with Supposition.jl. For example, the basic generators for integers, strings, floating point values etc. are defined here. Everything listed in this section is considered supported under semver.

Functions

Base.:| — Method
|(::Possibility{T}, ::Possibility{S}) where {T,S} -> OneOf{Union{T,S}}

Combine two Possibility into one, sampling uniformly from either.

If either of the two arguments is a OneOf, the resulting object acts as if all original non-OneOf had be given to OneOf instead. That is, e.g. OneOf(a, b) | c will act like OneOf(a,b,c).

See also OneOf.

source
Base.filter — Method
filter(f, pos::Possibility)

Filter the output of produce! on pos by applying the predicate f.

No stalling

In order not to stall generation of values, this will not try to produce a value from pos forever, but reject the testcase after some attempts.

source
Base.map — Method
map(f, pos::Possibility)

Apply f to the result of calling produce! on pos (lazy mapping).

Equivalent to calling Map(pos, f).

See also Map.

source
Supposition.Data.BitIntegers — Method
BitIntegers() <: Possibility{Union{Int128, Int16, Int32, Int64, Int8, UInt128, UInt16, UInt32, UInt64, UInt8}}

A Possibility for generating all possible bitintegers with fixed size.

source
Supposition.Data.bind — Method
bind(f, pos::Possibility)

Maps the output of produce! on pos through f, and calls produce! on the result again. f is expected to take a value and return a Possibility.

Equivalent to calling Bind(pos, f).

See also Bind.

source
Supposition.Data.postype — Method
postype(::P) where P <: Possibility

Gives the type of objects this Possibility object will generate.

source
Supposition.Data.postype — Method
postype(::Type{P<:Possibility})

Gives the type of objects this Possibility type will generate.

source
Supposition.Data.recursive — Method
recursive(f, pos::Possibility; max_layers=5)

Recursively expand pos into deeper nested Possibility by repeatedly passing pos itself to f. f returns a new Possibility, which is then passed into f again until the maximum depth is achieved.

Equivalent to calling Recursive(pos, f).

See also Recursive.

source

Types

Supposition.Data.AsciiCharacters — Type
AsciiCharacters() <: Possibility{Char}

A Possibility of producing arbitrary Char instances that are isascii. More efficient than filtering Characters.

julia> using Supposition
 
 julia> ascii = Data.AsciiCharacters()
 
@@ -33,7 +33,7 @@
  'i': ASCII/Unicode U+0069 (category Ll: Letter, lowercase)
  'R': ASCII/Unicode U+0052 (category Lu: Letter, uppercase)
  '\f': ASCII/Unicode U+000C (category Cc: Other, control)
- '>': ASCII/Unicode U+003E (category Sm: Symbol, math)
source
Supposition.Data.Bind — Type
Bind(source::Possibility, f)

Binds f to source, i.e., on produce!(::Bind, ::TestCase) this calls produce! on source, the result of which is passed to f, the output of which will be used as input to produce! again.

In other words, f takes a value produce!d by source and gives back a Possibility that is then immediately produce!d from.

Equivalent to bind(f, source).

source
Supposition.Data.Booleans — Type
Booleans() <: Possibility{Bool}

A Possibility for sampling boolean values.

julia> using Supposition
+ '>': ASCII/Unicode U+003E (category Sm: Symbol, math)
source
Supposition.Data.Bind — Type
Bind(source::Possibility, f)

Binds f to source, i.e., on produce!(::Bind, ::TestCase) this calls produce! on source, the result of which is passed to f, the output of which will be used as input to produce! again.

In other words, f takes a value produce!d by source and gives back a Possibility that is then immediately produce!d from.

Equivalent to bind(f, source).

source
Supposition.Data.Booleans — Type
Booleans() <: Possibility{Bool}

A Possibility for sampling boolean values.

julia> using Supposition
 
 julia> bools = Data.Booleans()
 
@@ -42,7 +42,7 @@
  0
  1
  0
- 1
source
Supposition.Data.Characters — Type
Characters(;valid::Bool = false) <: Possibility{Char}

A Possibility of producing arbitrary Char instances.

Unicode

This will produce! ANY possible Char by default, not just valid unicode codepoints! To only produce valid unicode codepoints, pass valid=true as a keyword argument.

julia> using Supposition
+ 1
source
Supposition.Data.Characters — Type
Characters(;valid::Bool = false) <: Possibility{Char}

A Possibility of producing arbitrary Char instances.

Unicode

This will produce! ANY possible Char by default, not just valid unicode codepoints! To only produce valid unicode codepoints, pass valid=true as a keyword argument.

julia> using Supposition
 
 julia> chars = Data.Characters()
 
@@ -52,12 +52,12 @@
  '𰳍': Unicode U+30CCD (category Lo: Letter, other)
  '\U6ec9c': Unicode U+6EC9C (category Cn: Other, not assigned)
  '\U1a05c5': Unicode U+1A05C5 (category In: Invalid, too high)
- '𓂫': Unicode U+130AB (category Lo: Letter, other)
source
Supposition.Data.Dicts — Type
Dicts(keys::Possibility, values::Possibility; min_size=0, max_size=10_000)

A Possibility for generating Dict objects. The keys are drawn from keys, while the values are drawn from values. min_size/max_size control the number of objects placed into the resulting Dict, respectively.

julia> dicts = Data.Dicts(Data.Integers{UInt8}(), Data.Integers{Int8}(); max_size=3);
+ '𓂫': Unicode U+130AB (category Lo: Letter, other)
source
Supposition.Data.Dicts — Type
Dicts(keys::Possibility, values::Possibility; min_size=0, max_size=10_000)

A Possibility for generating Dict objects. The keys are drawn from keys, while the values are drawn from values. min_size/max_size control the number of objects placed into the resulting Dict, respectively.

julia> dicts = Data.Dicts(Data.Integers{UInt8}(), Data.Integers{Int8}(); max_size=3);
 
 julia> example(dicts)
 Dict{UInt8, Int8} with 2 entries:
   0x54 => -29
-  0x1f => -28
source
Supposition.Data.Floats — Type
Floats{T <: Union{Float16,Float32,Float64}}(;infs=true, nans=true) <: Possibility{T}

A Possibility for sampling floating point values.

The keyword infs controls whether infinities can be generated. nans controls whether any NaN (signaling & quiet) will be generated.

Inf, Nan

This possibility will generate any valid instance, including positive and negative infinities, signaling and quiet NaNs and every possible float.

julia> using Supposition
+  0x1f => -28
source
Supposition.Data.Floats — Type
Floats{T <: Union{Float16,Float32,Float64}}(;infs=true, nans=true) <: Possibility{T}

A Possibility for sampling floating point values.

The keyword infs controls whether infinities can be generated. nans controls whether any NaN (signaling & quiet) will be generated.

Inf, Nan

This possibility will generate any valid instance, including positive and negative infinities, signaling and quiet NaNs and every possible float.

julia> using Supposition
 
 julia> floats = Data.Floats{Float16}()
 
@@ -67,7 +67,7 @@
    1.459e4
    3.277
  NaN
-  -0.0001688
source
Supposition.Data.Floats — Method
Floats(;nans=true, infs=true) <: Possibility{Union{Float64,Float32,Float16}}

A catch-all for generating instances of all three IEEE floating point types.

source
Supposition.Data.Integers — Type
Integers(minimum::T, maximum::T) <: Possibility{T <: Integer}
+  -0.0001688
source
Supposition.Data.Floats — Method
Floats(;nans=true, infs=true) <: Possibility{Union{Float64,Float32,Float16}}

A catch-all for generating instances of all three IEEE floating point types.

source
Supposition.Data.Integers — Type
Integers(minimum::T, maximum::T) <: Possibility{T <: Integer}
 Integers{T}() <: Possibility{T <: Integer}

A Possibility representing drawing integers from [minimum, maximum]. The second constructors draws from the entirety of T.

Produced values are of type T.

julia> using Supposition
 
 julia> is = Data.Integers{Int}()
@@ -78,7 +78,7 @@
   4430062772779972974
     -9995351034504801
   2894734754389242339
- -6640496903289665416
source
Supposition.Data.Just — Type
Just(value::T) <: Possibility{T}

A Possibility that always produces value.

Mutable Data

The source object given to this Just is not copied when produce! is called. Be careful with mutable data!

julia> using Supposition
+ -6640496903289665416
source
Supposition.Data.Just — Type
Just(value::T) <: Possibility{T}

A Possibility that always produces value.

Mutable Data

The source object given to this Just is not copied when produce! is called. Be careful with mutable data!

julia> using Supposition
 
 julia> three = Data.Just(3)
 
@@ -86,14 +86,14 @@
 3-element Vector{Int64}:
  3
  3
- 3
source
Supposition.Data.Map — Type
Map(source::Possibility, f) <: Possibility

A Possibility representing mapping values from source through f.

Equivalent to calling map(f, source).

The pre-calculated return type of Map is a best effort and may be wider than necessary.

julia> using Supposition
+ 3
source
Supposition.Data.Map — Type
Map(source::Possibility, f) <: Possibility

A Possibility representing mapping values from source through f.

Equivalent to calling map(f, source).

The pre-calculated return type of Map is a best effort and may be wider than necessary.

julia> using Supposition
 
 julia> makeeven(x) = (x ÷ 2) * 2
 
 julia> pos = map(makeeven, Data.Integers{Int8}())
 
 julia> all(iseven, example(pos, 10_000))
-true
source
Supposition.Data.OneOf — Type
OneOf(pos::Possibility...) <: Possibility

A Possibility able to generate any of the examples one of the given Possibility can produce. The given Possibility are sampled from uniformly.

At least one Possibility needs to be given to OneOf.

postype(::OneOf) is inferred as a best effort, and may be wider than necessary.

OneOf can also be constructed through use of a | b on Possibility. Constructed in this way, if either a or b is already a OneOf, the resulting OneOf acts as if it had been given the original Possibility objects in the first place. That is, OneOf(a, b) | c acts like OneOf(a, b, c).

julia> of = Data.OneOf(Data.Integers{Int8}(), Data.Integers{UInt8}());
+true
source
Supposition.Data.OneOf — Type
OneOf(pos::Possibility...) <: Possibility

A Possibility able to generate any of the examples one of the given Possibility can produce. The given Possibility are sampled from uniformly.

At least one Possibility needs to be given to OneOf.

postype(::OneOf) is inferred as a best effort, and may be wider than necessary.

OneOf can also be constructed through use of a | b on Possibility. Constructed in this way, if either a or b is already a OneOf, the resulting OneOf acts as if it had been given the original Possibility objects in the first place. That is, OneOf(a, b) | c acts like OneOf(a, b, c).

julia> of = Data.OneOf(Data.Integers{Int8}(), Data.Integers{UInt8}());
 
 julia> Data.postype(of)
 Union{Int8, UInt8}
@@ -106,14 +106,14 @@
 (-83, Int8)
 
 julia> example(ex)
-(0x9f, UInt8)
source
Supposition.Data.Pairs — Type
Pairs(first::Possibility{T}, second::Possibility{S}) where {T,S} <: Possibility{Pair{T,S}}

A Possibility for producing a => b pairs. a is produced by first, b is produced by second.

julia> p = Data.Pairs(Data.Integers{UInt8}(), Data.Floats{Float64}());
+(0x9f, UInt8)
source
Supposition.Data.Pairs — Type
Pairs(first::Possibility{T}, second::Possibility{S}) where {T,S} <: Possibility{Pair{T,S}}

A Possibility for producing a => b pairs. a is produced by first, b is produced by second.

julia> p = Data.Pairs(Data.Integers{UInt8}(), Data.Floats{Float64}());
 
 julia> example(p, 4)
 4-element Vector{Pair{UInt8, Float64}}:
  0x41 => 4.1183566661848205e-230
  0x48 => -2.2653631095108555e-119
  0x2a => -6.564396855333643e224
- 0xec => 1.9330751262581671e-53
source
Supposition.Data.Recursive — Type
Recursive(base::Possibility, extend; max_layers::Int=5) <: Possibility{T}

A Possibility for generating recursive data structures. base is the basecase of the recursion. extend is a function returning a new Possibility when given a Possibility, called to recursively expand a tree starting from base. The returned Possibility is fed back into extend again, expanding the recursion by one layer.

max_layers designates the maximum number of times extend will be used to wrap base in new layers. This must be at least 1, so that at least the base case can always be generated.

Equivalent to calling recursive(extend, base).

Examples

julia> base = Data.Integers{UInt8}()
+ 0xec => 1.9330751262581671e-53
source
Supposition.Data.Recursive — Type
Recursive(base::Possibility, extend; max_layers::Int=5) <: Possibility{T}

A Possibility for generating recursive data structures. base is the basecase of the recursion. extend is a function returning a new Possibility when given a Possibility, called to recursively expand a tree starting from base. The returned Possibility is fed back into extend again, expanding the recursion by one layer.

max_layers designates the maximum number of times extend will be used to wrap base in new layers. This must be at least 1, so that at least the base case can always be generated.

Equivalent to calling recursive(extend, base).

Examples

julia> base = Data.Integers{UInt8}()
 
 julia> wrap(pos) = Data.Vectors(pos; min_size=2, max_size=3)
 
@@ -136,7 +136,7 @@
 julia> example(rec)
 2-element Vector{UInt8}:
  0xbd
- 0x25
source
Supposition.Data.SampledFrom — Type
SampledFrom(collection) <: Possibility{eltype(collection)}

A Possibility for sampling uniformly from collection.

collection, as well as its eachindex, is assumed to be indexable.

Mutable Data

The source objects from the collection given to this SampledFrom is not copied when produce! is called. Be careful with mutable data!

julia> using Supposition
+ 0x25
source
Supposition.Data.SampledFrom — Type
SampledFrom(collection) <: Possibility{eltype(collection)}

A Possibility for sampling uniformly from collection.

collection, as well as its eachindex, is assumed to be indexable.

Mutable Data

The source objects from the collection given to this SampledFrom is not copied when produce! is called. Be careful with mutable data!

julia> using Supposition
 
 julia> sampler = Data.SampledFrom([1, 1, 1, 2])
 
@@ -145,12 +145,12 @@
  1
  1
  2
- 1
source
Supposition.Data.Satisfying — Type
Satisfying(source::Possibility, pred) <: Possibility

A Possibility representing values from source fulfilling pred.

Equivalent to calling filter(f, source).

julia> using Supposition
+ 1
source
Supposition.Data.Satisfying — Type
Satisfying(source::Possibility, pred) <: Possibility

A Possibility representing values from source fulfilling pred.

Equivalent to calling filter(f, source).

julia> using Supposition
 
 julia> pos = filter(iseven, Data.Integers{Int8}())
 
 julia> all(iseven, example(pos, 10_000))
-true
source
Supposition.Data.Text — Type
Text(alphabet::Possibility{Char}; min_len=0, max_len=10_000) <: Possibility{String}

A Possibility for producing Strings containing Chars of a given alphabet.

julia> using Supposition
+true
source
Supposition.Data.Text — Type
Text(alphabet::Possibility{Char}; min_len=0, max_len=10_000) <: Possibility{String}

A Possibility for producing Strings containing Chars of a given alphabet.

julia> using Supposition
 
 julia> text = Data.Text(Data.AsciiCharacters(); max_len=15)
 
@@ -160,7 +160,7 @@
  "hm\x172SJ-("
  "h`\x03\0\x01[[il"
  "\x0ep4"
- "9+Hk3 ii\x1eT"
source
Supposition.Data.Vectors — Type
Vectors(elements::Possibility{T}; min_size=0, max_size=10_000) <: Possibility{Vector{T}}

A Possibility representing drawing vectors with length l in min_size <= l <= max_size, holding elements of type T.

min_size and max_size must be positive numbers, with min_size <= max_size.

julia> using Supposition
+ "9+Hk3 ii\x1eT"
source
Supposition.Data.Vectors — Type
Vectors(elements::Possibility{T}; min_size=0, max_size=10_000) <: Possibility{Vector{T}}

A Possibility representing drawing vectors with length l in min_size <= l <= max_size, holding elements of type T.

min_size and max_size must be positive numbers, with min_size <= max_size.

julia> using Supposition
 
 julia> vs = Data.Vectors(Data.Floats{Float16}(); max_size=5)
 
@@ -168,4 +168,4 @@
 3-element Vector{Vector{Float16}}:
  [9.64e-5, 9.03e3, 0.04172, -0.0003352]
  [9.793e-5, -2.893, 62.62, 0.0001961]
- [-0.007023, NaN, 3.805, 0.1943]
source

Type-based hooks

These are hooks for users to provide custom implementations of certain parts of Supposition.jl. Follow their contracts precisely if you implement your own.

Possibility{T}

Supposition.Data.Possibility — Type
Possibility{T}

Abstract supertype for all generators. The T type parameter describes the kinds of objects generated by this integrated shrinker.

Required methods:

  • produce!(::TestCase, ::P) where P <: Possibility

Fallback definitions:

  • postype(::Possibility{T}) -> Type{T}
  • example(::Possibility{T}) -> T
source

ExampleDB

Supposition.ExampleDB — Type
ExampleDB

An abstract type representing a database of previous counterexamples.

Required methods:

  • records(::ExampleDB): Returns an iterable of all currently recorded counterexamples.
  • record!(::ExampleDB, key, value): Record the counterexample value under the key key.
  • retrieve(::ExampleDB, key)::Option: Retrieve the previously recorded counterexample stored under key. Return nothing if no counterexample was stored under that key.
source
+ [-0.007023, NaN, 3.805, 0.1943]source

Type-based hooks

These are hooks for users to provide custom implementations of certain parts of Supposition.jl. Follow their contracts precisely if you implement your own.

Possibility{T}

Supposition.Data.Possibility — Type
Possibility{T}

Abstract supertype for all generators. The T type parameter describes the kinds of objects generated by this integrated shrinker.

Required methods:

  • produce!(::TestCase, ::P) where P <: Possibility

Fallback definitions:

  • postype(::Possibility{T}) -> Type{T}
  • example(::Possibility{T}) -> T
source

ExampleDB

Supposition.ExampleDB — Type
ExampleDB

An abstract type representing a database of previous counterexamples.

Required methods:

  • records(::ExampleDB): Returns an iterable of all currently recorded counterexamples.
  • record!(::ExampleDB, key, value): Record the counterexample value under the key key.
  • retrieve(::ExampleDB, key)::Option: Retrieve the previously recorded counterexample stored under key. Return nothing if no counterexample was stored under that key.
source
diff --git a/dev/intro.html b/dev/intro.html index cf17c6c..76b5ea4 100644 --- a/dev/intro.html +++ b/dev/intro.html @@ -13,4 +13,4 @@ end end

Every time we run foo_prop, we generate a random input for foo and check whether its output behaves as expected. Written like this, it has a few major drawbacks:

  1. Being somewhat certain that we cover the function completely quickly becomes infeasible
  2. We have no control over the numbers being generated
  3. We can't reuse the way we generate these numbers; expanding a testsuite like this leads to a lot of boilerplate and repetition

On its own, just foo_prop is already property based testing - we take some expected input and check it against the expected output/behavior. However, on 64-bit systems, Int has a value in the interval [-9223372036854775808, 9223372036854775807], which is one of $2^{64}$ different values. Considering that our function takes two of those, our input space has $2^{2 \times 64}$ distinct pairs of elements! Looping through all of them would take much too long. Worse, we may then need to record the result for each of them to prove later that we actually checked it. With more complex data types, this only grows worse as more different types and combinations of them are involved.

This is where a related approach called fuzzing comes in - instead of checking ALL values and giving a 100% guarantee that it works as expected, we only check a sampled subset of all possible values and therefore only receive a probabilistic result. However, this comes with the distinct advantage of being much, much faster than checking all possible values. We trade accuracy for performance (much like we do with floating point values). If our sampling is good enough & representative of the actual data we'd usually expect, this can be a very good indicator for correctness on our input. The difficulty comes from the second point above - controlling the values we put in to a satisfying degree, as well as, once a failure is found, reducing it to something we humans can more easily use to pinpoint the uncovered bug, through a process called "shrinking". You can find the introductory explanations for how this works in the context of Supposition.jl in the Basic Usage section of the examples.

Julia specific nuances

Consider this (seemingly!) very trivial function:

function add(a,b)
     a + b
-end

Obviously, this function does nothing more than forward its arguments to +. From reading the source code above, we'd expect this to always behave the same as addition - and we'd probably be right! In julia though, a few subtleties come into play:

So in reality, purely from reading the source code, we know nothing more about add other than "passes its argument to +". This sort of genericity is both a blessing and a curse, in that it allows anyone that has + defined on two types to call our function, while also making it devilishly difficult for us as developers to anticipate all possible behaviors that can occur.

With property based testing, we should in theory be able to define a set of properties we'd like to hold on our code, for any object that can be passed into our add function. Users of our code who define a new type should be able to take those properties and check the behavior of their type & implementation in our function against the expected properties and find out (at least probabilistically) whether they've implemented the required functions correctly.

+end

Obviously, this function does nothing more than forward its arguments to +. From reading the source code above, we'd expect this to always behave the same as addition - and we'd probably be right! In julia though, a few subtleties come into play:

So in reality, purely from reading the source code, we know nothing more about add other than "passes its argument to +". This sort of genericity is both a blessing and a curse, in that it allows anyone that has + defined on two types to call our function, while also making it devilishly difficult for us as developers to anticipate all possible behaviors that can occur.

With property based testing, we should in theory be able to define a set of properties we'd like to hold on our code, for any object that can be passed into our add function. Users of our code who define a new type should be able to take those properties and check the behavior of their type & implementation in our function against the expected properties and find out (at least probabilistically) whether they've implemented the required functions correctly.

diff --git a/dev/objects.inv b/dev/objects.inv index 634cb23..a4ff374 100644 Binary files a/dev/objects.inv and b/dev/objects.inv differ diff --git a/dev/resources.html b/dev/resources.html index d3e422d..433d859 100644 --- a/dev/resources.html +++ b/dev/resources.html @@ -1,2 +1,2 @@ -PBT Resources · Supposition.jl Documentation
GitHub

PBT Resources

This page contains a collection of PBT tutorials and other useful resources for learning PBT techniques. Most, if not all, should be directly translatable to Supposition.jl in one form or another. If you find a new tutorial or resource that helped you test your code with Supposition.jl in some manner, please don't hesitate to open a PR adding the resource here!

  • The purpose of Hypothesis by David R. MacIver

    • [...], the larger purpose of Hypothesis is to drag the world kicking and screaming into a new and terrifying age of high quality software.

  • Hypothesis testing with Oracle functions by Hillel Wayne
    • A blogpost about using existing (but slower/partially incorrect) implementations to make sure a refactored or new implementation still conforms to all expected contracts of the old implementation.
  • Solving the Water Jug Problem from Die Hard 3 with TLA+ and Hypothesis by Nicholas Chammas
    • A blogpost about helping out John McClane (Bruce Willis) and Zeus Carver (Samuel L. Jackson) ~defuse a bomb~ solve fun children's games.
    • This blogpost has been translated to Supposition.jl! Check it out in the examples.
  • Rule Based Stateful Testing by David R. MacIver
    • A blogpost from the main developer behind Hypothesis, showing how to test stateful systems with Hypothesis.
    • This blogpost has been translated to Supposition.jl! Check it out in the examples.
      • Note: Not all features of Hypothesis have been ported to Supposition.jl, in particular the UX for stateful testing is very bare bones. The linked example contains a very manual implementation of the features utilized by Hypothesis for much the same thing, but should be easily adaptable for all kinds of stateful tests.
  • Proprty Testing Stateful Code in Rust by Raphael Gashignard
    • A blogpost about fuzzing internal datastructures of nushell using PBT and the Rust library proptest.
  • Automate Your Way to Better Code: Advanced Property Testing (with Oskar Wickström) by Kris Jenkins from Developer Voices

    • My Job as a programmer is to be lazy in the smart way - I see that many unit tests, and I just want to automate the problem away. Well that's the promise of property testing - write a bit of code that describes the shape of your software, and it will go away and create 10_000 unit tests to see if you're right, if it actually does work that way. [..] we're also going to address my biggest disappointment so far with property testing: which is that it only seems to work in theory. It's great for textbook examples, I'm sold on the principle, but I've struggled to make it work on my more gnarly real world code.

    • This is an absolutely delightful listen! A nice definition of what property based testing is, as well as a lot of discussion on how to start out with property based testing and continue with the approach onto more difficult pastures. Don't let yourself be intimidated by the length - take your time with this one, it's well worth it!
  • The Magic of Property Testing by Kris Jenkins from Developer Voices
    • This is a followup to "Automate Your Way to Better Code", showcasing an example of property based testing in PureScript. The fuzzing framework used here is a port of QuickCheck, but the general flow should be translatable to Supposition.jl. One feature being showcased (generation of objects through reflection) is not yet available in Supposition.jl; see this discussion for the state of things. Nevertheless, even without that, the generation capabilities of random data in Supposition.jl are just as powerful.
+PBT Resources · Supposition.jl Documentation
GitHub

PBT Resources

This page contains a collection of PBT tutorials and other useful resources for learning PBT techniques. Most, if not all, should be directly translatable to Supposition.jl in one form or another. If you find a new tutorial or resource that helped you test your code with Supposition.jl in some manner, please don't hesitate to open a PR adding the resource here!

  • The purpose of Hypothesis by David R. MacIver

    • [...], the larger purpose of Hypothesis is to drag the world kicking and screaming into a new and terrifying age of high quality software.

  • Hypothesis testing with Oracle functions by Hillel Wayne
    • A blogpost about using existing (but slower/partially incorrect) implementations to make sure a refactored or new implementation still conforms to all expected contracts of the old implementation.
  • Solving the Water Jug Problem from Die Hard 3 with TLA+ and Hypothesis by Nicholas Chammas
    • A blogpost about helping out John McClane (Bruce Willis) and Zeus Carver (Samuel L. Jackson) ~defuse a bomb~ solve fun children's games.
    • This blogpost has been translated to Supposition.jl! Check it out in the examples.
  • Rule Based Stateful Testing by David R. MacIver
    • A blogpost from the main developer behind Hypothesis, showing how to test stateful systems with Hypothesis.
    • This blogpost has been translated to Supposition.jl! Check it out in the examples.
      • Note: Not all features of Hypothesis have been ported to Supposition.jl, in particular the UX for stateful testing is very bare bones. The linked example contains a very manual implementation of the features utilized by Hypothesis for much the same thing, but should be easily adaptable for all kinds of stateful tests.
  • Proprty Testing Stateful Code in Rust by Raphael Gashignard
    • A blogpost about fuzzing internal datastructures of nushell using PBT and the Rust library proptest.
  • Automate Your Way to Better Code: Advanced Property Testing (with Oskar Wickström) by Kris Jenkins from Developer Voices

    • My Job as a programmer is to be lazy in the smart way - I see that many unit tests, and I just want to automate the problem away. Well that's the promise of property testing - write a bit of code that describes the shape of your software, and it will go away and create 10_000 unit tests to see if you're right, if it actually does work that way. [..] we're also going to address my biggest disappointment so far with property testing: which is that it only seems to work in theory. It's great for textbook examples, I'm sold on the principle, but I've struggled to make it work on my more gnarly real world code.

    • This is an absolutely delightful listen! A nice definition of what property based testing is, as well as a lot of discussion on how to start out with property based testing and continue with the approach onto more difficult pastures. Don't let yourself be intimidated by the length - take your time with this one, it's well worth it!
  • The Magic of Property Testing by Kris Jenkins from Developer Voices
    • This is a followup to "Automate Your Way to Better Code", showcasing an example of property based testing in PureScript. The fuzzing framework used here is a port of QuickCheck, but the general flow should be translatable to Supposition.jl. One feature being showcased (generation of objects through reflection) is not yet available in Supposition.jl; see this discussion for the state of things. Nevertheless, even without that, the generation capabilities of random data in Supposition.jl are just as powerful.