From d1f16b34c72827924473472778fa075669a8e376 Mon Sep 17 00:00:00 2001 From: eirini Date: Fri, 3 Jun 2011 16:08:05 +0300 Subject: [PATCH] move documentation from README to PropEr modules --- README | 34 ++--- src/proper.erl | 283 ++++++++++++++++++++++++++++++++++++++ src/proper_gen.erl | 6 +- src/proper_symb.erl | 64 +++++++++ src/proper_types.erl | 112 ++++++++++++++- src/proper_typeserver.erl | 128 ++++++++++++++++- 6 files changed, 603 insertions(+), 24 deletions(-) diff --git a/README b/README index 4107795e..7bb44156 100644 --- a/README +++ b/README @@ -68,7 +68,7 @@ Using PropEr under Erlang/OTP R13B03 or older: -------------------------------------------------------------------------------- -Introduction +Introduction -> moved the last paragraph to proper.erl -------------------------------------------------------------------------------- Traditional testing methodologies essentially involve software testers writing a @@ -107,7 +107,7 @@ way to provide tighter integration with Erlang's built-in type system. -------------------------------------------------------------------------------- -How to write properties (test case generators) +How to write properties (test case generators) -> moved to proper.erl -------------------------------------------------------------------------------- The simplest properties that PropEr can test consist of a single boolean @@ -220,7 +220,7 @@ testing modules in the tests directory may also be of interest. -------------------------------------------------------------------------------- -Program behaviour +Program behaviour -> moved to proper.erl -------------------------------------------------------------------------------- When running in verbose mode (this is the default), each sucessful test prints @@ -259,7 +259,7 @@ controls the return value format of proper:module itself (see the -------------------------------------------------------------------------------- -Counterexamples +Counterexamples -> moved to proper.erl -------------------------------------------------------------------------------- A counterexample for a property is represented as a list of terms; each such @@ -305,7 +305,7 @@ to verify that actually corresponds to . -------------------------------------------------------------------------------- -Options +Options -> moved to proper.erl -------------------------------------------------------------------------------- Options can be provided as an extra argument to testing functions exported from @@ -363,7 +363,7 @@ The available options are: -------------------------------------------------------------------------------- -Basic types +Basic types -> moved to proper_types.erl -------------------------------------------------------------------------------- The following basic types are provided: @@ -495,7 +495,7 @@ example of the type of a tagged tuple: {'result', integer()}. -------------------------------------------------------------------------------- -How to construct types +How to construct types -> moved to proper_types.erl -------------------------------------------------------------------------------- The following macros and functions can be applied to types in order to produce @@ -602,7 +602,7 @@ resize(, ) -------------------------------------------------------------------------------- -Native types support +Native types support -> moved to proper_typeserver.erl -------------------------------------------------------------------------------- PropEr can parse types expressed in Erlang's native type format and convert them @@ -711,7 +711,7 @@ The use of native types in properties is subject to the following usage rules: -------------------------------------------------------------------------------- -Spec testing +Spec testing -> moved to proper.erl -------------------------------------------------------------------------------- You can test the accuracy of an exported function's spec by running: @@ -762,7 +762,7 @@ treats these the same way as the non-parametric versions. -------------------------------------------------------------------------------- -Symbolic datatypes +Symbolic datatypes -> moved to proper_symb.erl -------------------------------------------------------------------------------- When writing properties that involve abstract data types, such as dicts or sets, @@ -814,7 +814,7 @@ instances: -------------------------------------------------------------------------------- -Auto-ADT +Auto-ADT -> move to proper_symb.erl -------------------------------------------------------------------------------- To simplify the symbolic testing of ADTs, PropEr comes with the Auto-ADT @@ -877,7 +877,7 @@ proper/proper_dict module, which wraps the STDLIB dict ADT. -------------------------------------------------------------------------------- -Testing stateful code +Testing stateful code -> moved to proper_statem.erl -------------------------------------------------------------------------------- PropEr provides the module proper_statem to facilitate testing of stateful @@ -995,7 +995,7 @@ respectively. -------------------------------------------------------------------------------- -Parallel testing +Parallel testing -> moved to proper_statem.erl -------------------------------------------------------------------------------- After ensuring that a system's behaviour can be described via an abstract state @@ -1042,7 +1042,7 @@ examples/ets_statem, where we test concurrent operations on a public ets table. -------------------------------------------------------------------------------- -PropEr fsm +PropEr fsm -> moved to proper_fsm.erl -------------------------------------------------------------------------------- PropEr provides another useful module for testing stateful systems, in @@ -1155,7 +1155,7 @@ containing a finite state machine specification for an elevator. -------------------------------------------------------------------------------- -Errors +Errors -> moved to proper.erl -------------------------------------------------------------------------------- The following errors may be encountered during testing. The term provided for @@ -1194,7 +1194,7 @@ occurs. Normaly, a message is also printed on screen describing the error. -------------------------------------------------------------------------------- -Demo functions +Demo functions -> moved to proper_gen.erl and proper_typeserver.erl -------------------------------------------------------------------------------- You can use the following functions to try out the random instance generation, @@ -1230,7 +1230,7 @@ for demonstration purposes only. -------------------------------------------------------------------------------- -Incompatibilities with QuviQ's QuickCheck +Incompatibilities with QuviQ's QuickCheck -> moved to proper.erl -------------------------------------------------------------------------------- We have generaly tried to keep PropEr's notation and output as compatible as diff --git a/src/proper.erl b/src/proper.erl index c3a79641..00f21cb5 100644 --- a/src/proper.erl +++ b/src/proper.erl @@ -22,7 +22,16 @@ %%% and Kostis Sagonas %%% @version {@version} %%% @author Manolis Papadakis + %%% @doc This is the main PropEr module. +%%% PropEr is a property-based testing tool, designed to test programs written +%%% in the Erlang programming language. Its focus is on testing the behaviour +%%% of pure functions. On top of that, it is equipped with two library modules +%%% that can be used for testing stateful code. The input domain of functions is +%%% specified through the use of a type system, modeled closely after the type +%%% system of the language itself. Properties are written using Erlang +%%% expressions, with the help of a few predefined macros. Work is currently under +%%% way to provide tighter integration with Erlang's built-in type system. %%% %%% == How to write properties (test case generators) == %%% The simplest properties that PropEr can test consist of a single boolean @@ -77,6 +86,280 @@ %%% any more wrappers.

%%% %%% +%%% Additionaly, there is a wrapper that allows to test a conjunction of +%%% sub-properties, see {@link conjunction/1} for more details. There are also +%%% multiple wrappers that can be used to collect statistics about test case +%%% distribution. See {@link collect/2}, {@link collect/3}, {@link aggregate/2}, +%%% {@link aggregate/3}, {@link classify/3}, {@link measure/3} for more details. +%%% +%%% Last but not least, a property may be wrapped with one or more of the +%%% following outer-level wrappers, which control the behaviour of the testing +%%% subsystem: {@link numtests/2}, {@link fails/2}, {@link on_output/2}. +%%% If the same wrapper appears more than once in a property, the innermost +%%% takes precedence. +%%% +%%% Note that failure of a property may also be signified by throwing an +%%% exception, error or exit. +%%% +%%% For some actual usage examples, see the code in the examples directory. The +%%% testing modules in the tests directory may also be of interest. +%%% +%%% == Program behaviour == +%%% When running in verbose mode (this is the default), each sucessful test +%%% prints a '.' on screen. If a test fails, a '!' is printed, along with the +%%% failing test case (the instances of the types in every `?FORALL') and the +%%% cause of the failure, if it was not simply the falsification of the property. +%%% Then, unless the test was expected to fail, PropEr attempts to produce a +%%% minimal test case that fails the property in the same way. This process is +%%% called shrinking. During shrinking, a '.' is printed for each +%%% successful simplification of the failing test case. When PropEr reaches its +%%% shrinking limit or realizes that the instance cannot be shrunk further while +%%% still failing the test, it prints the minimal failing test case and failure +%%% reason and exits. +%%% +%%% The return value of PropEr can be one of the following: +%%%
    +%%%
  • `true': The property held for all valid produced inputs.
    • +%%%
  • `false': The property failed for some input.
    • +%%%
  • `{error, }': An error occured - see the {@section Errors} +%%% section for a description of possible errors.
    • +%%%
+%%% +%%% You can also run PropEr in pure mode by using {@link proper:pure_check/1} or +%%% {@link proper:pure_check/2} instead of {@link proper:quickcheck/1} and +%%% {@link proper:quickcheck/2}. Under this mode, PropEr will perform no I/O and +%%% will not access the caller's process dictionary in any way. Please note that +%%% PropEr will not actually run as a pure function under this mode. +%%% +%%% To test all properties exported from a module (a property is a 0-arity function +%%% whose name begins with "prop_"), you can use {@link proper:module/1} or +%%% {@link proper:module/2}. This returns a list of all failing properties, +%%% represented by mfas. Testing progress is also printed on screen (unless 'quiet' +%%% mode is active). The provided options are passed on to each property, except for +%%% 'long_result', which controls the return value format of `proper:module' itself +%%% (see the {@section Counterexamples} section). +%%% +%%% == Counterexamples == +%%% A counterexample for a property is represented as a list of terms; each such +%%% term corresponds to the type in a `?FORALL'. The instances are provided in +%%% the same order as the `?FORALL' wrappers in the property, i.e. the instance +%%% at the head of the list corresponds to the outermost `?FORALL' etc. Instances +%%% generated inside a failing sub-property of a conjunction are marked with the +%%% sub-property's tag. +%%% +%%% The last (simplest) counterexample produced by PropEr during a (failing) run +%%% can be retrieved after testing has finished, by running +%%% {@link proper:counterexample/0}. When testing a whole module, run +%%% {@link proper:counterexamples/0} to get a counterexample for each failing +%%% property, as a list of {`mfa()', {@type counterexample()}} tuples. To enable +%%% this functionality, some information has to remain in the process dictionary +%%% even after PropEr has returned. To completely clean up the process dictionary +%%% of PropEr-produced entries, run {@link proper:clean_garbage/0}. +%%% +%%% Counterexamples can also be retrieved by running PropEr in long-result mode, +%%% where counterexamples are returned as part of the return value. Specifically, +%%% when testing a single property under long-result mode (activated by supplying +%%% the option 'long_result', or by calling {@link proper:counterexample/1}, +%%% {@link proper:counterexample/2} instead of {@link proper:quickcheck/1}, +%%% {@link proper:quickcheck/2}). PropEr will return a counterexample in case of +%%% failure (instead of simply returning `false'). When testing a whole module +%%% under long-result mode (activated by supplying the option `long_result' to +%%% {@link proper:module/2}), PropEr will return a list of +%%% {`mfa()', {@type counterexample()}} tuples, one for each failing property. +%%% +%%% You can re-check a specific counterexample against the property that it +%%% previously falsified by running {@link proper:check/2} or +%%% {@link proper:check/3}. This will return one of the following (both in short- +%%% and long-result mode): +%%%
    +%%%
  • `true': The property now holds for this test case.
    • +%%%
  • `false': The test case still fails (although not necessarily for the same +%%% reason as before).
    • +%%%
  • `{error, }': An error occured - see the {@section Errors} +%%% section for a description of possible errors.
    • +%%%
+%%% Proper will not attempt to shrink the input in case it fails the property. +%%% Unless silent mode is active, PropEr will also print a message on screen, +%%% describing the result of the re-checking. Note that PropEr can do very little +%%% to verify that the counterexample actually corresponds to the property that it +%%% is tested against. +%%% +%%% == Options == +%%% Options can be provided as an extra argument to testing functions exported +%%% from the main proper module (such as {@link proper:quickcheck/1}). A single +%%% option can be written stand-alone, or multiple options can be provided in a +%%% list. When two settings conflict, the one that comes first in the list takes +%%% precedence. Settings given inside external wrappers to a property (see the +%%% {@section How to write properties (test case generators)} section) override +%%% any conflicting settings provided as options. +%%% +%%% The available options are: +%%%
    +%%%
  • `quiet' +%%%

    Enables quiet mode - no output is printed on screen while PropEr is +%%% running.

    • +%%%
  • `verbose' +%%%

    Enables verbose mode - this is the default mode of operation.

    • +%%%
  • {`to_file', `'} +%%%

    Redirects all of PropEr's output to `', which should be an IO +%%% device associated with a file opened for writing.

    • +%%%
  • {`on_output', `'} +%%%

    PropEr will use the supplied function for all output printing. This +%%% function should accept two arguments in the style of `io:format/2'.
    +%%% CAUTION: The above output control options are incompatible with each +%%% other.

    • +%%%
  • `long_result' +%%%

    Enables long-result mode (see the {@section Counterexamples} section for +%%% details).

    • +%%%
  • {`numtests', `'} or simply `' +%%%

    This is equivalent to the {@link numtests/1} property wrapper. Any +%%% `numtests/1' wrappers in the actual property will overwrite this setting. +%%%

    • +%%%
  • {`start_size', `'} +%%%

    Specifies the initial value of the `size' parameter (default is 1), see +%%% the {@section PropEr types} section for details.

    • +%%%
  • {`max_size', `'} +%%%

    Specifies the maximum value of the `size' parameter (default is 42), see +%%% the {@section PropEr types} section for details.

    • +%%%
  • {`max_shrinks', `'} +%%%

    Specifies the maximum number of times a failing test case should be +%%% shrunk before returning. Note that the shrinking may stop before so many +%%% shrinks are achieved if the shrinking subsystem deduces that it cannot +%%% shrink the failing test case further. Default is 500.

    • +%%%
  • `noshrink' +%%%

    Instructs PropEr to not attempt to shrink any failing test cases. +%%%

    • +%%%
  • {`constraint_tries', `'} +%%%

    Specifies the maximum number of tries before the generator subsystem +%%% gives up on producing an instance that satisfies a `?SUCHTHAT' constraint. +%%% Default is 50.

    • +%%%
  • `fails' +%%%

    This is equivalent to the {@link fails/1} property wrapper.

    • +%%%
  • {`spec_timeout', `infinity | '} +%%%

    When testing a spec, PropEr will consider an input to be failing if the +%%% function under test takes more that the specified amount of milliseconds +%%% to return for that input.

    • +%%%
  • `any_to_integer' +%%%

    All generated instances of the type {@link proper_types:any/0} will be +%%% integers. This is provided as a means to speed up the testing of specs, +%%% where `proper_types:any/0' is a commonly used type (see the +%%% {@section Spec testing} section for details).

    • +%%%
+%%% +%%% == PropEr types == +%%% For information on basic PropEr types and how to construct new types please +%%% refer to the documentation of the {@link proper_types} module. +%%% +%%% == Native types support == +%%% For information on native types support please refer to the documentation +%%% of the {@link proper_typeserver} module. +%%% +%%% == Spec testing == +%%% You can test the accuracy of an exported function's spec by running +%%% {@link proper:check_spec/1} or {@link proper:check_spec/2}. +%%% Under this mode of operation, PropEr will call the provided function with +%%% increasingly complex valid inputs (according to its spec) and test that no +%%% unexpected value is returned. If an input is found that violates the spec, +%%% it will be saved as a counterexample and PropEr will attempt to shrink it. +%%% +%%% You can test all exported functions of a module against their spec by +%%% running {@link proper:check_specs/1} or {@link proper:check_specs/2}. +%%% +%%% The use of `check_spec' is subject to the following usage rules: +%%%
    +%%%
  • Currently, PropEr can't test functions whose range contains a type +%%% that exhibits a certain kind of self-reference: it is (directly or +%%% indirectly) self-recursive and at least one recursion path contains only +%%% unions and type references. E.g. these types are acceptable: +%%% ``` -type a(T) :: T | {'bar',a(T)}. +%%% -type b() :: 42 | [c()]. +%%% -type c() :: {'baz',b()}.''' +%%% while these are not: +%%% ``` -type a() :: 'foo' | b(). +%%% -type b() :: c() | [integer()]. +%%% -type c() :: 'bar' | a(). +%%% -type d(T) :: T | d({'baz',T}).'''
    • +%%%
  • Throwing any exception or raising an `error:badarg' is considered +%%% normal behaviour. Currently, users cannot fine-tune this setting.
    • +%%%
  • Only the first clause of the function's spec is considered.
    • +%%%
  • The only spec constraints we accept are 1is_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.
    • +%%%
+%%% +%%% PropEr comes with an extra header file, +%%% `proper/include/proper_param_adts.hrl', which contains definitions of +%%% parametric wrappers for some STDLIB ADTs, namely `array/1', `dict/2', +%%% `gb_set/1', `gb_tree/2', `queue/1', `set/1', `orddict/2' and `ordset/1'. By +%%% including this header file, you can use the above parametric types to better +%%% document your code and facilitate spec testing (PropEr automatically +%%% recognizes these types and produces valid instances). Please note that +%%% Dialyzer currenty treats these the same way as the non-parametric versions. +%%% +%%% == Errors == +%%% The following errors may be encountered during testing. The term provided +%%% for each error is the error type returned by proper:quickcheck in case such +%%% an error occurs. Normaly, a message is also printed on screen describing +%%% the error. +%%%
    +%%%
  • `arity_limit' +%%%

    The random instance generation subsystem has failed to produce +%%% a function of the desired arity. Please recompile PropEr with a suitable +%%% value for `?MAX_ARITY' (defined in `proper_internal.hrl'). This error +%%% should only be encountered during normal operation.

    • +%%%
  • `cant_generate' +%%%

    The random instance generation subsystem has failed to +%%% produce an instance that satisfies some `?SUCHTHAT' constraint. You +%%% should either increase the `constraint_tries' limit, loosen the failing +%%% constraint, or make it non-strict. This error should only be encountered +%%% during normal operation.

    • +%%%
  • `cant_satisfy' +%%%

    All the tests were rejected because no produced test case +%%% would pass all `?IMPLIES' checks. You should loosen the failing `?IMPLIES' +%%% constraint(s). This error should only be encountered during normal +%%% operation.

    • +%%%
  • `non_boolean_result' +%%%

    The property code returned a non-boolean result. Please +%%% fix your property.

    • +%%%
  • `rejected' +%%%

    Only encountered during re-checking, the counterexample does not +%%% match the property, since the counterexample doesn't pass an `?IMPLIES' +%%% check.

    • +%%%
  • `too_many_instances' +%%%

    Only encountered during re-checking, the counterexample +%%% does not match the property, since the counterexample contains more +%%% instances than there are `?FORALLs' in the property.

    • +%%%
  • `type_mismatch' +%%%

    The variables' and types' structures inside a `?FORALL' don't +%%% match. Please check your properties.

    • +%%%
  • {`typeserver', `'} +%%%

    The typeserver encountered an error. The `' field contains +%%% specific information regarding the error.

    • +%%%
  • {`unexpected', `'} +%%%

    A test returned an unexpected result during normal operation. If you ever +%%% get this error, it means that you have found a bug in PropEr - please send an +%%% error report to the maintainers and remember to include both the failing test +%%% case and the output of the program, if possible.

    • +%%%
  • {`unrecognized_option', `
    • +%%%
+%%% +%%% == Incompatibilities with QuviQ's QuickCheck == +%%% We have generaly tried to keep PropEr's notation and output as compatible as +%%% possible with QuviQ's QuickCheck, to allow for the reuse of existing testing +%%% code written for QuickCheck. However, incompatibilities are to be expected, +%%% since the two programs probably bear little resemblance under the hood. Here +%%% we provide a nonexhaustive list of known incompatibilities: +%%%
    +%%%
  • `?SUCHTHATMAYBE' behaves differently in PropEr.
    • +%%%
  • `proper_gen:pick' differs from `eqc_gen:pick' in return value format.
    • +%%%
  • PropEr handles `size' differently from QuickCheck.
    • +%%%
  • `proper:module/2' accepts options in the second argument instead of the +%%% first.
    • +%%%
+%%% @end -module(proper). -export([quickcheck/1, quickcheck/2, counterexample/1, counterexample/2, diff --git a/src/proper_gen.erl b/src/proper_gen.erl index 250ba9a5..d1d55bc1 100644 --- a/src/proper_gen.erl +++ b/src/proper_gen.erl @@ -23,7 +23,11 @@ %%% @version {@version} %%% @author Manolis Papadakis %%% @doc The generator subsystem and generators for basic types are contained -%%% in this module. +%%% in this module. You can use the these functions +%%% to try out the random instance generation and shrinking subsystems.
+%%% +%%% CAUTION: These functions should never be used +%%% inside properties. They are meant for demonstration purposes only. -module(proper_gen). -export([pick/1, pick/2, sample/1, sample/3, sampleshrink/1, sampleshrink/2]). diff --git a/src/proper_symb.erl b/src/proper_symb.erl index 04bfb664..25aa7d96 100644 --- a/src/proper_symb.erl +++ b/src/proper_symb.erl @@ -60,6 +60,70 @@ %%% When including the "proper/include/proper.hrl" header file, %%% all API functions of {@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 +%%% definition module, which is expected to contain one or more '-spec'ed +%%% 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 fully supported, +%%% as long as they appear 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'). +%%% +%%% 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. %%% @end -module(proper_symb). diff --git a/src/proper_types.erl b/src/proper_types.erl index 75a340c2..e4cce0d5 100644 --- a/src/proper_types.erl +++ b/src/proper_types.erl @@ -22,8 +22,113 @@ %%% and Kostis Sagonas %%% @version {@version} %%% @author Manolis Papadakis + %%% @doc Type manipulation functions and predefined types are contained in this -%%% module. +%%% module. +%%% +%%% == How to construct types == +%%% The following macros can be applied to basic types in order to produce new +%%% ones: +%%%
    +%%%
  • `?LET(, , )' +%%%

    To produce an instance of this type, all appearances of the variables +%%% in `' inside `' are replaced by their corresponding values in a +%%% randomly generated instance of `'. It's OK for the `' part to +%%% evaluate to a type - in that case, an instance of the inner type is +%%% generated recursively.

    +%%%
    • +%%%
  • `?SUCHTHAT(, , )' +%%%

    This produces a specialization of `', which only includes those +%%% members of `' that satisfy the constraint `' - that is, +%%% those members for which the function `fun() -> end' returns +%%% `true'. If the constraint is very strict - that is, only a small percentage +%%% of instances of `' pass the test - it will take a lot of tries for +%%% the instance generation subsystem to randomly produce a valid instance of +%%% the specialized type. This will result in slower testing - testing may even +%%% be stopped short, in case the `constraint_tries' limit is reached (see the +%%% 'Options' section in {@link proper} module documentation). If this is the +%%% case, it would be more appropriate to generate valid instances of the +%%% specialized type using the ?LET macro. Also make sure that even small +%%% instances can satisfy the constraint, since PropEr will only try small +%%% instances at the start of testing. If this is not possible, you can +%%% instruct PropEr to start at a larger size (`start_size' option - see the +%%% 'Options' section in {@link proper} module documentation for details).

    +%%%
    • +%%%
  • `?SUCHTHATMAYBE(, , )' +%%%

    Equivalent to the `?SUCHTHAT' macro, but the constraint `' is +%%% considered non-strict: if the `constraint_tries' limit is reached, the +%%% generator will just return an instance of `' instead of failing, +%%% even if that instance doesn't satisfy the constraint.

    +%%%
    • +%%%
  • `?SHRINK(, )' +%%%

    This creates a type whose instances are generated by evaluating the +%%% statement block `' (this may evaluate to a type, which is +%%% generated recursively). If an instance of such a type is to be shrunk, +%%% the generators in `' are first run to +%%% produce hopefully simpler instances of the type. Thus, the generators in +%%% the second argument should be simpler than the default. The simplest ones +%%% should be at the front of the list, since those are the generators preferred +%%% by the shrinking subsystem. Like the main `', the alternatives may +%%% also evaluate to a type, which is generated recursively.

    +%%%
    • +%%%
  • `?LETSHRINK(, , )' +%%%

    This is created by combining a `?LET' and a `?SHRINK' macro. Instances +%%% are generated by applying a randomly generated list of values inside +%%% `' (just like a `?LET', with the added constraint that the +%%% variables and types must be provided in a list - alternatively, +%%% `' may be a list or vector type). When shrinking instances of +%%% such a type, the sub-instances that were combined to produce it are first +%%% tried in place of the failing instance.

    +%%%
    • +%%%
  • `?LAZY()' +%%%

    This construct returns a type whose only purpose is to delay the +%%% evaluation of `' (`' can return a type, which will +%%% be generated recursively). Using this, you can simulate the lazy generation +%%% of instances: +%%% ``` stream() -> ?LAZY(frequency([ {1,[]}, {3,[0|stream()]} ])). ''' +%%% The above type produces lists of zeroes with an average length of 3. Note +%%% that, had we not enclosed the generator with a `?LAZY' macro, the evaluation +%%% would continue indefinitely, due to the eager evaluation of the Erlang +%%% language.

    +%%%
    • +%%%
+%%% Additionally, the functions {@link non_empty/1}, {@link noshrink/1}, +%%% {@link with_parameter/3}, {@link with_parameters/2} can be used to add extra +%%% attributes to a type. +%%% +%%% == Size-related issues == +%%% The following functions and macros are related to the `size' parameter, +%%% which controls the maximum size of produced instances. The actual size of +%%% a produced instance is chosen randomly, but can never exceed the value of +%%% the `size' parameter at the moment of generation. A more accurate definition +%%% is the following: the maximum instance of `size S' can never be smaller than +%%% then maximum instance of `size S-1'. The actual size of an instance is +%%% measured differently for each type: the actual size of a list is its length, +%%% while the actual size of a tree may be the number of its internal nodes. +%%% Some types, e.g. unions, have no notion of size, thus their generation is not +%%% influenced by the value of `size'. The `size' parameter starts at `0' and +%%% grows automatically during testing. +%%%
    +%%%
  • `?SIZED(, )' +%%%

    Creates a new type, whose instances are produced by replacing all +%%% appearances of the `' parameter inside the statement block `' +%%% with the value of the `size' parameter. It's OK for the `' to +%%% return a type - in that case, an instance of the inner type is generated +%%% recursively.

    +%%%
    • +%%%
  • `resize(, )' +%%%

    Overrides the `size' parameter used when generating instances of +%%% `' with `'. Has no effect on size-less types, such as +%%% unions. Also, this will not affect the generation of any internal types +%%% contained in `', such as the elements of a list - those will still be +%%% generated using the test-wide value of `size'. One use of this function is +%%% to modify types to grow faster or slower, like so: +%%% ```?SIZED(Size, resize(Size * 2, list(integer()))''' +%%% The above specifies a list type that grows twice as fast as normal lists. +%%%

    +%%%
    • +%%%
+%%% @end -module(proper_types). -export([is_inst/2, is_inst/3]). @@ -1047,10 +1152,7 @@ weighted_default(Default, OtherType) -> %% `RawType' with `NewSize'. It has no effect on size-less types, such as %% unions. Also, this will not affect the generation of any internal types %% contained in `RawType', such as the elements of a list - those will still be -%% generated using the test-wide value of `size'. One use of this function is -%% to modify types to grow faster or slower, like so: -%% ```?SIZED(Size, resize(Size * 2, list(integer()))''' -%% The above specifies a list type that grows twice as fast as normal lists. +%% generated using the test-wide value of `size'. -spec resize(size(), raw_type()) -> proper_types:type(). resize(NewSize, RawType) -> Type = cook_outer(RawType), diff --git a/src/proper_typeserver.erl b/src/proper_typeserver.erl index 933dd02d..66bf914c 100644 --- a/src/proper_typeserver.erl +++ b/src/proper_typeserver.erl @@ -22,8 +22,134 @@ %%% and Kostis Sagonas %%% @version {@version} %%% @author Manolis Papadakis + %%% @doc This module contains the subsystem responsible for integration with -%%% Erlang's built-in type system. +%%% Erlang's built-in type system. PropEr can parse types expressed in Erlang's +%%% native type format and convert them to its own type format. Such expressions +%%% can be used instead of regular type constructors in the second argument of +%%% `?FORALLs'. No extra notation is required -PropEr will detect which calls +%%% correspond to native types by applying a parse transform during compilation. +%%% This parse transform is automatically applied to any module that includes +%%% the `proper.hrl' header file. You can disable this feature by compiling your +%%% modules with `-DPROPER_NO_TRANS'. Note that this will currently also disable +%%% the automatic exporting of properties. +%%% +%%% The use of native types in properties is subject to the following usage +%%% rules: +%%%
    +%%%
  • Native types cannot be used outside of `?FORALLs'.
    • +%%%
  • Inside `?FORALLs', native types can be combined with other native +%%% types, and even with PropEr types, inside tuples and lists (the constructs +%%% `[...]', `{...}' and `++' are all allowed).
    • +%%%
  • All other constructs of Erlang's built-in type system (e.g. `|' for union, +%%% `_' as an alias of `any()', `<<_:_>>' binary type syntax or +%%% `fun((...) -> ...)' function type syntax) are not allowed in `?FORALLs', +%%% since they are rejected by the Erlang parser.
    • +%%%
  • Anything other than a tuple constructor, list constructor, `++' application, +%%% local or remote call will automatically be considered a PropEr type +%%% constructor and not be processed further by the parse transform.
    • +%%%
  • Parametric native types are fully supported - of course, they can only +%%% appear instantiated in a `?FORALL'. The arguments of parametric native types +%%% are always interpreted as native types.
    • +%%%
  • Parametric PropEr types, on the other hand, can take any kind of argument. +%%% You can even mix native and PropEr types in the arguments of a PropEr type. +%%% For example, assuming that the following declarations are present: +%%% ``` my_proper_type() -> ?LET(...). +%%% -type my_native_type() :: ... .''' +%%% Then the following expressions are all legal: +%%% ``` vector(2, my_native_type()) +%%% function(0, my_native_type()) +%%% union([my_proper_type(), my_native_type()])'''
    • +%%%
  • Some type constructors can take native types as arguments (but only +%%% inside `?FORALLs'): +%%%
      +%%%
    • `?SUCHTHAT', `?SUCHTHATMAYBE', `non_empty', `noshrink': these work with +%%% native types too
      • +%%%
    • `?LAZY', `?SHRINK', `resize', `?SIZED': these don't work with native +%%% types
      • +%%%
    • `?LET', `?LETSHRINK': only the top-level base type can be a native type +%%%
      • +%%%
    • +%%%
  • Native type declarations in the `?FORALLs' of a module can reference any +%%% custom type declared in a `-type' or `-opaque' attribute of the same module, +%%% as long as no module identifier is used.
    • +%%%
  • Typed records cannot be referenced inside `?FORALLs' using the `#rec_name{}' +%%% syntax. To use a typed record in a `?FORALL', enclose the record in a custom +%%% type like so: +%%% ``` -type rec_name() :: #rec_name{}. ''' +%%% and use the custom type instead.
    • +%%%
  • `?FORALLs' may contain references to self-recursive or mutually recursive +%%% native types, so long as each type in the hierarchy has a clear base case. +%%% Currently, PropEr requires that the toplevel of any recursive type +%%% declaration is either a (maybe empty) list or a union containing at least +%%% one choice that doesn't reference the type (it may, however, reference any +%%% of the types that are mutually recursive with it). This means, for example, +%%% that some valid recursive type declarations, such as this one: +%%% ``` ?FORALL(..., a(), ...) ''' where: +%%% ``` -type a() :: {'a','none' | a()}. ''' +%%% are not accepted by PropEr. However, such types can be rewritten in a way +%%% that allows PropEr to parse them: +%%% ``` ?FORALL(..., a(), ...) ''' where: +%%% ``` -type a() :: {'a','none'} | {'a',a()}. ''' +%%% This also means that recursive record declarations are not allowed: +%%% ``` ?FORALL(..., rec(), ...) ''' where: +%%% ``` -type rec() :: #rec{}. +%%% -record(rec, {a = 0 :: integer(), b = 'nil' :: 'nil' | #rec{}}). ''' +%%% A little rewritting can usually remedy this problem as well: +%%% ``` ?FORALL(..., rec(), ...) ''' where: +%%% ``` -type rec() :: #rec{b :: 'nil'} | #rec{b :: rec()}. +%%% -record(rec, {a = 0 :: integer(), b = 'nil' :: 'nil' | #rec{}}). '''
    • +%%%
  • Remote types may be referenced in a `?FORALL', as long as they are +%%% exported from the remote module. Currently, PropEr requires that any remote +%%% modules whose types are directly referenced from within properties are +%%% present in the code path at compile time, either compiled with `debug_info' +%%% enabled or in source form. If PropEr cannot find a remote module at all, +%%% finds only a compiled object file with no debug information or fails to +%%% compile the source file, all calls to that module will automatically be +%%% considered calls to PropEr type constructors.
    • +%%%
  • For native types to be translated correctly, both the module that contains +%%% the `?FORALL' declaration as well as any module that contains the declaration +%%% of a type referenced (directly or indirectly) from inside a `?FORALL' must be +%%% present in the code path at runtime, either compiled with debug_info enabled +%%% or in source form.
    • +%%%
  • Local types with the same name as an auto-imported BIF are not accepted by +%%% PropEr, unless the BIF in question has been declared in a `no_auto_import' +%%% option.
    • +%%%
  • When an expression can be interpreted both as a PropEr type and as a native +%%% type, the former takes precedence. This means that a function `foo()' will +%%% shadow a type `foo()' if they are both present in the module. The same rule +%%% applies to remote functions and types as well.
    • +%%%
  • The above may cause some confusion when list syntax is used: +%%%
      +%%%
    • The expression `[integer()]' can be interpreted both ways, so the +%%% PropEr way applies. Therefore, instances of this type will always be +%%% lists of length 1, not arbitrary integer lists, as would be expected when +%%% interpreting the expression as a native type.
      • +%%%
    • Assuming that a custom type foo/1 has been declared, the expression +%%% `foo([integer()])' can only be interpreted as a native type declaration, +%%% which means that the generic type of integer lists will be passed to +%%% `foo/1'.
      • +%%%
    +%%%
    • +%%%
  • Currently, PropEr does not detect the following mistakes: +%%%
      +%%%
    • inline record-field specializations that reference non-existent +%%% fields
      • +%%%
    • type parameters that are not present in the RHS of a `-type' +%%% declaration
      • +%%%
    • using `_' as a type variable in the LHS of a `-type' declaration
      • +%%%
    • using the same variable in more than one position in the LHS of a +%%% `-type' declaration
      • +%%%
    +%%%
    • +%%%
+%%% +%%% You can use the these functions to try out the type +%%% translation subsystem. +%%% +%%% CAUTION: These functions should never be used inside +%%% properties. They are meant for demonstration purposes only. +%%% @end -module(proper_typeserver). -behaviour(gen_server).