It’s been 3 months that I tried to shed some light on the importance of shrinking failed properties. Now that we’ve covered many of the technicalities of the approach it’s time to occupy with how to use PBT in practice.

Patterns to Find Good Properties

When you’re taking your early steps with PBT finding suitable properties can feel like an almost impossible task. Whereas examples often appear naturally when thinking and talking about the functionality of a system, properties are often more abstract. They require a different kind of thinking. A set of useful patterns for finding properties would come in handy.

Luckily, we do not have to discover all things on our own. PBT has been around for a while and there is a small but well known collection of Property-based Testing Patterns. My personal list is certainly incomplete, and apart from the first one I’ve stolen all names elsewhere:

Let’s dive into more details and a bit of code for some of the patterns…

Pattern: Business Rule as Property

Consider this business rule, which could be directly from a domain expert’s written specification:

For all customers with last year’s sales volume above 5000 EUR we will provide an additional discount of 5 percent, if the invoice’s total amount is equal or above 500 EUR.

You could, for example, split this discount rule into two properties:

@Property
@Label("High volume customer discount is 5% for total above 500 EUR")
boolean highVolumeCustomerDiscount(@ForAll Euro lastYearVolume, @ForAll Euro invoiceTotal) {
    Assume.that(lastYearVolume.compareTo(Euro.amount(5000)) > 0);
    Assume.that(invoiceTotal.compareTo(Euro.amount(500)) >= 0);

    return new DiscountCalculator().discountInPercent(lastYearVolume, invoiceTotal)
        .equals(new Percent(5));
}

@Property
@Label("No discount for low volume customer or total below 500 EUR")
boolean noDiscount(@ForAll Euro lastYearVolume, @ForAll Euro invoiceTotal) {
    Assume.that(
        lastYearVolume.compareTo(Euro.amount(5000)) <= 0 ||
        invoiceTotal.compareTo(Euro.amount(500)) < 0
    );

    return new DiscountCalculator().discountInPercent(lastYearVolume, invoiceTotal)
        .equals(new Percent(0));
}

These properties are on a micro testing level; the customer itself with their transactions of last year and their current order does not show up at all. Instead we check the property against an exposed discount calculating function which only takes the necessary values as input.

You might also consider to verify the business rule with similar properties using integrated testing filling a real user database, creating transaction histories and an invoice referring to an order for a set of items in your inventory store. Keep in mind, however, that integrated property testing has the same drawbacks as integrated example testing: High setup costs, slower execution, increased non-determinism and low precision. In addition, you have to multiply the individual runtime by the number of checks: If a single integrated check takes one second, 1000 runs of this check will take more than 15 minutes.

Pattern: Inverse Functions

You have already seen an example of this pattern. In the second episode we checked JDK’s Collections.reverse() method. Reverse is a special case since it is its own inverse function.

Let’s therefore try something else, namely URLEncoder.encode and URLDecoder.decode. Both functions take a string to en/decode and the name of a charset as arguments. The property method to check the “invertibility” of encoding any string with any charset is fairly simple:

@Property
void encodeAndDecodeAreInverse(
        @ForAll @StringLength(min = 1, max = 20) String toEncode,
        @ForAll("charset") String charset
) throws UnsupportedEncodingException {
    String encoded = URLEncoder.encode(toEncode, charset);
    assertThat(URLDecoder.decode(encoded, charset)).isEqualTo(toEncode);
}

@Provide
Arbitrary<String> charset() {
    Set<String> charsets = Charset.availableCharsets().keySet();
    return Arbitraries.of(charsets.toArray(new String[charsets.size()]));
}

What surprised me - and might surprise you: Decode is NOT an inverse function of encode for all charsets:

org.opentest4j.AssertionFailedError:
  Expecting:
   <"?">
  to be equal to:
   <"€">
  but was not.

                              |-----------------------jqwik-----------------------
tries = 13                    | # of calls to property
checks = 13                   | # of not rejected calls
generation-mode = RANDOMIZED  | parameters are randomly generated
after-failure = SAMPLE_FIRST  | try previously failed sample, then previous seed
seed = 4002273756594553579    | random seed to reproduce generated values
sample = ["€", "Big5"]
original-sample = ["⹡骞ḅ遈㻴謯갨㩌셖觯蔊⁕ṏ舰眸鿾꫆閨֒渺", "x-IBM1364"]

Even a standard character like ‘€’ cannot be reliably encoded in all charsets!

Pattern: Induction

Those of you with a bit of formal mathematical education are familiar with the term complete induction. While mathematical induction is used as a technique to proof theorems we can use a related approach to formulate functional domain properties without duplicating the logic under examination in our tests.

I’ll use Sorting a List of Integers as example:

Here’s the equivalent code:

class SortingProperties {

	@Property
	boolean sortingAListWorks(@ForAll List<Integer> unsorted) {
		return isSorted(sort(unsorted));
	}

	private boolean isSorted(List<Integer> sorted) {
		if (sorted.size() <= 1) return true;
		return sorted.get(0) <= sorted.get(1) //
				&& isSorted(sorted.subList(1, sorted.size()));
	}

	private List<Integer> sort(List<Integer> unsorted) {
		unsorted.sort((a, b) -> a > b ? 1 : -1);
		return unsorted;
	}
}

Mind that this property actually does check a desired functional quality of List.sort. In this case we might even consider to forgo example-based testing completely.

Next Episode

In the forthcoming article I will have a closer look at Stateful Testing, which is well suited to be tackled by Property-Based-Testing ideas.

Update

As a reaction to this blog post, Dierk König suggested additional patterns: