QuickTheories

Property-based testing for Java 8.

If you were looking for QuickCheck for Java you just found it.

Unlike many other systems QuickTheories supports both auto-magical shrinking and targeted search using coverage data.

What is property based testing

Traditional unit testing is performed by specifying a series of concrete examples and asserting on the outputs/behaviour of the unit under test.

Property based testing moves away from concrete examples and instead checks that certain properties hold true for all possible inputs. It does this by automatically generating a random sample of valid inputs from the possible values.

This can be a good way to uncover bad assumptions made by you and your code.

If the word "random" is making you feel a little nervous, don't worry QuickTheories provides ways to keep your tests repeatable.

Quick Start

Add the QuickTheories jar to your build (see the badge at the top of the page for the maven coordinates of the latest version).

You can run QuickTheories from JUnit, TestNG or any other test framework.

Here we are using JUnit

import static org.quicktheories.QuickTheory.qt;
import static org.quicktheories.generators.SourceDSL.*;

public class SomeTests {

  @Test
  public void addingTwoPositiveIntegersAlwaysGivesAPositiveInteger(){
    qt()
    .forAll(integers().allPositive()
          , integers().allPositive())
    .check((i,j) -> i + j > 0); 
  }

}

The static import org.quicktheories.QuickTheory.qt provides access to the QuickTheories DSL.

The static import org.quicktheories.generators.SourceDSL.* provides access to a DSL that allows valid inputs to be defined.

This property looks pretty simple, it just checks that adding two integers always produces a number greater than 0.

This couldn't possibly fail could it? That would mean math was broken.

If we run this test we get something like :-

java.lang.AssertionError: Property falsified after 1 example(s) 
Smallest found falsifying value(s) :-
{840226137, 1309274625}
Other found falsifying value(s) :- 
{848253830, 1320535400}
{841714728, 1317667877}
{840894251, 1310141916}
{840226137, 1309274625}
 
Seed was 29678088851250	

The falsified theory has highlighted something that we forgot.

Math works just fine, but in Java integers can overflow.

Without static imports

If you prefer the QuickTheories entry points can be brought into scope by implementing an interface, removing the need for static imports.

public class SomeTests implements WithQuickTheories {

  @Test
  public void addingTwoPositiveIntegersAlwaysGivesAPositiveInteger(){
    qt()
    .forAll(integers().allPositive()
          , integers().allPositive())
    .check((i,j) -> i + j > 0); 
  }

}

Less verbose

The source DSL reads nicely but can be a little verbose. Most of the core generators can also be accessed by importing org.quicktheories.generators.Generate. This provides simple static methods that return generators of core types.

import static org.quicktheories.generators.Generate.*;

@Test
public void someProperty() {
  qt()
  .forAll(range(1, 102), constant(7))
  .check((i,c) -> i + c >= 7);
}

Shrinking

QuickTheories supports shrinking.

This means that it doesn't just find a falsifying value and stop. Instead it will try to find other smaller (or "simpler") values that also invalidate the theory.

By default QuickTheories will spend about 100 times more effort looking for smaller values than it did looking for the original falsifying value.

The smallest found value is reported along with a sample of any other falsifying values found along the way.

There is no guarantee that this is the smallest possible falsifying value or that others don't exist. Generally the shrunk values will be easier to understand and work with than the original un-shrunk ones – patterns might be visible in the reported values.

Unlike straight QuickCheck clones QuickTheories does not require you to supply your own shrinking implementation for each type. Shrinking is performed automatically for any and all types. The mechanism by which this is achieved does not make any assumptions about the structure or implementation of the type or break encapsulation.

Seeds and repeatable tests

At the end of the report the Seed is reported.

This is the value from which all randomness is derived in QuickTheories.

By default it is set to the System.nanoTime() so the values will be different each time QuickTheories is run, however the seed can also be set explicitly so runs can be reproduced and deterministic.

Whenever a property is falsified the seed used is reported so you can always reproduce the exact same run.

It is therefore always possible to recreate a run, and you can opt for a fully deterministic behaviour by using a single fixed seed.

Two methods are provided to set the seed.

Directly using the DSL

  qt()
  .withFixedSeed(0)
  .forAll( . . .)

Or using the QT_SEED system property.

The same tests can therefore be run with a fixed seed for the purpose of catching regression, or with a changing seed so that falsifying values are constantly being searched for.

Assertions

Our example theory used a simple predicate, but sometimes it would be nice to take advantage of the functionality provided by assertion libraries such as assertj and hamcrest.

This can be done using the checkAssert method.

  @Test
  public void someTheory() {
    qt().forAll(longs().all())
        .checkAssert(i -> assertThat(i).isEqualsTo(42));
  }

Any block of code that returns void can be passed to checkAssert. Any unchecked exception will be interpreted as falsifying the theory.

Assumptions

As we've seen we can create theories from a pair of Gens - which produce a pair of values.

In fact we can create theories about any number of values between 1 and 4.

   @Test
  public void someTheoryOrOther(){
    qt()
    .forAll(integers().allPositive()
          , strings().basicLatinAlphabet().ofLengthBetween(0, 10)
          , lists().allListsOf(integers().all()).ofSize(42))
    .check((i,s,l) -> l.contains(i) && s.equals(""));
  }

In the example above we use three Gens, as you can see QuickTheories provides ways of generating most common Java types.

A Gen is just a simple function from a random number generator to a value. As we can see, the DSL provides a way to put constraints on the values we generate (e.g we will only generate positive integers and the lists in this example will only be of size 42).

Whenever possible you should use the DSL to provide constraints, but sometimes you might need to constrain the domain in ways that cannot be expressed with the DSL.

When this happens use assumptions.

  @Test
  public void someTheoryOrOther(){
    qt()
    .forAll(integers().allPositive()
          , strings().basicLatinAlphabet().ofLengthBetween(0, 10)
          , lists().allListsOf(integers().all()).ofSize(42))
    .assuming((i,s,l) -> s.contains(i.toString())) // <-- an assumption
    .check((i,s,l) -> l.contains(i) && s.contains(i.toString()));
  }

Assumptions further constrain the values which form the subject of the theory.

Although we could always replace the constraints we created in the DSL with assumptions, this would be very inefficient. QuickTheories would have to spend a lot of effort just trying to find valid values before it could try to invalidate a theory.

As difficult to find values probably represent a coding error, QuickTheories will throw an error if less than 10% of the generated values pass the assumptions:

  @Test
  public void badUseOfAssumptions() {
    qt()
    .forAll(integers().allPositive())
    .assuming(i -> i < 30000)
    .check( i -> i < 3000);
  }

Gives

java.lang.IllegalStateException: Gave up after finding only 107 example(s) matching the assumptions
	at org.quicktheories.quicktheories.core.ExceptionReporter.valuesExhausted(ExceptionReporter.java:20)

(Note: this assumption could have been replaced by the following:

   @Test
  public void goodUseOfSource(){
    qt().forAll(integers().from(1).upTo(30000))
    .check( i -> i < 3000);
  }

Which gives the following failure message: )

java.lang.AssertionError: Property falsified after 1 example(s) 
Smallest found falsifying value(s) :-
3000
Other found falsifying value(s) :- 
13723
13722
13721
13720
13719
13718
13717
13716
13715
13714
 
Seed was 2563360080237

Gens

It is likely that you will want to construct instances of your own types. You could do this within each check, but this would result in a lot of code duplication.

Instead you can define a conversion function. This can be done inline, or placed somewhere convenient for reuse.

  @Test
  public void someTheoryOrOther(){
    qt()
    .forAll(integers().allPositive()
          , integers().allPositive())
    .as( (width,height) -> new Widget(width,height) ) // <-- convert to our own type here
    .check( widget -> widget.isValid());
  }

This works well for simple cases, but there are two problems.

1. We cannot refer to the original width and height integers in our theory. So we couldn't (for example) check that the widget had the expected size.
2. If our widget doesn't define a toString method it is hard to know what the falsifying values were

Both of these problems are solved by the asWithPrecursors method

`