Module proper_symb

Symbolic datatypes handling functions.

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

Version: Jun 20 2016 16:27:12

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

abstract datatype: symb_term()

var_id()

var_id() = atom() | pos_integer()

var_values()

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

Function Index

defined/1Returns true if the SymbTerm symbolic instance can be successfully evaluated (its evaluation doesn't raise an error or exception).
eval/1Equivalent to eval([], SymbTerm).
eval/2Intended for use inside the property-testing code, this function evaluates a symbolic instance SymbTerm.
pretty_print/1Equivalent to pretty_print([], SymbTerm).
pretty_print/2Similar in calling convention to eval/2, but returns a string representation of the call sequence SymbTerm instead of evaluating it.
well_defined/1An 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, Jun 20 2016, 16:27:12.