Copyright © 2017 Andreas Löscher and Kostis Sagonas
Version: Dec 31 2021 22:34:16
Authors: Andreas Löscher.
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)).
?MAXIMIZE(UV)
UV
.?MINIMIZE(UV)
?MAXIMIZE(-UV)
?USERNF(Gen, Nf)
Nf
instead of PropEr's
constructed neighborhood function for this generator. The neighborhood
function Fun
should be of type proper_gen_next:nf()
?USERMATCHER(Gen, Matcher)
Matcher
function. the matcher should be of type proper_gen_next:matcher()
fitness() = number()
fitness_func() = fun((target_state(), fitness()) -> target_state()) | none
key() = nonempty_string() | reference()
next_func() = fun((target_state()) -> {target_state(), any()})
strategy() = module()
----------------------------------------------------------------------------- proper_target callback functions for defining strategies ----------------------------------------------------------------------------
target() = {target_state(), next_func(), fitness_func()}
target_state() = term()
tmap() = #{atom() => term()}
init_strategy/1 | |
strategy/0 |
init_strategy(Strat :: strategy()) -> ok
strategy() -> strategy()
Generated by EDoc