# PropCheck.TargetedPBT (PropCheck v1.4.1) View Source

This module defines the top-level behaviour for targeted property-based testing (TPBT). Using TPBT the input generation is no longer random, but guided by a search strategy to increase the probability of finding failing input. For this to work the user has to specify a search strategy and also needs to extract utility-values from the system under test that the search strategy then tries to maximize.

To use TPBT the test specification macros `forall_targeted`

, `exists`

, and `not_exists`

are used.
The typical structure for a targeted property looks as follows:

```
property prop_target do # Try to check that
exists input <- params do # some input exists that fulfills the property.
uv = sut.run(input) # Do so by running SUT with input
maximize(uv) # and maximize its utility value
uv < threshold # up to some threshold, the property condition.
end
end
```

## Some thoughts on strategies how to use targeted properties

Targeted PBT is a rather new technology and really fascinating. But when should you to use it and when are the classical technologies more suitable? Here are some thoughts on that topic based on the limited experience we currently have.

If you want to test interesting parts of your algorithms or data structures, you would typically invest
into more elaborated generators. If you are working on binary trees and you need more lefty trees, then a new
generator is required that somehow generates trees of that particular shape. The big advantage here is that
you can use all of the standard functions and macros, in particular for collecting statistics about the quality
of the generated data (e.g. by `PropCheck.collect/2`

and its friends).

Another approach would be to use targeted properties
as shown in `targeted_tree_test.exs`

: You use a rather simple data generator and define a measuring function
on the data to express the "leftiness" of the tree. Equiped with that, a target property searches automatically
for data the maximizes (or minimizes) the measuring function (often called utility value or function). Not
inventing a clever data generators comes with a price - there is no free lunch...

- You need some
*relevant*property of your generated data which you can measure, i.e. you need a function from your data to the real numbers. This is not always possible. - Searching for an optimum takes more time than simply generating random data: the run-time of the properties increases.
- Data collecting functions and macros such as
`PropCheck.collect/2`

are currently not available. This it the reason why in`targeted_tree_test.exs`

we use print-outs to show and verify the generated data. - Counter examples and shrinking are not available
- The current implementation in PropEr does not work well together with recursive data generators, which renders the approach unusable for state-based PBT.

But, of course, you gain also something. You can use rather straight data generators and let the searching algorithm find the interesting parts with respect to the measuring function.

In `level_tpbt_test.exs`

a very different approach is used. Here the basic idea is to verify that a data
structure (here: a maze in a computer game) has a proper structure (here: there exists at least one valid
path from the entrance to the exit of the maze). The function to minimize is the distance from the end of
the path to the exit position. The searching algorithm then optimizes the path length for a minimal
distance until the exit is found. For more complex mazes, it is required to adopt the amount of `search_steps`

and the `neighbor_hood`

function to find the exit. They takes over the role `numtests`

and `resize`

to
enlarge or refit the generated data for the next search step.

You can combine approaches by using a classical generator for e.g. generating a new maze, and then use inside a targeted property to find a path to the maze's exit. This would be roughly like this:

```
forall maze <- maze_generator() do
exists p <- path_generator() do
pos = Maze.follow_path(maze, maze.entry_pos, p)
uv = distance(pos, maze.exit_pos)
minimize(uv)
pos == maze.exit_pos
end
end
```

## How the targeted properties relate

The targeted macros `forall_targeted`

, `exists`

and `not_exists`

are related to each other.
The universal laws of quantors from first-order logic apply here as well (cf.
provable entities in first-order logic)
and explain why some conditions in the test examples are constructed the way they are.

In the following, we use the variable `x`

, the generator `x_gen()`

and a boolean predicate `p()`

. The
term `<==>`

means that the expression on both sides are equivalent.

```
forall_targeted x <- x_gen(), do: p(x)
<==> not_exists x <- x_gen(), do: not(p(x))
exists x <- x_gen(), do: p(x)
<==> forall_targeted x <- x_gen(), do: not(p(x))
|> fails()
not_exists x <- x_gen(), do: p(x)
<==> forall_targeted x <- x_gen(), do: not(p(x))
```

## Options

For targeted properties exists a new option:

`{:search_steps, non_negative_number}`

<br> takes an integer defining how many search steps the searching algorithm takes. Its default value is`1_000`

. The effect of`search_steps`

is similar to`num_tests`

for ordinary properties.`num_tests`

has no effect on the search strategy. This helps when you combine a regular property with search strategy, e.g. generating a configuration parameter and search for specific properties to hold depending on that parameter.

Some of the documentation is taken directly from PropEr.

# Link to this section Summary

## Functions

The `exists`

macro uses the targeted PBT component of PropEr to try
to find one instance of `xs`

that makes the `prop`

return `true`

.

The `forall_targeted`

macros uses the targeted PBT component of PropEr to try
that all instances of `xs`

fulfill property `prop`

.

This macro tells the search strategy to maximize the value `fitness`

.

This macro tells the search strategy to minimize the value `fitness`

and
is equivalent to `maximize(-fitness)`

.

The `not_exists`

macro uses the targeted PBT component of PropEr to try
to find one instance of `xs`

that makes the `prop`

return `false`

.

This overwrites the structural matching of PropEr for the generator with the user provided
`matcher`

function.

This uses the neighborhood function `nf`

instead of PropEr's
constructed neighborhood function for this generator.

# Link to this section Functions

The `exists`

macro uses the targeted PBT component of PropEr to try
to find one instance of `xs`

that makes the `prop`

return `true`

.

If such a `xs`

is found, the property passes. Note that there is no counterexample if no
such `xs`

could be found.

The `forall_targeted`

macros uses the targeted PBT component of PropEr to try
that all instances of `xs`

fulfill property `prop`

.

In contrast to `exists`

, often the property here is negated.

This macro tells the search strategy to maximize the value `fitness`

.

This macro tells the search strategy to minimize the value `fitness`

and
is equivalent to `maximize(-fitness)`

.

The `not_exists`

macro uses the targeted PBT component of PropEr to try
to find one instance of `xs`

that makes the `prop`

return `false`

.

If such a `xs`

is found the property passes. Note that there is no counterexample if no
such `xs`

could be found.

This overwrites the structural matching of PropEr for the generator with the user provided
`matcher`

function.

The `matcher`

should be of type `:proper_gen_next.matcher()`

This uses the neighborhood function `nf`

instead of PropEr's
constructed neighborhood function for this generator.

The neighborhood function `nf`

should be of type
`fun(any(), {Depth :: number(), Temperature::float()} -> any()`