Introduction to Targeted Properties

What is a targeted property?

So far, the properties we have written have been rather tightly coupled with generators, since by needing to write specific properties, we tend to need specific generators. More general generators tend to be more useful when we do broader scanning rather than intricate validation, and so we rarely can have just one generator that can do it all.

This is necessary because we need to control randomness to some extent. In this chapter, we’ll learn about targeted properties. They let us use generic generators and specialize them from within the property so that they generate data more relevant to the property.

Understanding targeting properties

Regular properties work by using generators to create random data for each iteration of a test, running some checks, and then seeing if it works for all inputs. Inputs for each iteration are mostly independent. The framework scales the size element of generation between each one. If we want the data generated to be diverse and relevant, we have to use metrics to tweak the generator by hand. By comparison, targeted properties operate with a different principle: each iteration of a property can be used to influence later iterations’ data generation. Even better, the property itself can give feedback to PropEr telling it whether things are headed in the right direction.

This is a bit abstract, so let’s make things practical.

What targeted properties look like

In appearances, targeted properties are fairly similar to regular properties. Instead of using the ?FORALL(Pattern, Generator, Property) macro, we just have to use the ?FORALL_TARGETED(Pattern, Generator, Property) macro.

Let’s try them. First, we’ll write a simple path generator that we can use to create sequences of directions. It is defined as the path generator at line 5 in the code below.

It’s going to be pretty random, going in any direction. Let’s write a property with the new macro, one that should always pass. This property is defined as prop_path in the code below.

The move function just enacts each movement on a {X,Y} coordinate system, where -X goes to the left, +X to the right. Similarly, -Y is to the bottom, and +Y is to the top. By applying it in every direction, we can get a general feeling for all the travel done by a path. The path [left, top, left, top] should return {-2,2}, and a path such as [top,down,left,right] would come back to {0,0}.

If we run this property, we’ll see that most of the paths tend to average to the {0,0} coordinates.