Module proper_target

This module defines the top-level behaviour for Targeted Property-Based Testing (TPBT).

Copyright © 2017-2023 Andreas Löscher and Kostis Sagonas

Version: Jul 24 2025 02:02:43

Behaviours: gen_server.

This module defines the proper_target behaviour.
Required callback functions: init_strategy/1, init_target/2, next/2, get_shrinker/2, update_fitness/3, reset/2.

Authors: Andreas Löscher.

Description

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 (or minimize).

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:

      prop_target() ->                 % Try to check that
        ?EXISTS(Input, Params,         % some input exists
                begin                  % 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.
                end)).

Macros

?MAXIMIZE(UV)
This tells the search strategy to maximize the value UV.
?MINIMIZE(UV)
equivalent to ?MAXIMIZE(-UV)
?USERNF(Gen, Nf)
This uses the neighborhood function Nf instead of PropEr's constructed neighborhood function for this generator. The neighborhood function Fun should be of type fun(term(), {Depth :: pos_integer(), Temperature::float()} -> term()
?USERMATCHER(Gen, Matcher)
This overwrites the structural matching of PropEr with the user provided Matcher function. the matcher should be of type proper_gen_next:matcher()

Data Types

fitness()

fitness() = number()

fitness_fun()

fitness_fun() = fun((target_state(), fitness()) -> target_state()) | none

mod_name()

mod_name() = atom()

next_fun()

next_fun() = fun((...) -> next_fun_ret())

next_fun_ret()

next_fun_ret() = proper_types:type() | proper_gen:instance()

opts()

opts() = #{search_steps := search_steps(), search_strategy := strategy(), atom() => term()}

search_steps()

search_steps() = pos_integer()

strategy()

strategy() = mod_name()

strategy_data()

strategy_data() = term()

target_state()

target_state() = term()

Function Index

cleanup_strategy/0Cleans up proper_gen_next as well as stopping the gen_server.
get_shrinker/1Get the shrinker for a Type.
init_strategy/1Initializes targeted gen server based on a search strategy.
init_target/1Initialize the target of the strategy.
reset/0Reset the strategy target and data to a random initial value.

Function Details

cleanup_strategy/0

cleanup_strategy() -> ok

Cleans up proper_gen_next as well as stopping the gen_server.

get_shrinker/1

get_shrinker(Type::proper_types:type()) -> proper_types:type()

Get the shrinker for a Type.

init_strategy/1

init_strategy(X1::opts()) -> ok

Initializes targeted gen server based on a search strategy.

init_target/1

init_target(RawType::proper_types:type()) -> ok

Initialize the target of the strategy.

reset/0

reset() -> ok

Reset the strategy target and data to a random initial value. Useful when the generated instances differ from the target, depending on the problem.


Generated by EDoc