Triq: The Free QuickCheck for Erlang

Today I released the first version of Triq - Trifork QuickCheck (or triq for short), a free clone of QuviQ eqc. While triq is being developed for the purpose of testing Erjang it is "plain erlang" all the way, with no dependencies on Erjang in any way.

First I have to say that i feel a little uneasy releasing Triq, because the good guys at QuviQ are trying to make a business out of this. Never the less, I made the decision because an open source project is the only way for many people to try out quickcheck, and because eqc doesn't work on Erjang yet (I got a 30 day trial license, but failed to run in on Erjang). I have a lot of respect for John and Thomas, and I hope that Triq will have the effect of generating more interest for QuviQ eqc, which [at least for the time being] is a far superior product. I hope that Triq will make it easier for people to get started with quickcheck on the Erlang platform, and using the professional QuviQ eqc will be a natural progression for commercial users.

Enough disclaimers, now onto the action. In this blog post I'd like to explain how quick check works, because I think that it really needed to some extent to be able to envision what you can use it for. I'll followup with some more examples later on how I use it in context of Erjang.

Property Based Testing

Property based testing with QuickCheck is really nice, and very easy in context of a functional language like Erlang. QuickCheck properties are like unit tests, that are supposed to be true. A property is represented in Triq Check as an opaque value that you can give to triq:check/1 to have it tested, as in:

Prop = ?FORALL({X,Y}, 
               {int(),int()},
               (X==Y) == (Y==X)).

That is, for all two integers X and Y the (boolean) value of (X == Y) is equal to (Y == X). That may sound pretty moot, but for a VM implementation that is perhaps not so obvious.

To test the property, you call triq:check/1 like this:

1> triq:check(Prop).
.....................................................................
.................
Ran 100 tests
true
2> 

A more interesting case happens when a test fails. Here is one that typically fails:

prop_delete() ->
  ?FORALL(L,list(int()), 
    ?IMPLIES(L /= [],
       ?FORALL(I,elements(L), 
          not lists:member(I,lists:delete(I,L))))).

Which reads like this: For all values L in the domain "list of integers", if L is not an empty list, then for all values I, where I is an element of L; removing I from L yields a list of which I is not a member. Read that one more time.

When you run it, it fails if L happens to be a list that contains the same value twice. The lists:delete function only deletes the first occurrence of I in the list.

2> triq:check(prop_delete()).
x....Failed!

Failed after 5 tests with false
Simplified:
        L = [0,0]
        I = 0
false
3> 

The cool thing is that not only does Triq Check find some counter example for the property, it finds the minimal counter example.

But how does all this work?

To get started, let us take a closer look at the FORALL macro found in triq.hrl, in context of the first really simple example:

Prop = ?FORALL({X,Y}, 
               {int(),int()},
               (X==Y) == (Y==X)).

Here is an explanation of what you see:

• The first argument {X,Y} is a syntactic form used to assign value that will be bound in the body.
• The second argument {int(),int()} is a value domain, describing the domain of two-tuples containing integers at both position 1 and 2. The structure of the first two arguments must match, otherwise the check will fail with an exception.
• The third argument (the body) is an expression which is evaluated with X and Y bound to some random integers.

What actually happens is that FORALL saves a fun in a tuple ... the macro is defined something like this:

-define(FORALL(Args,Domain,Body), 
    { ..., body = fun( Args ) -> Body end, domain = Domain... }).

Later, when the test is executed, triq uses an internal (magic) function to generate some "random" member of the given domain, and pass it to the body:

test({ ..., body=Body, domain=Domain, ...}) ->
   Input = generate_member(Domain),
   Result = Body(Input).

The result of evaluating the body controls the how the test proceeds:

• If the body evaluates to true, then the test succeeds; (and triq will try again with another value of the given domain)
• if the body evaluates to a property then that property is checked recursively;
• otherwise the test fails.

Two concepts: properties, and value domains.

A property is an opaque value, which is the result of evaluating one of the macros FORALL, IMPLIES, WHENFAIL, TRAPEXIT, and TIMEOUT, or one of the functions in triq such as triq:fails/1 which inverts the success/failure of it's containing property.

A value domain can have one of several forms, some of which are opaque, and some are not:

• a tuple {VD1, ..., VDn} where each element VDi is itself a value domain generates N-tuples (i.e. the same size as the input), where each element is generated in the value domain of the corresponding tuple element.
• a list [VD1, ..., VDm] does the same thing, but for lists.
• all the functions exported from triq_domain, such as int/0, list/1, any/0, etc. yield value domains for specific kinds of values.
• any other value describes the domain of values that contain exatly the value itself as a member i.e., this domain can only generate said value, and can only be "shrunk" to said value too.

Thus, for instance:

{foo, int(), [x|choose(1,10)]}

Describes the domain of 3-tuples, for which the first element is always the atom foo, the 2nd element is an integer, and the 3rd element is a cons cell in which the head is always the atom x, and the tail can be any integer in the range 1..10. The functions int and choose are imported for you from the module triq_domain when you include triq.hrl.

Shrinking

QuickCheck will repeatedly try to test a property with increasingly complex/size input values, until it reaches a fixed number of runs (currently 100), or until it stops because it has found a counter example (i.e., an input value that makes the property fail).

The magic in QuickCheck happens when it is able to shrink a counter example to something comprehensible. Internally it does that by calling a function

SimplerValue = simplify_value(ValueDomain, Value).

Which will try its best to pick another value from said ValueDomain which is "simpler" than Value, for some definition of "simpler".

• For the int() value domain, values gravitate to zero: negative numbers gradually grow and positive numbers gradually shrink.
• For aggregate domains such as list(Dom), simplify_value will either replace one of the elements of the list with a simpler member, or remove one of the members of the list thus gravitating towards the empty list,
• ... and so on for other value domains.

The shrinking is done by performing a second run on the property, repeatedly shrinking and checking the property again; until it shrinks no further. That's it really -- pretty cool, eh?

Onwards from here...

Triq Check is early in its life, but to the best of my knowledge completely functional for what it does. I'm eager to receive reports from someone using it.

One of the areas that I have not explored is that it seems that QuviQ eqc has some advanced strategies for controlling the shrinking; kind of "pointing it in the right direction". Triq Check uses a pretty brute force method which seems to work fine on my small examples, but may prove totally inadequate for larger values.

Let me hear from you! Follow the project on GitHub github.com/krestenkrab/triq, or follow me on twitter: @drkrab.