# Module proper_symb

- Description
- Data Types
- Function Index
- Function Details

Symbolic datatypes handling functions.

Copyright © 2010-2021 Manolis Papadakis, Eirini Arvaniti, and Kostis Sagonas

Authors: Manolis Papadakis.

## Description

Symbolic datatypes handling functions.

### Symbolic datatypes

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 construct 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 `-spec`ed 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 `?FORALL`s.

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 `?FORALL`s (`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 currently 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.

### pretty_print/1

    pretty_print(SymbTerm :: symb_term()) -> string()

Equivalent to `pretty_print([], SymbTerm)`.

### pretty_print/2

    pretty_print(VarValues :: var_values(), SymbTerm :: symb_term()) ->
                    string()

Similar in calling convention to `eval/2`, but returns a string representation of the call sequence `SymbTerm` instead of evaluating it.

### well_defined/1

    well_defined(SymbType :: proper_types:raw_type()) ->
                    proper_types:type()

An attribute which can be applied to any symbolic generator `SymbType` that may produce invalid sequences of operations when called. The resulting generator is guaranteed to only produce well-defined symbolic instances.

Generated by EDoc