Module proper_symb

Description
Data Types
Function Index
Function Details

Symbolic datatypes handling functions.

Version: May 19 2021 06:40:23

Authors: Manolis Papadakis.

When writing properties that involve abstract data types, such as dicts or sets, it is usually best to avoid dealing with the ADTs' internal representation directly. Working, instead, with a symbolic representation of the ADT's construction process (series of API calls) has several benefits:

Failing testcases are easier to read and understand. Compare:

         {call,sets,from_list,[[1,2,3]]}

with:

         {set,3,16,16,8,80,48,
              {[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]},
              {{[],[3],[],[],[],[],[2],[],[],[],[],[1],[],[],[],[]}}}

Failing testcases are easier to shrink.
It is especially useful when testing the datatype itself: Certain implementation errors may depend on some particular selection and ordering of API calls, thus it is important to cover the entire ADT construction API.

PropEr supports the symbolic representation of datatypes, using the following syntax:

{call,Module,Function,Arguments}: This represents a call to the API function Module:Function with arguments Arguments. Each of the arguments may be a symbolic call itself or contain other symbolic calls in lists or tuples of arbitrary depth.
{'$call',Module,Function,Arguments}: Identical to the above, but gets evaluated automatically before being applied to a property.
{var,var_id()}: This contruct serves as a placeholder for values that are not known at type construction time. It will be replaced by the actual value of the variable during evaluation.

When including the PropEr header file, all API functions of this module are automatically imported, unless PROPER_NO_IMPORTS is defined.

Auto-ADT

To simplify the symbolic testing of ADTs, PropEr comes with the Auto-ADT subsystem: An opaque native type, if exported from its module, is assumed to be an abstract data type, causing PropEr to ignore its internal representation and instead construct symbolic instances of the type. The API functions used in these symbolic instances are extracted from the ADT's defining module, which is expected to contain one or more -speced and exported functions that can be used to construct instances of the ADT. Specifically, PropEr will use all functions that return at least one instance of the ADT. As with recursive native types, the base case is automatically detected (in the case of ADTs, calls to functions like new/0 and from_list/1 would be considered the base case). The produced symbolic calls will be $call tuples, which are automatically evaluated, thus no call to eval/1 is required inside the property. Produced instances are guaranteed to evaluate successfully. Parametric ADTs are supported, so long as they appear fully instantiated inside ?FORALLs.

ADTs hard-coded in the Erlang type system (array, dict, digraph, gb_set, gb_tree, queue, and set) are automatically detected and handled as such. PropEr also accepts parametric versions of the above ADTs in ?FORALLs (array/1, dict/2, gb_set/1, gb_tree/2, queue/1, set/1, also orddict/2 and ordset/1). If you would like to use these parametric versions in -type and -spec declarations as well, to better document your code and facilitate spec testing, you can include the complementary header file proper/include/proper_param_adts.hrl, which provides the corresponding -type definitions. Please note that Dialyzer currenty treats these the same way as their non-parametric counterparts.

The use of Auto-ADT is currently subject to the following limitations:

In the ADT's -opaque declaration, as in all types' declarations, only type variables should be used as parameters in the LHS. None of these variables can be the special _ variable and no variable should appear more than once in the parameters.
ADTs inside specs can only have simple variables as parameters. These variables cannot be bound by any is_subtype constraint. Also, the special _ variable is not allowed in ADT parameters. If this would result in singleton variables, as in the specs of functions like new/0, use variable names that begin with an underscore.
Specs that introduce an implicit binding among the parameters of an ADT are rejected, e.g.:
```
         -spec foo(mydict(T,S),mydict(S,T)) -> mydict(T,S).
```
This includes using the same type variable twice in the parameters of an ADT.
While parsing the return type of specs in search of ADT references, PropEr only recurses into tuples, unions and lists; all other constructs are ignored. This prohibits, among others, indirect references to the ADT through other custom types and records.
When encountering a union in the return type, PropEr will pick the first choice that can return an ADT. This choice must be distinguishable from the others either by having a unique term structure or by having a unique tag (if it's a tagged tuple).
When parsing multi-clause specs, only the first clause is considered.
The only spec constraints we accept are is_subtype constraints whose first argument is a simple, non-_ variable. It is not checked whether or not these variables actually appear in the spec. The second argument of an is_subtype constraint cannot contain any non-_ variables. Multiple constraints for the same variable are not supported.
Unexported opaques and opaques with no suitable specs to serve as API calls are silently discarded. Those will be treated like ordinary types.
Unexported or unspecced functions are silently rejected.
Functions with unsuitable return values are silently rejected.
Specs that make bad use of variables are silently rejected.

For an example on how to write Auto-ADT-compatible parametric specs, see the examples/stack module, which contains a simple implementation of a stack, or the proper/proper_dict module, which wraps the STDLIB dict ADT.

Data Types

symb_term()

symb_term() = term()

var_id()

var_id() = atom() | pos_integer()

var_values()

var_values() = [{var_id(), term()}]

Function Index

defined/1	Returns true if the `SymbTerm` symbolic instance can be successfully evaluated (its evaluation doesn't raise an error or exception).
eval/1	Equivalent to `eval([], SymbTerm)`.
eval/2	Intended for use inside the property-testing code, this function evaluates a symbolic instance `SymbTerm`.
pretty_print/1	Equivalent to `pretty_print([], SymbTerm)`.
pretty_print/2	Similar in calling convention to `eval/2`, but returns a string representation of the call sequence `SymbTerm` instead of evaluating it.
well_defined/1	An attribute which can be applied to any symbolic generator `SymbType` that may produce invalid sequences of operations when called.

Function Details

defined/1

defined(SymbTerm::symb_term()) -> boolean()

Returns true if the SymbTerm symbolic instance can be successfully evaluated (its evaluation doesn't raise an error or exception).

eval/1

eval(SymbTerm::symb_term()) -> term()

Equivalent to eval([], SymbTerm).

eval/2

eval(VarValues::var_values(), SymbTerm::symb_term()) -> term()

Intended for use inside the property-testing code, this function evaluates a symbolic instance SymbTerm. It also accepts a proplist VarValues that maps variable names to values, which is used to replace any var tuples inside SymbTerm before proceeding with its evaluation.

Generated by EDoc