Overview

Module proper

• Description
• Data Types
• Function Index
• Function Details

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

Version: Jun 20 2016 16:27:12

Authors: Manolis Papadakis.

Description

This is the main PropEr module.

How to write properties

The simplest properties that PropEr can test consist of a single boolean expression (or a statement block that returns a boolean), which is expected to evaluate to true. Thus, the test true always succeeds, while the test false always fails (the failure of a property may also be signified by throwing an exception, error or exit. More complex (and useful) properties can be written by wrapping such a boolean expression with one or more of the following wrappers:

?FORALL(<Xs>, <Xs_type>, <Prop>)

The <Xs> field can either be a single variable, a tuple of variables or a list of variables. The <Xs_type> field must then be a single type, a tuple of types of the same length as the tuple of variables or a list of types of the same length as the list of variables, respectively. Tuples and lists can be combined in any way, as long as <Xs> and <Xs_type> are compatible. Both PropEr-provided types, as listed in the proper_types module, and types declared in Erlang's built-in typesystem (we will refer to such types in as native types) may be used in the <Xs_type> field. The use of native types in ?FORALLs is subject to some limitations, as described in the documentation for the proper_typeserver module. All the variables inside <Xs> can (and should) be present as free variables inside the wrapped property <Prop>. When a ?FORALL wrapper is encountered, a random instance of <Xs_type> is produced and each variable in <Xs> is replaced inside <Prop> by its corresponding instance.

?IMPLIES(<Precondition>, <Prop>)

This wrapper only makes sense when in the scope of at least one ?FORALL. The <Precondition> field must be a boolean expression or a statement block that returns a boolean. If the precondition evaluates to false for the variable instances produced in the enclosing ?FORALL wrappers, the test case is rejected (it doesn't count as a failing test case), and PropEr starts over with a new random test case. Also, in verbose mode, an x is printed on screen.

?WHENFAIL(<Action>, <Prop>)

The <Action> field should contain an expression or statement block that produces some side-effect (e.g. prints something to the screen). In case this test fails, <Action> will be executed. Note that the output of such actions is not affected by the verbosity setting of the main application.

?TRAPEXIT(<Prop>)

If the code inside <Prop> spawns and links to a process that dies abnormally, PropEr will catch the exit signal and treat it as a test failure, instead of crashing. ?TRAPEXIT cannot contain any more wrappers.

?TIMEOUT(<Time_limit>, <Prop>)

Signifies that <Prop> should be considered failing if it takes more than <Time_limit> milliseconds to return. The purpose of this wrapper is to test code that may hang if something goes wrong. ?TIMEOUT cannot contain any more wrappers.

conjunction(<SubProps>)

See the documentation for conjunction/1.

equals(<A>, <B>)

See the documentation for equals/2.

There are also multiple wrappers that can be used to collect statistics on the distribution of test data:

• collect/2
• collect/3
• aggregate/2
• aggregate/3
• classify/3
• measure/3

A property may also be wrapped with one or more of the following outer-level wrappers, which control the behaviour of the testing subsystem. If an outer-level wrapper appears more than once in a property, the innermost instance takes precedence.

• numtests/2
• fails/2
• on_output/2

For some actual usage examples, see the code in the examples directory, or check out PropEr's site. 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, <Type_of_error>}: An error occured; see the Errors section for more information.

To test all properties exported from a module (a property is a 0-arity function whose name begins with prop_), you can use module/1 or 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 the module function itself.

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 counterexample/0. When testing a whole module, run counterexamples/0 to get a counterexample for each failing property, as a list of {mfa(),counterexample()} tuples. To enable this functionality, some information has to remain in the process dictionary even after PropEr has returned. If, for some reason, you want to completely clean up the process dictionary of PropEr-produced entries, run 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 counterexample/1 or counterexample/2 instead of quickcheck/1 and quickcheck/2 respectively), 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 module/2), PropEr will return a list of {mfa(),counterexample()} tuples, one for each failing property.

You can re-check a specific counterexample against the property that it previously falsified by running check/2 or 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, <Type_of_error>}: An error occured - see the Errors section for more information.

Proper will not attempt to shrink the input in case it still 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 most testing functions (such as 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 How to write properties 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, <IO_device>}

Redirects all of PropEr's output to <IO_device>, which should be an IO device associated with a file opened for writing.

{on_output, <Output_function>}

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 Counterexamples section for details).

{numtests, <Positive_number>} or simply <Positive_number>

This is equivalent to the numtests/1 property wrapper. Any numtests/1 wrappers in the actual property will overwrite this setting.

{start_size, <Size>}

Specifies the initial value of the size parameter (default is 1), see the documentation of the proper_types module for details.

{max_size, <Size>}

Specifies the maximum value of the size parameter (default is 42), see the documentation of the proper_types module for details.

{max_shrinks, <Non_negative_number>}

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, <Positive_number>}

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 fails/1 property wrapper.

{spec_timeout, infinity | <Non_negative_number>}

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

any_to_integer

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

{skip_mfas, [<MFA>]}

When checking a module's specs, PropEr will not test the specified MFAs. Default is [].

{false_positive_mfas, fun((mfa(),[Arg::term()],{fail, Result::term()} | {error | exit | throw, Reason::term()}) -> boolean()) | undefined}

When checking a module's spec(s), PropEr will treat a counterexample as a false positive if the user supplied function returns true. Otherwise, PropEr will treat the counterexample as it normally does. The inputs to the user supplied function are the MFA, the arguments passed to the MFA, and the result returned from the MFA or an exception with it's reason. If needed, the user supplied function can call erlang:get_stacktrace/0. Default is undefined.

Spec testing

You can test the accuracy of an exported function's spec by running check_spec/1 or 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 check_specs/1 or 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 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.

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, <SubError>}

The typeserver encountered an error. The <SubError> field contains specific information regarding the error.

{unexpected, <Result>}

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, <Option>}

<Option> is not an option that PropEr understands.

Data Types

clean_input()

clean_input() = proper_gen:instance() | sub_counterexamples()

counterexample()

counterexample() = [clean_input()]

error()

error() = {error, error_reason()}

error_reason()

error_reason() = 
    arity_limit |
    cant_generate |
    cant_satisfy |
    non_boolean_result |
    rejected |
    too_many_instances |
    type_mismatch |
    wrong_type |
    {typeserver, term()} |
    {unexpected, any()} |
    {unrecognized_option, term()}

false_positive_mfas()

false_positive_mfas() = 
    fun((mfa(),
         Args :: [term()],
         {fail, Result :: term()} |
         {error | exit | throw, Reason :: term()}) ->
            boolean()) |
    undefined

----------------------------------------------------------------------------- Options and Context types -----------------------------------------------------------------------------

long_module_result()

long_module_result() = [{mfa(), counterexample()}] | error()

long_result()

long_result() = true | counterexample() | error()

mod_name()

mod_name() = atom()

module_result()

module_result() = long_module_result() | short_module_result()

outer_test()

abstract datatype: outer_test()

A testable property that has optionally been wrapped with one or more external wrappers.

output_fun()

output_fun() = fun((string(), [term()]) -> ok)

A fun to be used by PropEr for output printing. Such a fun should follow the conventions of io:format/2.

result()

result() = long_result() | short_result()

sample()

sample() = [term()]

short_module_result()

short_module_result() = [mfa()] | error()

short_result()

short_result() = boolean() | error()

size()

size() = non_neg_integer()

stats_printer()

stats_printer() = 
    fun((sample()) -> ok) | fun((sample(), output_fun()) -> ok)

A stats-printing function that can be passed to some of the statistics collection functions, to be used instead of the predefined stats-printer. Such a function will be called at the end of testing (in case no test fails) with a sorted list of collected terms. A commonly used stats-printer is with_title/1.

sub_counterexamples()

sub_counterexamples() = [{tag(), counterexample()}]

tag()

tag() = atom()

test()

abstract datatype: test()

A testable property that has not been wrapped with an external wrapper.

title()

title() = atom() | string()

user_opt()

user_opt() = 
    quiet |
    verbose |
    {to_file, io:device()} |
    {on_output, output_fun()} |
    long_result |
    {numtests, pos_integer()} |
    pos_integer() |
    {start_size, size()} |
    {max_size, size()} |
    {max_shrinks, non_neg_integer()} |
    noshrink |
    {constraint_tries, pos_integer()} |
    fails |
    any_to_integer |
    {spec_timeout, timeout()} |
    {skip_mfas, [mfa()]} |
    {false_positive_mfas, false_positive_mfas()}

user_opts()

user_opts() = [user_opt()] | user_opt()

Function Index

Function Details

aggregate/2

aggregate(Sample :: sample(), Test :: test()) -> test()

Same as collect/2, but accepts a list of categories under which to classify the produced test case.

aggregate/3

aggregate(Printer :: stats_printer(),
          Sample :: sample(),
          Test :: test()) ->
             test()

Same as collect/3, but accepts a list of categories under which to classify the produced test case.

check/2

check(OuterTest :: outer_test(), CExm :: counterexample()) ->
         short_result()

Re-checks a specific counterexample CExm against the property OuterTest that it previously falsified.

check/3

check(OuterTest :: outer_test(),
      CExm :: counterexample(),
      UserOpts :: user_opts()) ->
         short_result()

Same as check/2, but also accepts a list of options.

check_spec/1

check_spec(MFA :: mfa()) -> result()

Tests the accuracy of an exported function's spec.

check_spec/2

check_spec(MFA :: mfa(), UserOpts :: user_opts()) -> result()

Same as check_spec/1, but also accepts a list of options.

check_specs/1

check_specs(Mod :: mod_name()) -> module_result()

Tests all exported, -speced functions of a module Mod against their spec.

check_specs/2

check_specs(Mod :: mod_name(), UserOpts :: user_opts()) ->
               module_result()

Same as check_specs/1, but also accepts a list of options.

classify/3

classify(Count :: boolean(),
         TermOrSample :: term() | sample(),
         Test :: test()) ->
            test()

Same as collect/2, but can accept both a single category and a list of categories. Count is a boolean flag: when false, the particular test case will not be counted.

clean_garbage/0

clean_garbage() -> ok

Cleans up the process dictionary of all PropEr-produced entries.

collect/2

collect(Category :: term(), Test :: test()) -> test()

Specifies that test cases produced by this property should be categorized under the term Category. This field can be an expression or statement block that evaluates to any term. All produced categories are printed at the end of testing (in case no test fails) along with the percentage of test cases belonging to each category. Multiple collect wrappers are allowed in a single property, in which case the percentages for each collect wrapper are printed separately.

collect/3

collect(Printer :: stats_printer(),
        Category :: term(),
        Test :: test()) ->
           test()

Same as collect/2, but also accepts a fun Printer to be used as the stats printer.

conjunction/1

conjunction(SubProps :: [{tag(), test()}]) -> test()

Returns a property that is true only if all of the sub-properties SubProps are true. Each sub-property should be tagged with a distinct atom. If this property fails, each failing sub-property will be reported and saved inside the counterexample along with its tag.

counterexample/0

counterexample() -> counterexample() | undefined

Retrieves the last (simplest) counterexample produced by PropEr during the most recent testing run.

counterexample/1

counterexample(OuterTest :: outer_test()) -> long_result()

Equivalent to quickcheck(OuterTest, [long_result]).

counterexample/2

counterexample(OuterTest :: outer_test(), UserOpts :: user_opts()) ->
                  long_result()

Same as counterexample/1, but also accepts a list of options.

counterexamples/0

counterexamples() -> [{mfa(), counterexample()}] | undefined

Returns a counterexample for each failing property of the most recent module testing run.

equals/2

equals(A :: term(), B :: term()) -> test()

A custom property that evaluates to true only if A =:= B, else evaluates to false and prints "A =/= B" on the screen.

fails/1

fails(Test :: outer_test()) -> outer_test()

Specifies that we expect the property Test to fail for some input. The property will be considered failing if it passes all the tests.

measure/3

measure(Title :: title(),
        Sample :: number() | [number()],
        Test :: test()) ->
           test()

A function that collects numeric statistics on the produced instances. The number (or numbers) provided are collected and some statistics over the collected sample are printed at the end of testing (in case no test fails), prepended with Title, which should be an atom or string.

module/1

module(Mod :: mod_name()) -> module_result()

Tests all properties (i.e., all 0-arity functions whose name begins with prop_) exported from module Mod.

module/2

module(Mod :: mod_name(), UserOpts :: user_opts()) ->
          module_result()

Same as module/1, but also accepts a list of options.

numtests/2

numtests(N :: pos_integer(), Test :: outer_test()) -> outer_test()

Specifies the number N of tests to run when testing the property Test. Default is 100.

on_output/2

on_output(Print :: output_fun(), Test :: outer_test()) ->
             outer_test()

Specifies an output function Print to be used by PropEr for all output printing during the testing of property Test. This wrapper is equivalent to the on_output option.

quickcheck/1

quickcheck(OuterTest :: outer_test()) -> result()

Runs PropEr on the property OuterTest.

quickcheck/2

quickcheck(OuterTest :: outer_test(), UserOpts :: user_opts()) ->
              result()

Same as quickcheck/1, but also accepts a list of options.

with_title/1

with_title(Title :: title()) -> stats_printer()

A predefined function that accepts an atom or string and returns a stats printing function which is equivalent to the default one, but prints the given title Title above the statistics.

Overview

Generated by EDoc, Jun 20 2016, 16:27:12.