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 Propertybased Testing Patterns. My personal list is certainly incomplete, and apart from the first one I’ve stolen all names elsewhere:

Business Rule as Property (aka Obvious Property)
Sometimes the domain specification itself can be interpreted and written as a property.

Fuzzying
Code should never explode, even if you feed it with lots of diverse and unforeseen input data. Thus, the main idea is to generate the input, execute the function under test and check that:
 No exceptions occur, at least no unexpected ones
 No 5xx return codes in http requests, maybe you even require 2xx all the time
 All return values are valid
 Runtime is under an acceptable threshold
 Using the same input several times will produce the same outcome
Fuzzying is often done in retrospect when you want to examine the robustness of existing code. It’s also more common in integrated testing since during micro or unit testing you can usually be more specific than just demanding “Don’t blow up!”.

Inverse Functions
If a function has an inverse function, then applying function first and inverse second should return the original input.

Idempotent Functions
The multiple application of an idempotent function should not change results. Ordering a list a second time, for example, shouldn’t change it anymore.

Invariant Functions
Some properties of our code do not change after applying our logic. For example:
 Sorting and mapping should never change the size of a collection.
 After filtering out some values, the remaining values should still be in the original order.
 When you use stateful objects in sets or as keys in maps, whatever you do with them should never change their hash value.

Commutativity
If a set of functions is commutative, change of order in applying the functions should not change the final result. Think of sorting then filtering should have the same effect as filtering then sorting.

Test Oracle
Sometimes we know of an alternative implementation for our function or algorithm which is called a test oracle. In this case any result of using the function should be the same for both original and alternative. There are a few sources where the alternatives can come from:
 Simple and slow versus complicated but fast
 Parallel versus singlethreaded
 Selfmade versus commercial
 Old (prerefactoring) versus new (postrefactoring)

Hard to compute, easy to verify (aka Blackbox Testing)
Some logic is hard to execute but easy to check. Consider e.g. the effort for finding prime numbers versus checking a prime number.

Induction: Solve a smaller problem first
You might be able to divert your domain check in a base case and a general rule derived from that base case.

Stateful Testing
Especially in the OO world, an object’s behaviour can often (partially) be described as a state machine with a finite set of states and actions to move from state to state. Exploring the space of transitions is an important use case for PBT, that’s why I will dedicate a later article to it.
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 nondeterminism 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:
timestamp = 20180716T11:32:45.021,
seed = 1207350373430593188,
originalSample = ["萸偟쌴穎䀝珣亂兝뢏", "ISO2022JP2"],
sample = ["", "Big5"]
org.junit.ComparisonFailure: expected:<"[]"> but was:<"[?]">
Expected :""
Actual :"?"
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:
 Our base case is simple: Lists of length 1 or below are always sorted.
 The rule for larger lists is also straightforward: A list is sorted when its first element is smaller than its second element and when the list without the first element is also sorted.
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 examplebased
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 PropertyBasedTesting ideas.
Update
As a reaction to this blog post, Dierk König suggested additional patterns:

PureFunction
Check that multiple calls with same arguments produce the same result

Corridor
Check that the returned value of a function or metho call is in its required range

Rules
Test associativity, commutativity, symmetry, neutrality, transitivity where applicable