Skip to content

Commit

Permalink
Update docs to include finite generation
Browse files Browse the repository at this point in the history
  • Loading branch information
Seelengrab committed Aug 12, 2023
1 parent 502bf71 commit b8f65be
Show file tree
Hide file tree
Showing 8 changed files with 209 additions and 10 deletions.
3 changes: 2 additions & 1 deletion docs/make.jl
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,8 @@ function builddocs(clear=false)
"Basic Usage" => "Examples/basic.md",
"Generating Structs" => "Examples/structs.md",
"Generating Containers" => "Examples/containers.md",
"Composing Generators" => "Examples/properties.md"
"Composing Generators" => "Examples/properties.md",
"Generator Chaining" => "Examples/chaining.md"
],
"Shrinking with `Tree`s" => "shrinktrees.md",
"FAQ" => "faq.md",
Expand Down
2 changes: 1 addition & 1 deletion docs/src/Examples/basic.md
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ julia> failprop(x) = add(x, one(x)) < x;
julia> check(failprop, gen)
┌ Info: Found counterexample for 'failprop', beginning shrinking...
└ Counterexample = 909071986488726633
[ Info: 10 counterexamples found
[ Info: 10 counterexamples found for failprop
0
```

Expand Down
124 changes: 124 additions & 0 deletions docs/src/Examples/chaining.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,124 @@
# Chaining generation

Sometimes, it is useful to be able to generate a finite set of "special values", before throwing the full brunt of possible values of a type at your function.
At other times, you may want to test a few special distributions of values whose generation isn't finite, before having PropCheck.jl try a generic type-based
fuzzing approach. In these cases, it's helpful to try one of the subtypes of [`PropCheck.FiniteIntegrated`](@ref).

## IntegratedOnce

[`PropCheck.IntegratedOnce`](@ref) is the "Give me a value, but please only one value" version of [`PropCheck.ival`](@ref). It is semantically the same as
`PropCheck.IntegratedLengthBounded(ival(x), 1)` (which we'll look at in detail later), but with a more efficient implementation.

Here's an example:

```@repl once
using PropCheck
using PropCheck: IntegratedOnce
gen = IntegratedOnce(5)
tree = generate(gen)
subtrees(tree) |> collect # The shrink tree is unfolded as usual
generate(gen) isa Nothing # but subsequent `generate` calls don't produce any value
generate(gen) isa Nothing
```

If you know that you're only going to require the value to be tested exactly once, while still being able to test its shrinks in case the property fails, `IntegratedOnce` can be a very good choice.
An example use case is for regression testing of known previous failures.

Of course, this kind of integrated shrinker can be `map`ped and `filter`ed just the same as regular infinite generators:

```@repl once
gen = filter(iseven, IntegratedOnce(5));
tree = generate(gen)
root(tree)
subtrees(tree) |> collect
gen = map(x -> 2x, IntegratedOnce(5));
tree = generate(gen)
root(tree)
subtrees(tree) |> collect
```

!!! warning "Copying & exhaustion"
Keep in mind that all finite generators can only be exhausted _once_. So be sure to `deepcopy` the finite generators
if you want to reuse them in multiple places. This may later be relaxed to only `copy` for some finite generators,
in order to reuse as many reusable generators as possible.

## IntegratedFiniteIterator

[`PropCheck.IntegratedFiniteIterator`](@ref) can be used to produce the values of a given finite iterator, one after the other, before suspending generation of new values.

This is useful when you have a known set of special values that you want to try, which are likely to lead to issues. `IntegratedOnce` is similar to this integrated shrinker, with the difference being
that `IntegratedFiniteIterator` can take any arbitrary iterable (except other `AbstractIntegrated`) to produce their values in exactly the order they were originally produced in from the iterator.

```@repl finiteiter
using PropCheck
using PropCheck: IntegratedFiniteIterator
iter = 1:2:21
gen = IntegratedFiniteIterator(iter); # all odd values between 1 and 21, inclusive
length(gen) == length(iter)
all(zip(gen, iter)) do (gval, ival)
root(gval) == ival
end
generate(gen) isa Nothing # and of course, once it's exhausted that's it
```

## IntegratedLengthBounded

[`PropCheck.IntegratedLengthBounded`](@ref) can be used to limit an [`PropCheck.AbstractIntegrated`](@ref) to a an upperbound in the count of generated values, before generation is suspended.

This can be useful for only wanting to generate a finite number of elements from some other infinite generator before switching to another one, as mentioned earlier. The basic usage is
passing an `AbstractIntegrated` as well as the desired maximum length. If a `FiniteIntegrated` is passed, the resulting integrated shrinker has as its length the `min` of the given
`FiniteIntegrated` and the given upper bound.

```@repl bounded
using PropCheck
using PropCheck: IntegratedLengthBounded, IntegratedOnce
gen = IntegratedLengthBounded(itype(Int8), 7);
collect(gen) # 7 `Tree{Int8}`
gen = IntegratedLengthBounded(IntegratedOnce(42), 99);
length(gen) # still only one `Tree{Int}`
collect(gen)
```

## IntegratedChain

While itself not guaranteed to be finite, [`PropCheck.IntegratedChain`](@ref) is the most useful tool when combining finite generators in this fashion. Its
constructor takes any number of `AbstractIntegrated`, though all but the last one are required to subtype `FiniteIntegrated`.
The last integrated shrinker may be truly `AbstractIntegrated`, though being `FiniteIntegrated` is also ok.

This allows `IntegratedChain` to be a building block for grouping special values together, or for preparing a known set of previous failures into a regression test,
while still allowing the values to shrink according to the shrinking function used during the original generation, if available.

```@repl chain
using PropCheck
using PropCheck: IntegratedChain, IntegratedOnce, IntegratedFiniteIterator
using Test
function myAdd(a::Float64, b::Float64)
# whoops, this isn't `add` at all!
1.0 <= a && return NaN
a + b
end
previousFailure = interleave(IntegratedOnce(0.5), IntegratedOnce(0.2));
specialCases = IntegratedFiniteIterator((NaN, -1.0, 1.0, 0.0));
specialInput = interleave(specialCases, deepcopy(specialCases)); # take care to not consume too early
addGen = IntegratedChain(previousFailure, # fail early if this doesn't work
specialInput, # some known special cases
PropCheck.tuple(ival(2), itype(Float64))); # finally, fuzzing on arbitrary stuff!
function nanProp(a, b)
res = myAdd(a,b)
# only `NaN` should produce `NaN`
(isnan(a) || isnan(b)) == isnan(res)
end
@testset "myAdd" begin # We find a failure past our first chain of special cases
@test check(splat(nanProp), addGen)
end
```
6 changes: 3 additions & 3 deletions docs/src/Examples/containers.md
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,7 @@ julia> check(prop, vec)
│ -62
│ 57
└ 81
[ Info: 7 counterexamples found
[ Info: 7 counterexamples found for prop
3-element Vector{Int8}:
0
0
Expand Down Expand Up @@ -131,13 +131,13 @@ and subsequently, the minimal counterexample also changes, to the vector contain
```jldoctest examplevec; filter=[r"(\[ Info: \d+)",r"[┌│└]\s+-?\d+"], setup=:(using PropCheck; valvec = PropCheck.vector(ival(3), itype(Int8)); samplevec=PropCheck.vector(isample(0:5), itype(Int8)))
julia> check(prop, valvec; show_initial=false)
[ Info: Found counterexample for 'prop', beginning shrinking...
[ Info: 7 counterexamples found
[ Info: 7 counterexamples found for prop
1-element Vector{Int8}:
5
julia> check(prop, samplevec; show_initial=false)
[ Info: Found counterexample for 'prop', beginning shrinking...
[ Info: 9 counterexamples found
[ Info: 9 counterexamples found for prop
1-element Vector{Int8}:
5
```
2 changes: 1 addition & 1 deletion docs/src/Examples/properties.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# Complex generation
# Composing Generators

I've mentioned in the last section how we need `tuple` and `vector` to generate tuples and vectors of values respectively.
In this chapter, we'll use these to build a slightly more complex example.
Expand Down
50 changes: 50 additions & 0 deletions docs/src/faq.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,55 @@
# FAQ

## What exactly is "shrinking"?

And the related questions, "What is being minimized when shrinking? What is the figure of merit?", originally asked [here](https://discourse.julialang.org/t/ann-propcheck-jl/101481/21?u=sukera).

Measuring shrinking values is a bit difficult - after all, the goal is to create a smaller (to human eyes) instance of the given type. It's very subjective what that means, but there are
some generalities you can apply. For example, a `0.0` is less "complex" of a value than `1234651.3465`, so it's usually considered smaller for shrinking purposes. Similarly, an array with
just 2 values is generally considered simpler/smaller than an array with 4123 values, even if both arrays otherwise exhibit the same properties.

Expanding on that - consider checking whether all arrays of positive integers are sorted. Surely, there are lots of counterexamples to that, like `[164, 45, 128, 202, 87]`, `[5,3,2,1]`,
`[1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]`, but there's only one example that's minimal: `[1, 0]`, the array with minimal values and minimal length.

This is of course not correct for all properties and all value domains; the "minimal counterexample" can look quite different depending on what kind of values you're mostly
interested in. For example, if you're interested in finding the smallest possible counterexample for arrays of `Int8`, it'll be `[-127, -128]`, because the smallest possible
counterexample numerically is a negative number with larger absolute value. By default, PropCheck won't give you that, because a smaller absolute value is usually more desirable
for humans to think about; the bitpattern underlying the number is simpler (or shorter, if you remove leading zeros). To have PropCheck give you those smaller numerical shrinks,
you simply give e.g. `itype` a shrinking function producing those values:

```julia
julia> using PropCheck

julia> vect = PropCheck.vector(ival(4), itype(Int8, PropCheck.shrinkTowards(typemin(Int8))));

julia> check(issorted, vect)
┌ Info: Found counterexample for 'issorted', beginning shrinking...
│ Counterexample =
4-element Vector{Int8}:
-2
58
21
-85
[ Info: 32 counterexamples found
2-element Vector{Int8}:
-127
-128
```
`shrinkTowards` currently only has definitions for numeric types (`<: Integer`, `<: AbstractFloat`, `Bool`) because shrinking towards a general object is quite a bit harder - e.g.
shrinking towards a given string could be an option by working through inserts, deletions & character changes, but I'll have to think about how to best do that to make sure the
full possible space between a given source & target string is generateable.
> What is being minimized when shrinking? What is the figure of merit?
Circling back around to your question - anything you want, really! With a custom shrinking function (which you can supply to everything that generates a value),
YOU get to decide how you want to shrink/minimize things. PropCheck.jl just tries to give you some sane defaults for types from Base (or at least, those I've
gotten around to implementing `generate` and `shrink` for). E.g. in [Composing Generators](@ref),
I use `PropCheck.noshrink` to make sure some strings _don't_ shrink when shrinking the object the generator is used in, because looking at a student with a name
is nicer than looking at a student with the empty string as a name. This is generally applicable with any custom shrinking function; whichever values you
consider to be smaller for the purpose of that shrinking function are what PropCheck.jl considers "smaller" (which is also why it's important that shrinking
functions can't produce shrinking loops - i.e. a shrinking function must never produce a value that, when shrunk with the same shrinking function again, could lead to the initial value).
## What about formal specifications?
While efforts regarding formal specifications & machine checkable proofs are comendable, I think we can get quite far with property based testing & fuzzing
Expand Down
24 changes: 23 additions & 1 deletion docs/src/interfaces.md
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,26 @@ PropCheck.ExtentIntegrated
Its purpose is simple - values produced by an `ExtentIntegrated` are expected to fall within a given
ordered set, with a maximum and a minimum, which is what is returned by `extent`.

## `InfiniteIntegrated{T}`

```@docs
PropCheck.InfiniteIntegrated
```

`InfiniteIntegrated` are at the core of PropCheck.jl; they allow for arbitrarily long generation of new values.
They are currently always implementes as stateless objects, and underpin the majority of generation that is possible
with PropCheck.jl.

## `FiniteIntegrated{T}`

```@docs
PropCheck.FiniteIntegrated
```

`FiniteIntegrated` are used for stopping generation of values. They are currently always implemented as
stateful objects during generation, i.e. they cannot be restarted. This may change in the future, but is
(currently) a consequence of the existing design.

## Generation & Shrinking

These two functions are required if you want to customize shrinking & type-based generation.
Expand All @@ -56,6 +76,8 @@ PropCheck.itype

In order to hook into the generation provided by `itype`, define [`generate`](@ref) for your type `T`.

Generally speaking, `generate` should always produce the full set of possible values of a type.
Generally speaking, `generate` should always produce the full set of possible values of a type. For example,
`itype(Float64)` can produce every possible `Float64` value, with every possible bitpattern - that includes all
different kinds of `NaN`.

Be sure to also define a shrinking function for your type, by adding a method to [`shrink`](@ref).
8 changes: 5 additions & 3 deletions docs/src/shrinktrees.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ When we `generate` a value from an integrated shrinker, we get some `Tree` out,

```@repl generateTree
using PropCheck
nums = PropCheck.iconst(3);
nums = PropCheck.isample(1:3);
t = generate(nums)
```

Expand All @@ -23,9 +23,11 @@ print_tree(t)

On the left hand side up top we can see our generated root - the initial value `3`. One layer to the
right, we can see the first level of shrinks of `3`. These values have been produced by the default
shrinking function `shrink` that is passed to `ival` - they observe the property that their absolute
shrinking function `shrink` that is passed to `isample` - they observe the property that their absolute
value is strictly less than the value of our root, in order to guarantee that their shrunk values
in turn don't ever generate the original value (in this case, `3`) again.
in turn don't ever generate the original value (in this case, `3`) again. In addition, the default shrinking
function also guarantees that the shrunk values are larger than the minimum of the given range; hence,
the smallest number that can be generated is `1`.

The magic behind PropCheck.jl is in this `Tree` object, which is heavily inspired by the [Hedgehog
Haskell library](https://hedgehog.qa) for property based testing.
Expand Down

0 comments on commit b8f65be

Please sign in to comment.