# Module proper

- Description
- Data Types
- Function Index
- Function Details

This is the main PropEr module.

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

Version: Jan 2 2021 16:13:05

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 `?FORALL`s 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.
`?SETUP(<Fun>, <Prop>)`
  Adds a setup `<Fun>`ction to the property which will be called before the first test. This function has to return a finalize function of arity 0, which should return the atom `ok`, that will be called after the last test. It is possible to use multiple `?SETUP` macros on the same property.
`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.
`nocolors`
  Don't use term colors in output.

### 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 `?FORALL`s 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()]

### setup_opts()

    setup_opts() =
        #{numtests := pos_integer(),
          start_size := size(),
          max_size := size(),
          output_fun := output_fun()}

----------------------------------------------------------------------------- Result types -----------------------------------------------------------------------------

### 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()} |
        nocolors

### user_opts()

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

## Function Index

aggregate/2 | Same as `collect/2`, but accepts a list of categories under which to classify the produced test case.
aggregate/3 | Same as `collect/3`, but accepts a list of categories under which to classify the produced test case.
check/2 | Re-checks a specific counterexample `CExm` against the property `OuterTest` that it previously falsified.
check/3 | Same as `check/2`, but also accepts a list of options.
check_spec/1 | Tests the accuracy of an exported function's spec.
check_spec/2 | Same as `check_spec/1`, but also accepts a list of options.
check_specs/1 | Tests all exported, `-spec`ed functions of a module `Mod` against their spec.
check_specs/2 | Same as `check_specs/1`, but also accepts a list of options.
classify/3 | Same as `collect/2`, but can accept both a single category and a list of categories.
clean_garbage/0 | Cleans up the process dictionary of all PropEr-produced entries.
collect/2 | Specifies that test cases produced by this property should be categorized under the term `Category`.
collect/3 | Same as `collect/2`, but also accepts a fun `Printer` to be used as the stats printer.
conjunction/1 | Returns a property that is true only if all of the sub-properties `SubProps` are true.
counterexample/0 | Retrieves the last (simplest) counterexample produced by PropEr during the most recent testing run.
counterexample/1 | Equivalent to `quickcheck(OuterTest, [long_result])`.
counterexample/2 | Same as `counterexample/1`, but also accepts a list of options.
counterexamples/0 | Returns a counterexample for each failing property of the most recent module testing run.
equals/2 | A custom property that evaluates to `true` only if `A =:= B`, else evaluates to `false` and prints "`A =/= B`" on the screen.
fails/1 | Specifies that we expect the property `Test` to fail for some input.
measure/3 | A function that collects numeric statistics on the produced instances.
module/1 | Tests all properties (i.e., all 0-arity functions whose name begins with `prop_`) exported from module `Mod`.
module/2 | Same as `module/1`, but also accepts a list of options.
numtests/2 | Specifies the number `N` of tests to run when testing the property `Test`.
on_output/2 | Specifies an output function `Print` to be used by PropEr for all output printing during the testing of property `Test`.
quickcheck/1 | Runs PropEr on the property `OuterTest`.
quickcheck/2 | Same as `quickcheck/1`, but also accepts a list of options.
with_title/1 | 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.

## 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, `-spec`ed 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.

Generated by EDoc