Extremely basic usage of the package - readme example

[nilshg]

I don't understand the most basic example in the readme:

julia> using Supposition

julia> intgen = Data.Integers{Int8}();

julia> @check function foo(i=intgen)
           i isa Int
       end
┌ Error: Property doesn't hold!
│   Description = "foo"
│   julia> using Supposition

julia> intgen = Data.Integers{Int8}();

julia> @check function foo(i=intgen)
           i isa Int
       end
┌ Error: Property doesn't hold!
│   Description = "foo"
│   Example = (i = -128,)
└ @ Supposition C:\Users\NGudat\.julia\packages\Supposition\KpGkN\src\testset.jl:292
Test Summary: | Fail  Total  Time
foo           |    1      1  0.1s
└ @ Supposition ...\.julia\packages\Supposition\KpGkN\src\testset.jl:292
Test Summary: | Fail  Total  Time
foo           |    1      1  0.1s

Questions:

1. What function are we testing here? In the main docs a function add is defined, and then the PBT tests are like

@check function test_some_property(x = some_input_generator)
    function_to_test(x) == expected_output
end

if I understand correctly. But here there's no function that we're testing, so are we essentially just testing that (probabilistically) all elements of intgen are of type Int?

2. Why does this fail? The output says Example = (i = -128,) but foo(-128) returns true (because -128 isa Int) so clearly I don't understand what's actually being tested here.

3. The docs mention sampling, Bayesian stats, and probabilistic testing in various places. Is there any information on the statistical properties of what we're doing here? E.g. if I pass in some generator how many samples from that generator are being used? Are things being sampled completely at random, although it's probably often the case that certain input values (e.g. typemin/max, 0) are much more likely to uncover issues?

[Seelengrab]

Thanks for the questions!

What function are we testing here?

There's no explicit function/property per se that we're testing here; it's an example to introduce the @check syntax while defining a property foo. I should probably put a better example there that actually tests something! I originally used such a small example so that readers aren't overwhelmed with a large block of foreign syntax, but I can see how that backfires when the property is pretty nonsensical 😅

But here there's no function that we're testing, so are we essentially just testing that (probabilistically) all elements of intgen are of type Int?

Yes, that is correct - note that intgen is defined as Data.Integers{Int8}(), i.e. it will generate Int8 exclusively. Those are not an Int! Remember, Int is Int64 on 64 bit machines and Int32 on 32 bit machines; the overarching abstract type for integers is Integer. Would it help if I call this generator int8gen?

Why does this fail? The output says Example = (i = -128,) but foo(-128) returns true (because -128 isa Int) so clearly I don't understand what's actually being tested here.

That's an issue with the printing 😓 The generator ended up producing Int8(-128), but the default printing currently used here doesn't show the type.. I'm actively working on improving this (see e.g. #23) and the printing of Possibility in general (see #31), which has made good progress now that StyledStrings.jl is released. The improved printing should land in the coming week or so :)

I'll also add a convenience function to retrieve the actual counterexample programmatically, so people don't have to rely on the printing giving them what they need for further debugging.

The docs mention sampling, Bayesian stats, and probabilistic testing in various places. Is there any information on the statistical properties of what we're doing here?

For the most part, yes it's completely random. It's difficult to give exact statistical properties because it depends on the individual Possibility, as well as how they're composed. For example, for Data.Vectors, the lengths of the produced vectors follow a distribution that biases towards shorter vectors in the beginning of the generation process, increasing the length the longer a test runs. See #4 for some more details.

There is Data.WeightedNumbers as well as Data.WeightedSample which you can pass weights to indicate a distribution to sample the numbers 1:n/a collection with.

I mostly mention Bayesian stats as a sort of "think of testing not in terms of absolutes" kind of thing - unless a function is tested with literally all inputs (or other mathematical proof that shows you've tested all equivalency classes of the possible inputs), it's really impossible to say "the code works correctly". As such, I tend to think of a testsuite as giving myself some confidence in correctness, with each run of the testsuite increasing that confidence (hence, I'm updating my prior that the function under test works correctly 😉 ).

E.g. if I pass in some generator how many samples from that generator are being used?

That depends on how they're being composed & used 🤔 By default, @check generates 10_000 example inputs for the given property from the Possibility that are being passed in; that is, the property here will be invoked 10_000 times with input generated from the arguments int8gen and float16gen:

int8gen = Data.Integers{Int8}()
float16gen = Data.Floats{Float16}()
@check function baz(i=int8gen, f=float16gen)
    # ...
end

so each of int8gen and float16gen will be asked to generate a value 10_000 times. You can configure that by passing e.g. max_examples=100 to @check.

If, on the other hand, you're using that int8gen to create a Vector through Data.Vectors, int8gen may be invoked much more than that. So for Data.Vectors(int8gen; min_size=500), int8gen would be invoked at least 500 * 10_000 == 5_000_000 times, since the vector will be at least 500 elements long and there will be (by default) 10_000 vectors being generated.

Are things being sampled completely at random, although it's probably often the case that certain input values (e.g. typemin/max, 0) are much more likely to uncover issues?

For the most part, yes. I have been thinking about stateful generators that first try to generate some special values, but that turns out to be a bit difficult for composition. For example, if you had a generator that for the first call of produce! (the function that requests a Possibility to generate a value) always gives typemin, what should happen when it's used in Data.Vectors? Should only the first element of that Vector be typemin, or should all elements of the Vector be typemin?

In practice, what exactly is considered a special value for the purpose of finding bugs depends a lot on what property you're testing - there's no ultimately perfect heuristic to use here 🤷

---

Hope this helps alleviate (at least some of) the confusion!

[nilshg]

Cool thank you - I would say yes a slightly different example in the readme would be helpful, and I'm glad there was a sort-of-issue with the printing, although the reality is I mostly didn't get the example because I forgot that Int != Integer 😆

On the statistical properties I guess my work often involves things like "audit sampling" where we basically want to conclude that at a confidence level of X% there are less than Y% erroneous records in a population, and to do that we need to verify a sample of size Z (which can be computed from our desired levels of X and Y). I suppose that just doesn't really make sense here because some inputs will be "special cases" (which as you say aren't really generally identifiable) so normal sampling theory just doesn't apply.

Hope to find a way to use this package one day!

[Seelengrab]

You're welcome!

I would say yes a slightly different example in the readme would be helpful, and I'm glad there was a sort-of-issue with the printing, although the reality is I mostly didn't get the example because I forgot that Int != Integer 😆

Haha, alright, I'll think about a small example that's perhaps a bit clearer!

I suppose that just doesn't really make sense here because some inputs will be "special cases" (which as you say aren't really generally identifiable) so normal sampling theory just doesn't apply.

Yes, exactly. Not to mention, the sample sizes you'd need to get actual high confidence levels on a per-function-basis in software testing are super high; just take a function f(x::Int64, y::Int64), which already has an input statespace of size 2^128! To get "true high confidence" you'll have to either sample a still-ridiculously-large subset of that, identify some domain knowledge to segment the statespace into equivalence classes or find some other shortcut. This only gets worse with more complex inputs, like Strings or Vectors.

The value in Supposition.jl/fuzzing is thus in generating input that a human wouldn't ordinarily think of - or at least, input that has as few guarantees about what it looks like as possible, making it more likely to test the unexpected :)