demonstrate the utility of Apropos

[divipp]

The current examples produce mainly self-tests, and non-self-tests are easier to write with QuickCheck than with Apropos.
(Self-tests are testing the so-called Apropos morphisms which is not user code; it is written to help the testing of user code.)

I need one example which demonstrates that Apropos is better than QuickCheck.

• Define data types A and B, a function f : A -> B and a list of QuickCheck property tests [t1, t2, ..., tN] for f.
• Make sure that [t1, t2, ..., tN] is nearly optimal, i.e. you cannot write much shorter equivalent idiomatic QuickCheck code. (I volunteer to help in this step.)
• Write Apropos code which is equivalent to [t1, t2, ..., tN].
• Show that the Apropos code is faster/shorter than the definition of [t1, t2, ..., tN].

[divipp]

I understand that Apropos is still a proof-of-concept implementation of an idea, but being so it needs at least one convincing example.

[L-as]

Aren't self-tests a very big reason?

[divipp]

Aren't self-tests a very big reason?

Self tests are testing generators.
Probably it is easier to understand this with a QuickCheck example.
In QuickCheck there are predefined generators (= random distributions) for common data structures.
If you add a new generator, you may want to test it because good generators are essential for testing user code.
But testing generators alone is not enough; the ultimate goal is to test the user code.

[delicious-lemon]

@divipp The self tests for a HasParameterisedGenerator are representative of the property tests that would run against your user code. One of the main selling points of apropos is that you can specify your behavior before writing any user code. This is test driven development.

Building generators is what apropos does. It allows you to build generators that are parameterised by a logical model apropos a type. From this you can enumerate the generators for each property test.

The quantity of tests generated is dependent on the complexity of the logical model. Due to the nature of boolean satisfiability it is trivial to write a model that generates an enormous amount of tests - to see this you can extend the IntPair model to IntTriple, IntQuadruple, etc... and watch as the number of tests grows exponentially.

RE: improving the examples with a comparison to quickcheck. It is worth noting that we are interested in testing a specific kind of code - smart contracts. These are functions which express constraints on the contract inputs/outputs and context - i.e. A -> Bool. apropos is perfectly suited to testing these functions since your logical model can partition the space of A into those that should validate and those that should fail. You can specify this partition in terms of a logical formula in the language of your properties.

Other kinds of functions may be less well suited to testing with apropos. - for example [f :: A -> B would require a model of the relation A X B, associativity may require a model of an AST, etc...]. Apropos can test these things but it may be the wrong tool for some of them - for example there is no point in testing associativity of + with apropos since a single property test is all you need.

[divipp]

@delicious-lemon

Other kinds of functions may be less well suited to testing with apropos.

It is fine to chose Bool for B.
If so, the challenge looks like this:

• Define data type A, a function f : A -> Bool and a list of QuickCheck property tests [t1, t2, ..., tN] for f.
• ...

The self tests for a HasParameterisedGenerator are representative of the property tests that would run against your user code.

This fits the challenge too.
I interpret this as [t1, t2, ..., tN] is chosen to be the self-tests.
Maybe it works and you win the challenge.
It may not work because:

• either the self-tests has no connection with f (so they don't test f, they test something else)
• or the self-tests are trivial in the sense that they can be replaced by much shorter equivalent QuickCheck tests

[delicious-lemon]

@divipp I think this issue can be moved to the apropos-tx repo. We are planning on putting some examples for real world contracts (perhaps an auction) in there as well as library models for common things. The real world contract tests should be convincing.

[divipp]

@delicious-lemon I think it would be more convincing to have a synthetic self-contained example. Once you have a good candidate example in apropos-tx I can help to make it a bit more abstract so that it can be placed in this repo.

[NorfairKing]

I'd like to be convinced as well.
My main concern is that it looks like the tests are no simpler than the code, which means tests aren't necessarily going to work at all.

[delicious-lemon]

My main concern is that it looks like the tests are no simpler than the code, which means tests aren't necessarily going to work at all.

I don't understand what you mean by this. In my experience it is often the case that tests are more complex than the code.

The complexity here is required to explain to a solver how to build your test suite - there is an inflection point in terms of complexity where you will start to profit from the power of the solver (below that it might seem that writing tests by hand is simpler).

[AriFordsham]

@divipp Does #61 help?

[NorfairKing]

@AriFordsham It doesn't. This new readme doesn't show that apropos works better than manually writting validity-based tests.

[AriFordsham]

@NorfairKing I acknowledge apropos is under-documented as well as under-exampled and on that basis this issue is correct.

I just wanted to open a dialogue by answering your question here, where it can be recorded.

As I understand it, validity is essentially a replacement for the Arbitrary typeclass that is lawful and supports invariants that are not intrinsic to a datatype's layout. There is a 1-to-1 relationship between types with invariants and their generators, hence the typeclass.

This, as an extension of property testing in general, works by testing the assertion:

Laws should hold for all (valid) examples of input data

Test data are generated 'randomly'. From what distribution is this drawn?

This is another question QuickCheck leaves open, is not easy to answer, and as far as I can see, validity does not attempt to answer either.

The simple answer (and also the straightforward definition of 'random') is 'a uniform distribution.' This is not necessarily helpful, because some values are more 'different' than others. It's certainly not what QuickCheck does.

QuickCheck establishes a loose convention by which generators generate values based on some undefined property called 'size' in order that both 'small' and 'large' values are tested. There is some vague notion that if value causes a test to fail, this failure may be rooted in a 'smaller' precursor to itself. 'Shrinking' is provided to generate this precursor.

The problem here is that values often have properties that determine their propensity to trigger bugs. Examples include 'big'- and 'small'-ness, as implied by QuickCheck, but these are not always relevant, nor are they the only ones. For example, for numbers, zero, positive and negative values are important, and for finite number types bounds matter.

In certain circumstances, for example when inter-relations between substructures become interesting, this problem scales faster than ad-hoc solutions can.

The solution Apropos explores is to partition a value into its interesting properties or subtypes, and to test properties (laws) against all (or a selection) of these.

Like this, for each 'law', if I can subdivide the input datatype n interesting ways, I get up to n^2 property tests for free for each property written.

The design for Apropos is certainly still evolving. I would welcome any collaboration you would be interested in.