Property Based Testing with Javaslang

Usual unit testing is based on examples: We define the input for our unit and check for an expected output. Thus, we can ensure that for a specific sample our code works right. However, this does not prove the correctness for all possible inputs. Property based testing, also called property checking, takes another approach by adhering to the scientific theory of Falsifiability: As long as there is no evidence that a proposed property of our code is false, it is assumed to be true. In this article we are using Javaslang's API for property based testing to verify a simple FizzBuzz implementation.

Before We Start

I am using Javaslang Streams to generate an infinite FizzBuzz sequence which should satisfy certain properties. Compared with Java 8 Streams, the main benefit in the scope of this article is that the Javaslang variant provides a good API to retrieve individual elements with the get function.

Property Based Testing

Property based testing (PBT) allows developers to specify the high-level behaviour of a program in terms of invariants it should fullfill. A PBT framework creates test cases to ensure that the program runs as specified.

A property is the combination of an invariant with an input values generator. For each generated value, the invariant is treated as a predicate and checked whether it yields true or false for that value.

As soon as there is one value which yields false, the property is said to be falsified and checking is aborted. If a property cannot be falsified after a specific amount of sample data, the property is assumed to be satisfied.

Reverse List Example

Take a function that reverses a list as an example. It has several implicit invariants that must hold in order to provide proper functionality. One of them is, that the first element of a list is the last element of the same list reversed. A corresponding property combines this invariant with a generator which generates lists with random values and lengths.

Asssume, that the generator generates the following input values: [1,2,3], ["a","b"] and [4,5,6]. The list reverse function returns [3,2,1] for [1,2,3]. The first element of the list is the last elment of the same list reversed. The check yields true. The list reverse funcion returns ["a", "b"] for ["a", "b"]. The first element of the list is not the last element of the same list reversed. The check yields false. The property is falsified.

In Javaslang the default amount of tries to falisfy a property is 1000.

Property Checking FizzBuzz

FizzBuzz is a child's play counting from 1 on. Each child in turn has to say the current number out loud. If the current number is divisble by 3 the child should say "Fizz", if it is divisble by 5 the answer should be "Buzz" and if it is divisble by both 3 and 5 the answer should be "FizzBuzz". So the game starts like this:

1, 2, Fizz, 4, Buzz, Fizz, 7, 8, Fizz, Buzz, 11, Fizz, 13, 14, FizzBuzz, ...

FizzBuzz is often taken as a sample exercise in job interviews where applicants should fizzbuzz the numbers from 1 to 100. FizzBuzz can also be used as a Kata simple enough to focus on the surroundings like language, libraries or tooling instead of the business logic.

A stream seems to be a good way to model FizzBuzz. We will start with an empty one and gradually improve it to pass our tests.

public Stream<String> fizzBuzz() {
    Stream.empty();
}

Every Third Element Should Start with Fizz

From the description of FizzBuzz we can derive a first property about the FizzBuzz Stream: Every third element should start with Fizz. Javaslang's property checking implementation provides fluent APIs to create generators and properties.

@Test
public void every_third_element_starts_with_Fizz) {
    Arbitrary<Integer> multiplesOf3 = Arbitrary.integer()
        .filter(i -> i > 0)
        .filter(i -> i % 3 == 0);

    CheckedFunction1<Integer, Boolean> mustStartWithFizz = i ->
        fizzBuzz().get(i - 1).startsWith("Fizz");

    CheckResult result = Property
        .def("Every third element must start with Fizz")
        .forAll(multiplesOf3)
        .suchThat(mustStartWithFizz)
        .check();

    result.assertIsSatisfied();
}

Let's go through it one by one:

• Arbitrary.integer() generates arbitrary integers which are filtered for positive multiples of 3 using filter.
• The function mustStartWithFizz is the invariant: For a given index, the corresponding element in the stream (get is 0-indexed) must start with Fizz. The call to suchThat further below requires a CheckedFunction1, which is like a function but may throw a checked exception (something we do not need here).
• Property::def takes a short description and creates a Property. The call to forAll takes an Arbitrary and ensures that the invariant in suchThat must hold for all input values generated by the Arbitrary.
• The check function uses the generator to create multiples of 3 in the range from 0 to 100. It returns a CheckResult which can be queried about the result or be asserted.

The property is not satisfied, because for every generated multiple of 3 the corresponding element does not exist in the empty Stream. Let's fix this by providing a suitable stream.

public Stream<String> fizzBuzz() {
    return Stream.from(1).map(i -> i % 3 == 0 ? "Fizz": "");
}

Stream::from creates an infinite stream, which counts from the given number on. Every multiple of 3 is mapped to Fizz. The resulting stream contains a Fizz for every third element. Once we check the property again, it is satisfied and the result is printed on the console:

Every third element must start with Fizz: OK, passed 1000 tests in 111 ms.

Increase the Sample Size

Continue reading %Property Based Testing with Javaslang%

by Gregor Trefs via SitePoint