Overview

Module proper_target

• Description
• Data Types
• Function Index
• Function Details

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

Version: May 18 2021 22:41:22

Behaviours: gen_server.

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.

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 fullfills 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

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.

Overview

Generated by EDoc