Overview

Module proper_target

• Description
• Data Types
• Function Index
• Function Details

Copyright © 2017 Andreas Löscher and Kostis Sagonas

Version: Nov 15 2024 16:23:11

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 proper_gen_next:nf()

?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_func()

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

key()

key() = nonempty_string() | reference()

next_func()

next_func() = fun((target_state()) -> {target_state(), any()})

strategy()

strategy() = module()

----------------------------------------------------------------------------- proper_target callback functions for defining strategies ----------------------------------------------------------------------------

target()

target() = {target_state(), next_func(), fitness_func()}

target_state()

target_state() = term()

tmap()

tmap() = #{atom() => term()}

Function Index

Function Details

init_strategy/1

init_strategy(Strat :: strategy()) -> ok

strategy/0

strategy() -> strategy()

Overview

Generated by EDoc