Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Complete EDoc docs, fix bug in make_doc, remove pure_check from API

  • Loading branch information...
commit ca96110cb0bbbf31fbc7563e0424b2f2daafd156 1 parent cbbe239
@manopapad authored
View
1,245 README
@@ -1,1245 +0,0 @@
---------------------------------------------------------------------------------
-Contact information and license
---------------------------------------------------------------------------------
-
-PropEr (PROPerty-based testing tool for ERlang) is a QuickCheck-inspired
-open-source property-based testing tool for Erlang, developed by Manolis
-Papadakis <manopapad@gmail.com>, Eirini Arvaniti <eirinibob@gmail.com> and
-Kostis Sagonas <kostis@cs.ntua.gr>. The base PropEr system was written mainly by
-Manolis Papadakis, and the stateful code testing subsystem by Eirini Arvaniti.
-
-You can reach the developers in the following ways:
-* by email: at proper@softlab.ntua.gr
-* on the web: at github.com/manopapad/proper (project page on github)
-We welcome user contributions and feedback (comments, suggestions, feature
-requests, bug reports, patches etc.).
-
-Copyright 2010-2011 by Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas.
-
-This program is distributed under the GPL, version 3 or later. Please see the
-COPYING file for details.
-
-
---------------------------------------------------------------------------------
-Quickstart guide
---------------------------------------------------------------------------------
-
-* Compile PropEr: run 'make' (or 'make all', if you also want to build the
- documentation -- you will need the syntax_tools application and a recent
- version of EDoc).
-* Add PropEr's base directory to your Erlang code path by choosing one of the
- following ways:
- 1. ERL_LIBS environment variable - Add the following line to your shell
- startup file (~/.bashrc in the case of the Bash shell):
- export ERL_LIBS=/full/path/to/proper
- 2. Erlang resource file - Add the following line to your ~/.erlang file:
- code:load_abs("/full/path/to/proper").
-* Add the following include line to all source files containing properties you
- wish to test:
- -include_lib("proper/include/proper.hrl").
- By including this header, all the macros, types and functions described in
- this file are automatically imported, so you can use them without a module
- identifier. You can disable this behaviour by compiling your module with
- -DPROPER_NO_IMPORTS. Also, all functions of arity 0 whose name starts with
- "prop_" are automatically exported from the module. If you wish to disable the
- automatic exporting of properties, compile your module with -DPROPER_NO_TRANS.
-* Compile your source files.
-* For each property, run:
- proper:quickcheck(your_module:some_property()).
- or
- proper:quickcheck(your_module:some_property(), <option/options>).
-
-
---------------------------------------------------------------------------------
-Common Problems
---------------------------------------------------------------------------------
-
-Using PropEr in conjunction with EUnit:
- Both systems define a ?LET macro, which can cause a clash. Simply include
- PropEr's header file before EUnit's header file. That way, any instance of
- ?LET will count as a PropEr ?LET.
-Using PropEr under Erlang/OTP R13B03 or older:
- PropEr makes heavy use of recursive types, which are unsupported on versions
- of the Erlang/OTP distribution prior to R13B04. To compile PropEr under such
- a system, add {d,NO_TYPES} to erl_opts inside rebar.config. This enables the
- spec+type-stripping parse transform included in PropEr, which fixes the
- problem by stripping all type information from PropEr's source files while
- compiling.
-
-
---------------------------------------------------------------------------------
-Introduction -> moved the last paragraph to proper.erl
---------------------------------------------------------------------------------
-
-Traditional testing methodologies essentially involve software testers writing a
-series of test inputs for their programs, along with their corresponding
-expected outputs, then running the program with these inputs and observing
-whether it behaves as expected. This method of testing, while simple and easy to
-automate, suffers from a few problems, such as:
-* Writing test cases by hand is tedious and time consuming.
-* It is hard to know whether the test suite covers all aspects of the software
- under test.
-
-Property-based testing is a novel approach to software testing, where the tester
-needs only specify the generic structure of valid inputs for the program under
-test, plus certain properties (regarding the program's behaviour and the input-
-output relation) which are expected to hold for every valid input. A property-
-based testing tool, when supplied with this information, should randomly
-produce progressively more complex valid inputs, then apply those inputs to the
-program while monitoring its execution, to ensure that it behaves according to
-its specification, as outlined in the supplied properties.
-
-Here are a few examples of simple properties a user may wish to test, expressed
-in natural language:
-* The program should accept any character string and convert all lowercase
- letters inside the string to uppercase.
-* The program should accept any list of integers. If the input list is at least
- 4 elements long, the program should return the 4th largest integer in the
- list, else it should throw an exception.
-
-PropEr is such 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. The input domain of functions is specified through the use of
-a type system, modeled closely after the type system of the language itself
-(see the following sections for details). 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) -> moved to proper.erl
---------------------------------------------------------------------------------
-
-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. 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 'Basic types' and 'How to construct
- types' sections) and types declared in Erlang's built-in typesystem (we
- refer to such types in this README 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 'Native types support' section. 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.
-conjunction([{Tag1,Prop1},...,{TagN,PropN}])
- This property is true only if all of the sub-properties Prop1,...,PropN are
- true. The tags Tag1,...,TagN must be distinct atoms. These are used when
- reporting the failure of a property (each failing sub-property is reported
- using its tag) and inside counterexamples (see the 'Counterexamples' section
- for details).
-?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.
-collect(<Category>, <Prop>)
- The <Category> field can be an expression or statement block that evaluates
- to any term - the test case produced will be categorized under this 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(<Stats_printer>, <Category>, <Prop>)
- Same as collect/2, but takes an extra first argument, which should be a fun
- with the following signature:
- (SortedSample :: [term()]) -> 'ok'
- This fun will be called at the end of testing (in case no test fails) with
- a sorted list of collected terms. It is expected to print some statistics
- over the collected terms. with_title/1 is 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 above the statistics.
-aggregate(<Categories>, <Prop>)
- Same as collect/2, but accepts a list of categories under which to classify
- the produced test case.
-aggregate(<Stats_printer>, <Categories>, <Prop>)
- Same as collect/3, but accepts a list of categories under which to classify
- the produced test case.
-classify(<Counts>, <Category/Categories>, <Prop>)
- Same as collect/2, but accepts both a single category and a list of
- categories. Also, if the boolean flag <Counts> is 'false', the produced test
- case is not counted.
-measure(<Title>, <Number> | <List_of_numbers>, <Prop>)
- The number (or numbers) provided are collected and some numeric 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.
-?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.
-
-The following predefined properties may be used in place of a simple boolean
-expression as the innermost property:
-
-equals(<A>, <B>)
- Returns true if <A> =:= <B>, else returns false and prints "<A> =/= <B>" on
- screen.
-
-Additionally, a property may be wrapped with one or more of the following
-outer-level wrappers, which control the behaviour of the testing subsystem. If
-the same wrapper appears more than once in a property, the innermost takes
-precedence.
-
-numtests(<Positive_number>, <Prop>)
- Specifies the number of tests to run. Default is 100.
-fails(<Prop>)
- Specifies that we expect the property to fail for some input. The property
- will be considered failing if it passes all the tests.
-on_output(<Output_function>, <Prop>)
- Specifies an output function to be used by PropEr for all output printing.
- This wrapper is equivalent to the 'on_output' option (see the 'Options'
- section for details).
-
-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 -> moved to proper.erl
---------------------------------------------------------------------------------
-
-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 a
- description of possible errors.
-
-You can also run PropEr in pure mode by using proper:pure_check/1,2 instead of
-proper:quickcheck/1,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 run:
- proper:module(<Module>).
- or
- proper:module(<Module>, <option/options>).
-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
-'Counterexamples' section).
-
-
---------------------------------------------------------------------------------
-Counterexamples -> moved to proper.erl
---------------------------------------------------------------------------------
-
-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 proper:counterexample().
-When testing a whole module, run proper:counterexamples() 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. To completely clean up the
-process dictionary of PropEr-produced entries, run proper:clean_garbage().
-
-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 proper:counterexample/1,2 instead of
-proper:quickcheck/1,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
-proper:module/2), PropEr will return a list of {mfa(),counterexample()} tuples,
-one for each failing property.
-
-You can re-check a specific counterexample <CExm> against the property <Prop>
-that it previously falsified by running:
- proper:check(<Prop>, <CExm>)
- or
- proper:check(<Prop>, <CExm>, <option/options>)
-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
- 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 <CExm> actually corresponds to <Prop>.
-
-
---------------------------------------------------------------------------------
-Options -> moved to proper.erl
---------------------------------------------------------------------------------
-
-Options can be provided as an extra argument to testing functions exported from
-the main proper module (such as proper:quickcheck). 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' property wrapper. Any 'numtests'
- 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
- 'How to construct types' section for details.
-{'max_size', <Size>}
- Specifies the maximum value of the 'size' parameter (default is 42), see the
- 'How to construct types' section 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' 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 that the specified amount of milliseconds to
- return for that input.
-'any_to_integer'
- All generated instances of the type 'any()' 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).
-
-
---------------------------------------------------------------------------------
-Basic types -> moved to proper_types.erl
---------------------------------------------------------------------------------
-
-The following basic types are provided:
-
-* integer() : all integers,
- also written as largeint() for compatibility with QuickCheck,
- the shrinking subsystem will attempt to shrink instances of this type to
- values as close as possible to 0
-* integer(Low,High) : integers between 'Low' and 'High', bounds included,
- also written as choose(Low,High) and range(Low,High),
- Low and High must be Erlang expressions that evaluate to integers, with
- Low =< High,
- instances shrink towards the bound with the smallest absolute value
-* non_neg_integer() : all non-negative integers,
- instances shrink towards 0
-* pos_integer() : all positive integers,
- instances shrink towards 1
-* neg_integer() : all negative integers,
- instances shrink towards -1
-* float() : all floating point numbers,
- also written as real() for compatibility with QuickCheck,
- instances shrink towards 0.0
-* float(Low,High) : all floats between 'Low' and 'High', bounds included,
- Low and High must be Erlang expressions that evaluate to floats, with
- Low =< High,
- instances shrink towards the bound with the smallest absolute value
-* number() : all numbers (integers and floats),
- instances shrink towards zero (0 or 0.0)
-* byte() : all integers between 0 and 255,
- instances shrink towards 0
-* char() : all integers between 0 and 16#10ffff,
- instances shrink towards the NUL character, \000
-* binary() : all binaries,
- instances shrink towards the empty binary, <<>>
-* bitstring() : all bitstrings,
- instances shrink towards the empty bitstring, <<>>
-* atom() : all atoms, except those starting with '$'
- you should not use any atoms starting with a '$', as these may clash
- with atoms used internally by PropEr,
- instances shrink towards the empty atom, ''
-* boolean() : the atoms 'true' or 'false',
- also written as bool() for compatibility with QuickCheck,
- instances shrink towards 'false'
-* list(ElemType) : all lists containing elements of type ElemType,
- instances shrink towards the empty list, []
-* list() : equivalent to list(any())
-* string() : all lists of characters,
- instances shrink towards the empty string, ""
-* function(ArgTypes, RetType) : all pure functions that map instances of
- ArgTypes (ArgTypes must be provided in a list) to instances of RetType,
- the syntax function(Arity, RetType) is also acceptable
-* any() : all Erlang terms (that PropEr can produce)
- also written as term()
- currently, functions are never produced as instances of any()
- CAUTION: Instances of 'any()' are expensive to produce, shrink and instance-
- check, both in terms of processing time and consumed memory. Only use this
- type if you are certain that you need it.
-
-All the above have analogues in the built-in types of the Erlang language.
-
-In addition, the following types are provided:
-
-* int() : small integers (bound by the current value of the 'size' parameter -
- see the next section for details),
- instances shrink towards 0
-* nat() : small non-negative integers (bound by the current value of the 'size'
- parameter - see the next section for details),
- instances shrink towards 0
-* non_neg_float() : all non-negative floats,
- instances shrink towards 0.0
-* binary(Len) : all binaries with a byte size of 'Len',
- Len must be an Erlang expression that evaluates to a non-negative integer,
- instances shrink towards binaries of zeroes
-* bitstring(Len) : all bitstrings with a bit size of 'Len',
- Len must be an Erlang expression that evaluates to a non-negative integer,
- instances shrink towards bitstrings of zeroes
-* tuple(ListOfTypes) : all tuples whose i-th element is an instance of the type
- at index i of ListOfTypes,
- also written simply as a tuple of types
-* loose_tuple(ElemType) : all tuples whose elements are all of type ElemType
- instances shrink towards {}
-* tuple() : equivalent to loose_tuple(any())
-* vector(Len,ElemType) : all lists of length Len containing elements of type
- ElemType,
- Len must be an Erlang expression that evaluates to a non-negative integer
-* fixed_list(ListOfTypes) : all lists whose i-th element is an instance of the
- type at index i of ListOfTypes,
- also written simply as ListOfTypes
-* orderedlist(ElemType) : all sorted lists containing elements of type ElemType,
- instances shrink towards the empty list, []
-* exactly(X) : singleton type consisting only of X,
- X must be an evaluated term,
- also written as return(X) or simply as X
-* union(ListOfTypes) : the union of all types in ListOfTypes,
- ListOfTypes can't be empty,
- the random instance generator is equally likely to choose any one of the
- types in ListOfTypes,
- the shrinking subsystem will always try to shrink an instance of a type
- union to an instance of the first type in ListOfTypes, thus you should write
- the simplest case first,
- also written as oneof(ListOfTypes) and elements(ListOfTypes)
-* weighted_union(ListOfTypes) : a specialization of union(ListOfTypes), where
- each type in ListOfTypes is assigned a frequency like so: {frequency,type},
- frequencies must be Erlang expressions that evaluate to positive integers,
- types with larger frequencies are more likely to be chosen by the random
- instance generator,
- the shrinking subsystem will ignore the frequencies and try to shrink
- towards the first type in ListOfTypes,
- also written as wunion(ListOfTypes) and frequency(ListOfTypes)
-* default(Default, Type) : adds a default value, Default, to Type,
- the default serves as a primary shrinking target for instances, while it is
- also chosen by the random instance generation subsystem half the time
-* weighted_default(Default, Type) : a specialization of default(Default, Type),
- where Default and Type are assigned weights like so: {frequency,type},
- to be considered by the random instance generator,
- the shrinking subsystem will ignore the weights and try to shrink
- using the default value
-* function[0-4](RetType) : equivalent to function([0-4], RetType), provided for
- compatibility with QuickCheck
-* timeout() : equivalent to union([non_neg_integer() | 'infinity']),
- instances shrink towards 0
-* arity() : equivalent to range(0,255),
- instances shrink towards 0
-
-As you can see from the above descriptions, types can be combined in tuples or
-lists to produce other types, while exact values (such as exact numbers, atoms
-or strings) can be combined with types inside such structures, like in this
-example of the type of a tagged tuple: {'result', integer()}.
-
-
---------------------------------------------------------------------------------
-How to construct types -> moved to proper_types.erl
---------------------------------------------------------------------------------
-
-The following macros and functions can be applied to types in order to produce
-new ones:
-
-?LET(<Xs>, <Xs_type>, <In>)
- To produce an instance of this type, all appearances of the variables in
- <Xs> inside <In> are replaced by their corresponding values in a randomly
- generated instance of <Xs_type>. It's OK for the <In> part to evaluate to a
- type - in that case, an instance of the inner type is generated recursively.
-?SUCHTHAT(<X>, <Type>, <Condition>)
- This produces a specialization of <Type>, which only includes those members
- of <Type> that satisfy the constraint <Condition> - that is, those members
- for which the function 'fun(<X>) -> <Condition> end' returns 'true'. If the
- constraint is very strict - that is, only a small percentage of instances
- of <Type> 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). 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 for details).
-?SUCHTHATMAYBE(<X>, <Type>, <Condition>)
- Equivalent to the ?SUCHTHAT macro, but the constraint <Condition> is
- considered non-strict: if the 'constraint_tries' limit is reached, the
- generator will just return an instance of <Type> instead of failing,
- even if that instance doesn't satisfy the constraint.
-non_empty(<List_or_binary_type>)
- This is a predefined constraint that can be applied to random-length list
- and binary types (e.g. list(), string(), binary()) to ensure that the
- produced values are not empty.
-noshrink(<Type>)
- Creates a new type which is equivalent to <Type>, but whose instances are
- never shrunk by the shrinking subsystem.
-?SHRINK(<Generator>, <List_of_alternative_generators>)
- This creates a type whose instances are generated by evaluating the
- statement block <Generator> (this may evaluate to a type, which is generated
- recursively). If an instance of such a type is to be shrunk, the generators
- in <List_of_alternative_generators> 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 <Generator>, the alternatives may also evaluate to
- a type, which is generated recursively.
-?LETSHRINK(<List_of_variables>, <List_of_types>, <Generator>)
- This is created by combining a ?LET and a ?SHRINK macro. Instances are
- generated by applying a randomly generated list of values inside <Generator>
- (just like a ?LET, with the added constraint that the variables and types
- must be provided in a list - alternatively, <List_of_types> 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(<Generator>)
- This construct returns a type whose only purpose is to delay the evaluation
- of <Generator> (<Generator> 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.
-with_parameter(<Parameter_name>, <Value>, <Type>)
- <Parameter_name> will be associated with <Value> while generating <Type>.
- This can be useful when generating commands for stateful systems (as
- described in 'Testing stateful systems' section).
-with_parameters(<Proplist_of_parameters>, <Type>)
- Similar to with_parameter/3, but accepts a list of
- {<Parameter_name>,<Value>} pairs.
-parameter(<Parameter_name>, <Default>)
- Returns the <Value> associated with <Parameter_name>, or <Default> in case
- <Parameter_name> is not associated with any value.
-parameter(<Parameter_name>)
- Equivalent to parameter(<Parameter_name>, undefined).
-
-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 the
-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 1 and grows automatically during
-testing.
-
-?SIZED(<S>, <Generator>)
- Creates a new type, whose instances are produced by replacing all
- appearances of the <S> parameter inside the statement block <Generator> with
- the value of the 'size' parameter. It's OK for the <Generator> to return a
- type - in that case, an instance of the inner type is generated recursively.
-resize(<New_size>, <Type>)
- Overrides the 'size' parameter used when generating instances of <Type> with
- <New_size>. Has no effect on size-less types, such as unions. Also, this
- will not affect the generation of any internal types contained in <Type>,
- 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.
-
-
---------------------------------------------------------------------------------
-Native types support -> moved to proper_typeserver.erl
---------------------------------------------------------------------------------
-
-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
-
-
---------------------------------------------------------------------------------
-Spec testing -> moved to proper.erl
---------------------------------------------------------------------------------
-
-You can test the accuracy of an exported function's spec by running:
- proper:check_spec(mfa()).
- or
- proper:check_spec(mfa(), <option/options>).
-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:
- proper:check_specs(<Module>).
- or
- proper:check_specs(<Module>, <option/options/).
-The behaviour of proper:check_specs is similar to that of proper:module.
-
-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.
-
-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.
-
-
---------------------------------------------------------------------------------
-Symbolic datatypes -> moved to proper_symb.erl
---------------------------------------------------------------------------------
-
-When writing properties that involve abstract data types, such as dicts or sets,
-it is usually best to avoid dealing with the ADTs' internal representations
-directly. Working, instead, with a symbolic representation of an ADT's
-construction process (series of API calls) has several benefits:
-
-* Failing testcases are easier to read and understand. Compare:
- {call,sets,from_list,[[1,2,3]]}
- with:
- {set,3,16,16,8,80,48,
- {[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]},
- {{[],[3],[],[],[],[],[2],[],[],[],[],[1],[],[],[],[]}}}
-* Failing testcases are easier to shrink.
-* It is especially useful when testing the datatype itself: Certain
- implementation errors may depend on some particular selection and ordering of
- API calls, thus it is important to cover the entire ADT construction API.
-
-PropEr supports the symbolic representation of datatypes, using the following
-syntax:
-
-* {call,<Module>,<Function>,<Arguments>}: This represents a call to the API
- function <Module>:<Function> with arguments <Arguments>. Each of the arguments
- may be a symbolic call itself or contain other symbolic calls in lists or
- tuples of arbitrary depth.
-* {'$call',<Module>,<Function>,<Arguments>}: Identical to the above, but gets
- evaluated automatically before being applied to a property.
-* {var,<Atom>}: This contruct serves as a placeholder for values that are not
- known at type construction time. It will be replaced by the actual value of
- the variable during evaluation.
-
-The following functions, automatically imported from the proper_symb module
-(unless PROPER_NO_IMPORTS is defined), can be used when working with symbolic
-instances:
-
-* eval(<Symbolic_instance>): Intended for use inside the property-testing code,
- this function evaluates a symbolic instance.
-* eval(<VarValues>, <Symbolic_instance>): Same as above, but accepts a proplist
- of variable names and values, to be replaced anywhere inside the symbolic
- instance before proceeding with the evaluation.
-* defined(<Symbolic_instance>): Returns true if the symbolic instance can be
- successfully evaluated (its evaluation doesn't raise an error or exception).
-* well_defined(<Symbolic_instance>): An attribute which can be applied to
- symbolic generators that may produce invalid sequences of operations when
- called. The resulting type is guaranteed to only produce well-defined symbolic
- instances.
-* pretty_print/1,2: Similar in calling convention to eval/1,2, but returns a
- string representation of the call sequence instead of evaluating it.
-
-
---------------------------------------------------------------------------------
-Auto-ADT -> move to proper_symb.erl
---------------------------------------------------------------------------------
-
-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
-tests/stack module, which contains a simple implementation of a stack, or the
-proper/proper_dict module, which wraps the STDLIB dict ADT.
-
-
---------------------------------------------------------------------------------
-Testing stateful code -> moved to proper_statem.erl
---------------------------------------------------------------------------------
-
-PropEr provides the module proper_statem to facilitate testing of stateful
-systems whose side-effects are specified via an abstract state machine. Given a
-callback module implementing the state machine, PropEr can generate random
-symbolic command sequences subject to the constraints (preconditions) of the
-specification.
-
-The symbolic representation of a command has the following syntax:
-
-* {set,{var,<Integer>},{call,<Module>,<Function>,<Arguments>}}: Binds a
-symbolic variable to the result of a symbolic call.
-
-During command generation we use symbolic variables to bind the results of
-symbolic calls. Therefore, the state of the abstract state machine might (and
-usually does) contain symbolic variables and/or symbolic calls, which are
-necessary to operate on symbolic variables. Thus, we refer to it as symbolic
-state.
-
-As a next step, symbolic command sequences are evaluated in order to check that
-command execution behaves according to the state machine specifications
-(postconditions). During this phase, symbolic calls are evaluated and symbolic
-variables are replaced by their corresponding real values. Now we refer to the
-state as dynamic state.
-
-
-More specifically, the following functions must be exported from the callback
-module implementing the abstract state machine:
-
-* initial_state(): Specifies the (symbolic) initial state of the state machine.
-This state will be evaluated at command execution time to produce the actual
-initial state. The function is not only called at command generation time, but
-also in order to initialize the state every time the command sequence is run
-(i.e. during normal execution, while shrinking and when checking a
-counterexample). For this reason, it should be deterministic.
-* command(<Symbolic_state>): Generates a symbolic call to be included in the
-command sequence, given the current <Symbolic_state> of the state machine.
-However, before the call is actually included, a precondition is checked.
-* precondition(<Symbolic_state>, <Symbolic_call>): Specifies the precondition
-that should hold so that <Symbolic_call> can be included in the command
-sequence, given the current <Symbolic_state> of the state machine. In case
-precondition doesn't hold, a new call is chosen using the command/1
-generator. If preconditions are very strict, it will take a lot of tries for
-PropEr to randomly choose a valid command. Testing will be stopped in case the
-'constraint_tries' limit is reached (see the 'Options'section).
-* postcondition(<Dynamic_state>, <Symbolic_call>, <Result>): Specifies the
-postcondition that should hold about the <Result> of the evaluation of
-<Symbolic_call>, given the current <Dynamic_state> of the state machine.
-This function is called during command execution time, this is why the state
-is dynamic.
-* next_state(<Symbolic_state> | <Dynamic_state>, <Result>, <Symbolic_call>):
-Specifies the next state of the state machine, given the current state, the
-<Symbolic_call> chosen and its <Result>. This function is called both at
-command generation and command execution time in order to determine the next
-state, therefore the <Result> can be either symbolic (i.e. containing symbolic
-variables and/or symbolic calls) or dynamic (i.e. containing real values).
-
-
-The following functions, automatically imported from the proper_statem module
-(unless PROPER_NO_IMPORTS is defined), can be used when working with stateful
-code:
-
-* commands(<Module>): A special PropEr type which generates random command
-sequences, as specified by the absract state machine in <Module>. The initial
-state is specified by <Module>:initial_state().
-* commands(<Module>, <Symbolic_state>): Similar to commands/1, but generated
-command sequences always start at <Symbolic_state>. In this case, the first
-command is always {init,<Symbolic_state>} and is used to correctly initialize
-the state every time the command sequence is run (i.e. during normal execution,
-while shrinking and when checking a counterexample).
-In this case, <Module>:initial_state/0 is never called.
-* more_commands(<N>, <Generator>): Increases the maximum length of command
-sequences generated within Generator by a factor <N>.
-
-* run_commands(<Module>, <Cmds>): This function runs a given command sequence
-<Cmds> according to the state machine specified in <Module>. The result is a
-tuple of the form: {<History>,<Dynamic_state>,<Statem_result>}.
- - <History> contains the execution history of all commands that were executed
- without raising an exception. It contains tuples of the form {<Dynamic_state>,
- <Result>}, specifying the <Dynamic_state> prior to command execution and the
- actual <Result> of the command.
- - <Dynamic_state> contains the state of the abstract state machine at the
- moment when execution stopped.
- - <Statem_result> specifies the overall result of command execution. It
- can be one of the following:
- -- 'ok': all commands were successfully run and all postconditions were
- true
- -- 'initialization_error': there was an error while evaluating the initial
- state
- -- {'postcondition', <Boolean> | <Exception>}: a postcondition was false
- or raised an exception
- -- {'precondition', <Boolean> | <Exception>}: a precondition was false or
- raised an exception
- -- <Exception>: an exception was raised while running a command
-* run_commands(<Module>, <Cmds>, <Environment>): Similar to run_commands/2,
-but also accepts a list of {<Key>,<Value>} pairs. Keys may be used in symbolic
-variables (i.e. {var,<Key>}) whithin the command sequence <Cmds>. These
-symbolic variables will be replaced by their corresponding <Value> during
-command execution.
-
-* command_names(<Cmds>): Extracts the names of the commands in a given command
-sequence in the form of MFAs. It is useful in combination with functions such
-as aggregate/2,3 in order to collect statistics about command execution.
-* state_after(<Module>, <Cmds>): Returns the symbolic state after running
-the command sequence <Cmds> according to the state machine found in <Module>.
-The commands are not actually executed.
-* zip(<listA>, <listB>): Behaves like lists:zip/2, but listA, listB do no not
-necessarily have equal length. Zipping stops when the shortest list stops. This
-is useful for zipping a command sequence with its (failing) execution history.
-
-Examples of sample properties to check can be found at examples/pdict_statem
-and examples/ets_statem. These modules contain an abstract state machine
-specification for testing operations on the process dictionary and ets tables
-respectively.
-
-
---------------------------------------------------------------------------------
-Parallel testing -> moved to proper_statem.erl
---------------------------------------------------------------------------------
-
-After ensuring that a system's behaviour can be described via an abstract state
-machine when commands are executed sequentially, it is possible to move to
-parallel testing. The same state machine can be used to generate command
-sequences that will be executed concurrently to test for race conditions.
-A parallel testcase consists of a command list, which is run sequentially to put
-the system in a random state, and a list of concurrent tasks. These tasks are
-also command lists, but they are executed concurrently in separate processes.
-After running a parallel testcase, PropEr uses the state machine specification
-to check if the results observed could have been produced by a possible
-serialization of the concurrent tasks. If no such serialization is possible,
-then an atomicity violation is detected.
-
-The following functions, automatically imported from the proper_statem module
-(unless PROPER_NO_IMPORTS is defined), can be used for parallel testing:
-
-* parallel_commands(<Module>): A special PropEr type which generates parallel
-testcases from the absract state machine specified in <Module>. The initial
-state is specified by <Module>:initial_state().
-* parallel_commands(<Module>, <Symbolic_state): Similar to parallel_commands/1,
-but generated command sequences always start at <Symbolic_state>.
-* run_parallel_commands(<Module>, <TestCase>): This function runs a parallel
-<TestCase> according to the specifications in <Module>. The result is a tuple
-of the form: {<Sequential_history>,<Parallel_history>,<Statem_result>}.
- - <Sequential_history> contains the execution history of the sequential
- prefix
- - <Parallel_history> contains the execution history of each of the
- concurrent tasks.
- - <Statem_result> specifies the outcome of the attemp to serialize command
- execution, based on the results observed. It can be one of the following:
- -- 'ok'
- -- 'no_possible_interleaving'
-* run_parallel_commands(<Module>, <TestCase>, <Environment>): Similar to
-run_parallel_commands/2, but also accepts an <Environment> used for symbolic
-variable evaluation, exactly as described in run_commands/3.
-
-Note: in its current implementation PropEr might not be able to generate
-suitable concurrent tasks for each test. In this case, an 'f' is printed on
-screen to inform the user.
-
-An example of a sample property for parallel testing can be found at
-examples/ets_statem, where we test concurrent operations on a public ets table.
-
-
---------------------------------------------------------------------------------
-PropEr fsm -> moved to proper_fsm.erl
---------------------------------------------------------------------------------
-
-PropEr provides another useful module for testing stateful systems, in
-particular those that can be better described as a finite state machine.
-For PropEr, an FSM is a triple {S0, D, S}, where S0 is the initial state,
-D a set of possible updates (transitions) and S a finite set of states.
-
-* State representation
-Following the convention used in gen_fsm behaviour, a state is fully described
-by a StateName and some StateData. StateName is used to denote a state of
-the state machine and StateData is used to denote the internal state of the
-Erlang process which implements the state machine. States are fully represented
-as tuples {StateName, StateData}.
-
-StateName is usually an atom (i.e. the name of the state), but can also be a
-tuple. In the latter case, the first element of the tuple must be an atom
-specifying the name of the state, whereas the rest of the elements can be
-arbitrary terms specifying state attributes.
-For example, when implementing the fsm of an elevator which can reach N
-different floors, the StateName for each floor could be {floor,K}, 1 <= K <= N.
-StateData can be an arbitrary term, but is usually a record.
-
-* Transition represantation
-Transitions are represented as tuples {TargetState, {call,M,F,ArgsGen}}. This
-means that performing the specified symbolic call at the current state of the
-fsm will lead to TargetState. The atom <history> can be used as TargetState to
-denote that a transition does not change the current state of the fsm.
-
-
-The following functions must be exported from the callback module implementing
-the finite state machine:
-
-* initial_state(): Specifies the initial state_name of the fsm. As in
-proper_statem:initial_state/0, its result should be deterministic.
-* initial_state_data() : Specifies the (symbolic) initial state_data. As in
-proper_statem:initial_state/0, its result should be deterministic.
-* StateName(<StateData>): There should be one instance of this function for
-each possible state name StateName. In case StateName is a tuple the function
-takes a different form, described just below. The function returns a list
-of possible transitions from the current state {StateName,StateData}.
-At command generation time, the instance of this function with the same name
-as the current state name StateName is called to return the list of possible
-transitions. Then, PropEr will randomly choose a transition and, according to
-that, generate the next symbolic call to be included in the command sequence.
-However, before the call is actually included, a precondition that might
-impose constraints on <StateData> is checked.
-Note also that PropEr detects transitions that would raise an exception of class
-<error> at generation time (not earlier) and does not choose them. This feature
-can be used to include conditional transitions that depend on the <StateData>.
-* StateName(<Attr1>, ..., <AttrN>, <StateData>): There should be one instance
-of this function for each possible state name {StateName,<Attr1>,...,<AttrN>}.
-The function has similar beaviour to StateName/1, described above.
-* weight(<FromState>, <TargetState>, <Call>): This is an optional callback.
-When it is not defined (or not exported), transitions are chosen with equal
-probability. When it is defined, it assigns an integer weight to transitions
-from <FromState> to <TargetState> triggered by symbolic call <Call>. In this
-case, each transition is chosen with probability proportional to the weight
-assigned.
-* precondition(<FromState>, <TargetState>, <StateData>, <Call>):
-Similar to proper_statem:precondition/2. Specifies the precondition that should
-hold about <StateData> so that <Call> can be included in the command sequence.
-In case precondition doesn't hold, a new transition is chosen using the
-appropriate StateName/1 generator (more specifically FromState/1).
-It is possible for more than one transitions to be triggered by the same
-symbolic call and lead to different target states. In this case, at most one of
-the target states may have a true precondition. Otherwise, PropEr will not be
-able to detect which transition was chosen and an exception will be raised.
-Preconditions are also very important for the shrinking procedure. When
-attempting to shrink fsm command sequences, we try to eliminate commands that
-do not contribute to failure, ensuring that all preconditions still hold.
-* postcondition(<FromState>, <TargetState>, <StateData>, <Call>, <Result>):
-Similar to proper_statem:postcondition/3. Specifies the postcondition that
-should hold about the <Result> of the evaluation of <Call>.
-* next_state_data(<FromState>, <TargetState>, <StateData>, <Result>, <Call>):
-Similar to proper_statem:next_state/3. Specifies how the transition from
-<FromState> to <TargetState> triggered by <Call> affects the <StateData>.
-<Result> refers to the result of <Call> and can be either symbolic or dynamic.
-
-
-The following functions can be used when working with finite state machines.
-Due to name conflicts with functions automatically imported from proper_statem,
-a fully qualified call is needed, i.e. proper_fsm:Fun(Args).
-
-* proper_fsm:commands(<Module>): A special PropEr type which generates random
-command sequences, as specified by the finite state machine in <Module>. The
-initial state is {<Module>:initial_state(), <Module>:initial_state_data()}.
-* proper_fsm:commands(<Module>, <Symbolic_state>): Similar to commands/1, but
-generated command sequences always start at <Symbolic_state>, which should be
-a tuple {<StateName>, <StateData>}. In this case, the first command is always
-{init,<Symbolic_state>} and is used to correctly initialize the state every time
-the command sequence is run (i.e. during normal execution, while shrinking and
-when checking a counterexample).
-
-* proper_fsm:run_commands(<Module>, <Cmds>): This function runs a given command
-sequence <Cmds> according to the finite state machine specified in <Module>. The
-result is a tuple of the form: {<History>,<Dynamic_state>,<Fsm_result>}.
-See proper_statem:run_commands/2 for more details. <Fsm_result> has the same
-form and meaning as <Statem_result>.
-* proper_fsm:run_commands(<Module>, <Cmds>, <Environment>): Similar to
-run_commands/2, but also accepts an <Environment> used for symbolic variable
-evaluation, exactly as described in proper_statem:run_commands/3.
-
-* proper_fsm:state_names(<History>): Extracts the names of the states from a
-given command execution history. It is useful in combination with functions such
-as aggregate/2,3 in order to collect statistics about state transitions during
-command execution.
-
-Examples of sample properties to check can be found at examples/elevator_fsm,
-containing a finite state machine specification for an elevator.
-
-
---------------------------------------------------------------------------------
-Errors -> moved to proper.erl
---------------------------------------------------------------------------------
-
-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.
-
-
---------------------------------------------------------------------------------
-Demo functions -> moved to proper_gen.erl and proper_typeserver.erl
---------------------------------------------------------------------------------
-
-You can use the following functions to try out the random instance generation,
-shrinking and type translation subsystems:
-
-* proper_gen:pick(<Type>):
- equivalent to proper_gen:pick(<Type>, 10)
-* proper_gen:pick(<Type>, <Size>):
- Generates a random instance of <Type>, of size <Size>.
-* proper_gen:sample(<Type>):
- equivalent to proper_gen:sample(<Type>, 10, 20)
-* proper_gen:sample(<Type>, <Start_Size>, <End_Size>):
- Generates and prints one random instance of <Type> for each size from
- <Start_Size> up to <End_Size>.
-* proper_gen:sampleshrink(<Type>):
- equivalent to proper_gen:sampleshrink(<Type>, 10)
-* proper_gen:sampleshrink(<Type>, <Size>):
- Generates a random instance of <Type>, of size <Size>, then shrinks it as
- far as it goes. The value produced on each step of the shrinking process is
- printed on the screen.
-* proper_typeserver:demo_translate_type(<Module>, <Type_Expr>):
- Translates the native type expression <Type_Expr> (which should be provided
- inside a string) into a PropEr type, which can then be passed to any one
- of the above demo functions. PropEr acts as if it found this type expression
- inside the code for <Module>.
-* proper_typeserver:demo_is_instance(<Term>, <Module>, <Type_Expr>):
- Checks if <Term> is a valid instance of native type <Type_Expr> (which
- should be provided inside a string). PropEr acts as if it found this type
- expression inside the code for <Module>.
-
-CAUTION: These functions should never be used inside properties. They are meant
-for demonstration purposes only.
-
-
---------------------------------------------------------------------------------
-Incompatibilities with QuviQ's QuickCheck -> moved to proper.erl
---------------------------------------------------------------------------------
-
-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.
View
147 README.md
@@ -0,0 +1,147 @@
+PropEr
+======
+
+Contact information and license
+-------------------------------
+
+PropEr (PROPerty-based testing tool for ERlang) is a QuickCheck-inspired
+open-source property-based testing tool for Erlang, developed by Manolis
+Papadakis <manopapad@gmail.com>, Eirini Arvaniti <eirinibob@gmail.com> and
+Kostis Sagonas <kostis@cs.ntua.gr>. The base PropEr system was written mainly by
+Manolis Papadakis, and the stateful code testing subsystem by Eirini Arvaniti.
+
+You can reach PropEr's developers in the following ways:
+
+* by email: at <proper@softlab.ntua.gr>
+* on the web: at [the project's home page](http://proper.softlab.ntua.gr), or
+ at [the project's github page](https://github.com/manopapad/proper)
+
+We welcome user contributions and feedback (comments, suggestions, feature
+requests, bug reports, patches etc.).
+
+Copyright 2010-2011 by Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas.
+
+This program is distributed under the GPL, version 3 or later. Please see the
+COPYING file for details.
+
+
+Introduction
+------------
+
+Traditional testing methodologies essentially involve software testers writing a
+series of test inputs for their programs, along with their corresponding
+expected outputs, then running the program with these inputs and observing
+whether it behaves as expected. This method of testing, while simple and easy to
+automate, suffers from a few problems, such as:
+
+* Writing test cases by hand is tedious and time consuming.
+* It is hard to know whether the test suite covers all aspects of the software
+ under test.
+
+Property-based testing is a novel approach to software testing, where the tester
+needs only specify the generic structure of valid inputs for the program under
+test, plus certain properties (regarding the program's behaviour and the input-
+output relation) which are expected to hold for every valid input. A property-
+based testing tool, when supplied with this information, should randomly
+produce progressively more complex valid inputs, then apply those inputs to the
+program while monitoring its execution, to ensure that it behaves according to
+its specification, as outlined in the supplied properties.
+
+Here are a few examples of simple properties a user may wish to test, expressed
+in natural language:
+
+* The program should accept any character string and convert all lowercase
+ letters inside the string to uppercase.
+* The program should accept any list of integers. If the input list is at
+ least 4 elements long, the program should return the 4th largest integer in
+ the list, else it should throw an exception.
+
+PropEr is such 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.
+
+PropEr is also tightly integrated with Erlang's type language:
+
+* Types expressed in the Erlang type language can be used instead of
+ generators written in PropEr's own type system as input data specifications.
+* Generators for ADTs can be constructed automatically using the ADTs' API
+ functions.
+* PropEr can test functions automatically, based solely on information
+ provided in their specs.
+
+
+Quickstart guide
+----------------
+
+* Obtain a copy of PropEr's sources.
+* Compile PropEr: run `make` (or `make all`, if you also want to build the
+ documentation; in that case, you are going to need the syntax_tools
+ application and a recent version of `EDoc`).
+* Add PropEr's base directory to your Erlang library path, using one of the
+ following methods:
+ 1. `ERL_LIBS` environment variable: Add the following line to your shell
+ startup file (`~/.bashrc` in the case of the Bash shell):
+
+ export ERL_LIBS=/full/path/to/proper
+
+ 2. Erlang resource file: Add the following line to your `~/.erlang` file:
+
+ code:load_abs("/full/path/to/proper").
+
+* Add the following include line to all source files that contain properties:
+
+ -include_lib("proper/include/proper.hrl").
+
+* Compile those source files, preferably with `debug_info` enabled.
+* For each property, run:
+
+ proper:quickcheck(your_module:some_property()).
+
+
+Where to go from here
+---------------------
+
+To get started on using PropEr, see the tutorials and testing tips provided on
+[PropEr's home page](http://proper.softlab.ntua.gr). On the same site you can
+find a copy of PropEr's API documentation (you can also build this from source
+if you prefer, by running `make doc`), as well as links to more resources on
+property-based testing.
+
+
+Common Problems
+---------------
+
+### Using PropEr in conjunction with EUnit
+
+The main issue is that both systems define a `?LET` macro. To avoid a potential
+clash, simply include PropEr's header file before EUnit's. That way, any
+instance of `?LET` will count as a PropEr `?LET`.
+
+### Using PropEr under Erlang/OTP R13B03 or older
+
+PropEr makes heavy use of recursive types, which are unsupported on versions of
+the Erlang/OTP distribution prior to R13B04. To compile PropEr on such a system,
+add `{d,'NO_TYPES'}` to the `erl_opts` option inside `rebar.config`. This
+enables the spec+type-stripping parse transform included in PropEr, which fixes
+the problem by stripping all type information from PropEr's source files during
+compilation.
+
+
+Incompatibilities with QuviQ's QuickCheck
+-----------------------------------------
+
+We have generally tried to keep PropEr's notation and output format as compatible
+as possible with QuviQ's QuickCheck, to allow for the reuse of existing testing
+code written for that tool. 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/1` differs from `eqc_gen:pick/1` in return value format.
+* PropEr handles `size` differently from QuickCheck.
+* `proper:module/2` accepts options in the second argument instead of the
+ first
View
21 doc/overview.edoc
@@ -25,4 +25,23 @@ This is the source for PropEr's overview page.
@author Manolis Papadakis
@title PropEr: A QuickCheck-inspired property-based testing tool for Erlang
-@doc No top-level documentation yet.
+
+@doc This is PropEr's reference manual. The bulk of the PropEr API is contained
+in the documentation for the following modules:
+
+<dl>
+<dt>{@link proper}</dt>
+<dd>how to write properties, how to invoke PropEr, different modes of
+ operation</dd>
+<dt>{@link proper_types}</dt>
+<dd>how to write input data generators for properties</dd>
+<dt>{@link proper_symb}</dt>
+<dd>writing generators for ADTs, both manually and automatically</dd>
+<dt>{@link proper_typeserver}</dt>
+<dd>more information on PropEr's integration with the Erlang type language</dd>
+<dt>{@link proper_fsm}</dt>
+<dd>using PropEr to test stateful systems modeled as finite state machines</dd>
+<dt>{@link proper_statem}</dt>
+<dd>using PropEr to test stateful reactive systems specified via an abstract
+ state machine</dd>
+</dl>
View
4 make_doc
@@ -108,10 +108,10 @@ process(Filename) ->
pretty_print(Forms, Comments) ->
FormsWithLines = add_lines_to_forms(Forms),
CommentsWithLines =
- [{[Line],[["%",Str,"\n"] || Str <- Text]}
+ [{[Line],[["%",Str,"\n"] || Str <- Text] ++ "%@end\n"}
|| {Line,_Col,_Ind,Text} <- Comments],
CodeWithLines = lists:keymerge(1, FormsWithLines, CommentsWithLines),
- [[S,"\n"] || {_L,S} <- CodeWithLines].
+ [S || {_L,S} <- CodeWithLines].
-spec add_lines_to_forms([abs_form()]) -> [charlist_with_lines()].
add_lines_to_forms(Forms) ->
View
542 src/proper.erl
@@ -20,89 +20,92 @@
%%% @copyright 2010-2011 Manolis Papadakis, Eirini Arvaniti 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) ==
+%%% == 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. More complex (and useful) properties can be written by
-%%% wrapping such a boolean expression with one or more of the following
-%%% wrappers:
-%%% <ul>
-%%% <li><b>`?FORALL(<Xs>, <Xs_type>, <Prop>)'</b>
-%%% <p>The `<Xs>' field can either be a single variable, a tuple of variables
+%%% `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:
+%%%
+%%% <dl>
+%%% <dt>`?FORALL(<Xs>, <Xs_type>, <Prop>)'</dt>
+%%% <dd>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
+%%% 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
%%% {@link proper_types} module, and types declared in Erlang's built-in
-%%% typesystem (we refer to such types in this README as
-%%% <em>native types</em>) may be used in the `<Xs_type>' field. The use of
-%%% native types in `?FORALLs' is subject to some limitations, as described
-%%% in the "Native types support" section.
-%%% 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.</p>
-%%% </li>
-%%% <li><b>`?IMPLIES(<Precondition>, <Prop>)'</b>
-%%% <p>This wrapper only makes sense when in the scope of at least one
+%%% typesystem (we will refer to such types in as <em>native types</em>) 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
+%%% {@link 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.</dd>
+%%% <dt>`?IMPLIES(<Precondition>, <Prop>)'</dt>
+%%% <dd>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.</p>
-%%% </li>
-%%% <li><b>`?WHENFAIL(<Action>, <Prop>)'</b>
-%%% <p>The `<Action>' field should contain an expression or statement block
+%%% 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.</dd>
+%%% <dt>`?WHENFAIL(<Action>, <Prop>)'</dt>
+%%% <dd>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.</p>
-%%% </li>
-%%% <li><b>`?TRAPEXIT(<Prop>)'</b>
-%%% <p>If the code inside `<Prop>' spawns and links to a process that dies
+%%% application.</dd>
+%%% <dt>`?TRAPEXIT(<Prop>)'</dt>
+%%% <dd>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.</p>
-%%% </li>
-%%% <li><b>`?TIMEOUT(<Time_limit>, <Prop>)'</b>
-%%% <p>Signifies that `<Prop>' should be considered failing if it takes more
+%%% failure, instead of crashing. `?TRAPEXIT' cannot contain any more
+%%% wrappers.</dd>
+%%% <dt>`?TIMEOUT(<Time_limit>, <Prop>)'</dt>
+%%% <dd>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.</p>
-%%% </li>
+%%% contain any more wrappers.</dd>
+%%% <dt>`conjunction(<SubProps>)'</dt>
+%%% <dd>See the documentation for {@link conjunction/1}.</dd>
+%%% <dt>`equals(<A>, <B>)'</dt>
+%%% <dd>See the documentation for {@link equals/2}.</dd>
+%%% </dl>
+%%%
+%%% There are also multiple wrappers that can be used to collect statistics on
+%%% the distribution of test data:
+%%%
+%%% <ul>
+%%% <li>{@link collect/2}</li>
+%%% <li>{@link collect/3}</li>
+%%% <li>{@link aggregate/2}</li>
+%%% <li>{@link aggregate/3}</li>
+%%% <li>{@link classify/3}</li>
+%%% <li>{@link measure/3}</li>
%%% </ul>
-%%% 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.
+%%% <span id="external-wrappers"></span>
+%%% 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.
%%%
-%%% Note that failure of a property may also be signified by throwing an
-%%% exception, error or exit.
+%%% <ul>
+%%% <li>{@link numtests/2}</li>
+%%% <li>{@link fails/2}</li>
+%%% <li>{@link on_output/2}</li>
+%%% </ul>
%%%
-%%% For some actual usage examples, see the code in the examples directory. The
-%%% testing modules in the tests directory may also be of interest.
+%%% 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
@@ -119,27 +122,21 @@
%%% reason and exits.
%%%
%%% The return value of PropEr can be one of the following:
+%%%
%%% <ul>
-%%% <li> `true': The property held for all valid produced inputs.</li>
-%%% <li> `false': The property failed for some input.</li>
-%%% <li> `{error, <Type_of_error>}': An error occured - see the
-%%% {@section Errors} section for a description of possible errors.</li>
+%%% <li>`true': The property held for all valid produced inputs.</li>
+%%% <li>`false': The property failed for some input.</li>
+%%% <li>`{error, <Type_of_error>}': An error occured; see the {@section Errors}
+%%% section for more information.</li>
%%% </ul>
%%%
-%%% 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).
+%%% function whose name begins with `prop_'), you can use {@link module/1} or
+%%% {@link 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
@@ -151,124 +148,118 @@
%%%
%%% 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}.
+%%% {@link counterexample/0}. When testing a whole module, run
+%%% {@link 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. If, for some reason, you want to completely
+%%% clean up the process dictionary of PropEr-produced entries, run
+%%% {@link 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.
+%%% (activated by supplying the option `long_result', or by calling
+%%% {@link counterexample/1} or {@link counterexample/2} instead of
+%%% {@link quickcheck/1} and {@link 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 {@link 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):
+%%% previously falsified by running {@link check/2} or {@link check/3}. This
+%%% will return one of the following (both in short- and long-result mode):
+%%%
%%% <ul>
-%%% <li> `true': The property now holds for this test case.</li>
-%%% <li> `false': The test case still fails (although not necessarily for the
+%%% <li>`true': The property now holds for this test case.</li>
+%%% <li>`false': The test case still fails (although not necessarily for the
%%% same reason as before).</li>
-%%% <li> `{error, <Type_of_error>}': An error occured - see the
-%%% {@section Errors} section for a description of possible errors.</li>
+%%% <li>`{error, <Type_of_error>}': An error occured - see the {@section Errors}
+%%% section for more information.</li>
%%% </ul>
-%%% 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
+%%%
+%%% 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 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.
+%%% Options can be provided as an extra argument to most testing functions (such
+%%% as {@link 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}
+%%% section) override any conflicting settings provided as options.
%%%
%%% The available options are:
-%%% <ul>
-%%% <li>`quiet'
-%%% <p>Enables quiet mode - no output is printed on screen while PropEr is
-%%% running.</p></li>
-%%% <li>`verbose'
-%%% <p> Enables verbose mode - this is the default mode of operation.</p></li>
-%%% <li>{`to_file', `<IO_device>'}
-%%% <p>Redirects all of PropEr's output to `<IO_device>', which should be an
-%%% IO device associated with a file opened for writing.</p></li>
-%%% <li>{`on_output', `<output_function>'}
-%%% <p>PropEr will use the supplied function for all output printing. This
+%%%
+%%% <dl>
+%%% <dt>`quiet'</dt>
+%%% <dd>Enables quiet mode - no output is printed on screen while PropEr is
+%%% running.</dd>
+%%% <dt>`verbose'</dt>
+%%% <dd>Enables verbose mode - this is the default mode of operation.</dd>
+%%% <dt>`{to_file, <IO_device>}'</dt>
+%%% <dd>Redirects all of PropEr's output to `<IO_device>', which should be an
+%%% IO device associated with a file opened for writing.</dd>
+%%% <dt>`{on_output, <Output_function>}'</dt>
+%%% <dd>PropEr will use the supplied function for all output printing. This
%%% function should accept two arguments in the style of `io:format/2'.<br/>
%%% CAUTION: The above output control options are incompatible with each
-%%% other.</p></li>
-%%% <li>`long_result'
-%%% <p>Enables long-result mode (see the {@section Counterexamples} section
-%%% for details).</p></li>
-%%% <li>{`numtests', `<Positive_number>'} or simply `<Positive_number>'
-%%% <p>This is equivalent to the {@link numtests/1} property wrapper. Any
-%%% `numtests/1' wrappers in the actual property will overwrite this setting.
-%%% </p></li>
-%%% <li>{`start_size', `<Size>'}
-%%% <p>Specifies the initial value of the `size' parameter (default is 1), see
-%%% the {@section PropEr types} section for details.</p></li>
-%%% <li>{`max_size', `<Size>'}
-%%% <p>Specifies the maximum value of the `size' parameter (default is 42),
-%%% see the {@section PropEr types} section for details.</p></li>
-%%% <li>{`max_shrinks', `<Non_negative_number>'}
-%%% <p>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. </p></li>
-%%% <li>`noshrink'
-%%% <p>Instructs PropEr to not attempt to shrink any failing test cases.
-%%% </p></li>
-%%% <li>{`constraint_tries', `<Positive_number>'}
-%%% <p>Specifies the maximum number of tries before the generator subsystem
-%%% gives up on producing an instance that satisfies a `?SUCHTHAT'
-%%% constraint. Default is 50. </p></li>
-%%% <li>`fails'
-%%% <p>This is equivalent to the {@link fails/1} property wrapper.</p></li>
-%%% <li>{`spec_timeout', `infinity | <Non_negative_number>'}
-%%% <p>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. </p></li>
-%%% <li>`any_to_integer'
-%%% <p>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).</p></li>
-%%% </ul>
-%%%
-%%% == 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.
+%%% other.</dd>
+%%% <dt>`long_result'</dt>
+%%% <dd>Enables long-result mode (see the {@section Counterexamples} section
+%%% for details).</dd>
+%%% <dt>`{numtests, <Positive_number>}' or simply `<Positive_number>'</dt>
+%%% <dd>This is equivalent to the {@link numtests/1} property wrapper. Any
+%%% {@link numtests/1} wrappers in the actual property will overwrite this
+%%% setting.</dd>
+%%% <dt>`{start_size, <Size>}'</dt>
+%%% <dd>Specifies the initial value of the `size' parameter (default is 1), see
+%%% the documentation of the {@link proper_types} module for details.</dd>
+%%% <dt>`{max_size, <Size>}'</dt>
+%%% <dd>Specifies the maximum value of the `size' parameter (default is 42), see
+%%% the documentation of the {@link proper_types} module for details.</dd>
+%%% <dt>`{max_shrinks, <Non_negative_number>}'</dt>
+%%% <dd>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.</dd>
+%%% <dt>`noshrink'</dt>
+%%% <dd>Instructs PropEr to not attempt to shrink any failing test cases.</dd>
+%%% <dt>`{constraint_tries, <Positive_number>}'</dt>
+%%% <dd>Specifies the maximum number of tries before the generator subsystem
+%%% gives up on producing an instance that satisfies a `?SUCHTHAT'
+%%% constraint. Default is 50.</dd>
+%%% <dt>`fails'</dt>
+%%% <dd>This is equivalent to the {@link fails/1} property wrapper.</dd>
+%%% <dt>`{spec_timeout, infinity | <Non_negative_number>}'</dt>
+%%% <dd>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.</dd>
+%%% <dt>`any_to_integer'</dt>
+%%% <dd>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 `any()' is a commonly used type (see the {@section Spec testing}
+%%% section for details).</dd>
+%%% </dl>
%%%
%%% == 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}.
+%%% {@link check_spec/1} or {@link 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}.
+%%% running {@link check_specs/1} or {@link check_specs/2}.
%%%
%%% The use of `check_spec' is subject to the following usage rules:
+%%%
%%% <ul>
%%% <li>Currently, PropEr can't test functions whose range contains a type
%%% that exhibits a certain kind of self-reference: it is (directly or
@@ -285,91 +276,67 @@
%%% <li>Throwing any exception or raising an `error:badarg' is considered
%%% normal behaviour. Currently, users cannot fine-tune this setting.</li>
%%% <li>Only the first clause of the function's spec is considered.</li>
-%%% <li>The only spec constraints we accept are 1is_subtype' constraints whose
+%%% <li>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.</li>
%%% </ul>
%%%
-%%% 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.
-%%% <ul>
-%%% <li>`arity_limit'
-%%% <p>The random instance generation subsystem has failed to produce
+%%%
+%%% <dl>
+%%% <dt>`arity_limit'</dt>
+%%% <dd>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.</p></li>
-%%% <li>`cant_generate'
-%%% <p> The random instance generation subsystem has failed to
+%%% should only be encountered during normal operation.</dd>
+%%% <dt>`cant_generate'</dt>
+%%% <dd>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.</p></li>
-%%% <li>`cant_satisfy'
-%%% <p>All the tests were rejected because no produced test case
+%%% during normal operation.</dd>
+%%% <dt>`cant_satisfy'</dt>
+%%% <dd>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.</p></li>
-%%% <li>`non_boolean_result'
-%%% <p>The property code returned a non-boolean result. Please
-%%% fix your property.</p></li>
-%%% <li>`rejected'
-%%% <p>Only encountered during re-checking, the counterexample does not
+%%% operation.</dd>
+%%% <dt>`non_boolean_result'</dt>
+%%% <dd>The property code returned a non-boolean result. Please
+%%% fix your property.</dd>
+%%% <dt>`rejected'</dt>
+%%% <dd>Only encountered during re-checking, the counterexample does not
%%% match the property, since the counterexample doesn't pass an `?IMPLIES'
-%%% check.</p></li>
-%%% <li>`too_many_instances'
-%%% <p>Only encountered during re-checking, the counterexample
+%%% check.</dd>
+%%% <dt>`too_many_instances'</dt>
+%%% <dd>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.</p></li>
-%%% <li>`type_mismatch'
-%%% <p>The variables' and types' structures inside a `?FORALL' don't
-%%% match. Please check your properties.</p></li>
-%%% <li>{`typeserver', `<SubError>'}
-%%% <p>The typeserver encountered an error. The `<SubError>' field contains
-%%% specific information regarding the error.</p></li>
-%%% <li>{`unexpected', `<Result>'}
-%%% <p>A test returned an unexpected result during normal operation. If you
+%%% instances than there are `?FORALL's in the property.</dd>
+%%% <dt>`type_mismatch'</dt>
+%%% <dd>The variables' and types' structures inside a `?FORALL' don't
+%%% match. Please check your properties.</dd>
+%%% <dt>`{typeserver, <SubError>}'</dt>
+%%% <dd>The typeserver encountered an error. The `<SubError>' field contains
+%%% specific information regarding the error.</dd>
+%%% <dt>`{unexpected, <Result>}'</dt>
+%%% <dd>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.
-%%% </p></li>
-%%% <li>{`unrecognized_option', `<Option>'}
-%%% <p>`<Option>' is not an option that PropEr understands.</p></li>
-%%% </ul>
-%%%
-%%% == 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:
-%%% <ul>
-%%% <li>`?SUCHTHATMAYBE' behaves differently in PropEr.</li>
-%%% <li>`proper_gen:pick' differs from `eqc_gen:pick' in return value format.
-%%% </li>
-%%% <li> PropEr handles `size' differently from QuickCheck.</li>
-%%% <li> `proper:module/2' accepts options in the second argument instead of the
-%%% first.</li>
-%%% </ul>
-%%% @end
+%%% </dd>
+%%% <dt>`{unrecognized_option, <Option>}'</dt>
+%%% <dd>`<Option>' is not an option that PropEr understands.</dd>
+%%% </dl>
-module(proper).
-export([quickcheck/1, quickcheck/2, counterexample/1, counterexample/2,
- check/2, check/3, pure_check/1, pure_check/2, module/1, module/2,
- check_spec/1, check_spec/2, check_specs/1, check_specs/2]).
+ check/2, check/3, module/1, module/2, check_spec/1, check_spec/2,
+ check_specs/1, check_specs/2]).
-export([numtests/2, fails/1, on_output/2, conjunction/1]).
-export([collect/2, collect/3, aggregate/2, aggregate/3, classify/3, measure/3,
with_title/1, equals/2]).
@@ -377,6 +344,7 @@
-export([clean_garbage/0, global_state_erase/0]).
-export([get_size/1, global_state_init_size/1, report_error/2]).
+-export([pure_check/1, pure_check/2]).
-export([forall/2, implies/2, whenfail/2, trapexit/1, timeout/2]).
-export([spawn_link_migrate/1]).
@@ -392,7 +360,6 @@
-define(MISMATCH_MSG, "Error: The input doesn't correspond to this property: ").
-
%%-----------------------------------------------------------------------------
%% Test types
%%-----------------------------------------------------------------------------
@@ -416,23 +383,32 @@
-type side_effects_fun() :: fun(() -> 'ok').
-type fail_actions() :: [side_effects_fun()].
-type 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'.
-type tag() :: atom().
-type title() :: atom() | string().
-type 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'.
-type numeric_stat() :: number() | 'undefined'.
-type numeric_stats() :: {numeric_stat(),numeric_stat(),numeric_stat()}.
-type time_period() :: non_neg_integer().
%% TODO: This should be opaque.
-%% @type outer_test()
+%% @type outer_test(). A testable property that has optionally been wrapped with
+%% one or more <a href="#external-wrappers">external wrappers</a>.
-type outer_test() :: test()
| numtests_clause()
| fails_clause()
| on_output_clause().
%% TODO: This should be opaque.
%% TODO: Should the tags be of the form '$...'?
-%% @type test()
+%% @type test(). A testable property that has not been wrapped with an
+%% <a href="#external-wrappers">external wrapper</a>.
-type test() :: boolean()
| forall_clause()
| conjunction_clause()
@@ -521,6 +497,7 @@
bound :: imm_testcase() | counterexample(),
actions :: fail_actions(),
performed :: pos_integer()}).
+%% @alias
-type error() :: {'error', error_reason()}.
-type pass_reason() :: 'true_prop' | 'didnt_crash'.
@@ -539,7 +516,6 @@
-type run_result() :: #pass{performed :: 'undefined'}
| #fail{performed :: 'undefined'}
| error().
--type shrinking_result() :: {non_neg_integer(),imm_testcase()}.
-type imm_result() :: #pass{reason :: 'undefined'} | #fail{} | error().
-type long_result() :: 'true' | counterexample() | error().
-type short_result() :: boolean() | error().
@@ -547,6 +523,7 @@
-type long_module_result() :: [{mfa(),counterexample()}] | error().
-type short_module_result() :: [mfa()] | error().
-type module_result() :: long_module_result() | short_module_result().
+-type shrinking_result() :: {non_neg_integer(),imm_testcase()}.
%%-----------------------------------------------------------------------------
@@ -659,8 +636,8 @@ save_counterexample(CExm) ->
put('$counterexample', CExm),
ok.
-%% @doc Retrieves the last simplest counterexample produced by PropEr during a
-%% failing run. The counterexample can be retrieved after testing has finished.
+%% @doc Retrieves the last (simplest) counterexample produced by PropEr during
+%% the most recent testing run.
-spec counterexample() -> counterexample() | 'undefined'.
counterexample() ->
get('$counterexample').
@@ -670,13 +647,13 @@ save_counterexamples(CExms) ->
put('$counterexamples', CExms),
ok.
-%% @doc Returns a counterexample for each failing property, when testing a
-%% whole module with {@link module/1} or {@link module/2}.
+%% @doc Returns a counterexample for each failing property of the most recent
+%% module testing run.
-spec counterexamples() -> [{mfa(),counterexample()}] | 'undefined'.
counterexamples() ->
get('$counterexamples').
-%% @doc Cleans up the process dictionary of PropEr-produced entries.
+%% @doc Cleans up the process dictionary of all PropEr-produced entries.
-spec clean_garbage() -> 'ok'.
clean_garbage() ->
erase('$counterexample'),
@@ -688,13 +665,12 @@ clean_garbage() ->
%% Public interface functions
%%-----------------------------------------------------------------------------
-%% @doc Runs PropEr on the specified property.
+%% @doc Runs PropEr on the property `OuterTest'.
-spec quickcheck(outer_test()) -> result().
quickcheck(OuterTest) ->
quickcheck(OuterTest, []).
%% @doc Same as {@link quickcheck/1}, but also accepts a list of options.
-%% For information on available option see the {@section Options} section.
-spec quickcheck(outer_test(), user_opts()) -> result().
quickcheck(OuterTest, UserOpts) ->
try parse_opts(UserOpts) of
@@ -707,19 +683,17 @@ quickcheck(OuterTest, UserOpts) ->
{error, Reason}
end.
-%% @doc Retrieves the last simplest counterexample produced by PropEr during
-%% a failing run. The counterexample can be retrieved after testing has
-%% finished.
+%% @equiv quickcheck(OuterTest, [long_result])
-spec counterexample(outer_test()) -> long_result().
counterexample(OuterTest) ->
counterexample(OuterTest, []).
%% @doc Same as {@link counterexample/1}, but also accepts a list of options.
-%% For information on available option see the {@section Options} section.
-spec counterexample(outer_test(), user_opts()) -> long_result().
counterexample(OuterTest, UserOpts) ->
quickcheck(OuterTest, add_user_opt(long_result,UserOpts)).
+%% @private
%% @doc Runs PropEr in pure mode. 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.
@@ -727,8 +701,8 @@ counterexample(OuterTest, UserOpts) ->
pure_check(OuterTest) ->
pure_check(OuterTest, []).
+%% @private
%% @doc Same as {@link pure_check/2}, but also accepts a list of options.
-%% For information on available option see the {@section Options} section.
-spec pure_check(outer_test(), user_opts()) -> result().
pure_check(OuterTest, ImmUserOpts) ->
Parent = self(),
@@ -743,8 +717,7 @@ pure_check(OuterTest, ImmUserOpts) ->
check_spec(MFA) ->
check_spec(MFA, []).
-%% @doc Same as {@link check_spec/2}, but also accepts a list of options.
-%% For information on available option see the {@section Options} section.
+%% @doc Same as {@link check_spec/1}, but also accepts a list of options.
-spec check_spec(mfa(), user_opts()) -> result().
check_spec(MFA, UserOpts) ->
try parse_opts(UserOpts) of
@@ -756,14 +729,13 @@ check_spec(MFA, UserOpts) ->
{error, Reason}
end.
-%% @doc Re-checks a specific counterexample against the property that it
-%% previously falsified.
+%% @doc Re-checks a specific counterexample `CExm' against the property
+%% `OuterTest' that it previously falsified.
-spec check(outer_test(), counterexample()) -> short_result().
check(OuterTest, CExm) ->
check(OuterTest, CExm, []).
%% @doc Same as {@link check/2}, but also accepts a list of options.
-%% For information on available option see the {@section Options} section.
-spec check(outer_test(), counterexample(), user_opts()) -> short_result().
check(OuterTest, CExm, UserOpts) ->
try parse_opts(UserOpts) of
@@ -776,25 +748,24 @@ check(OuterTest, CExm, UserOpts) ->
{error, Reason}
end.
-%% @doc Tests all properties exported from a module (a property is a 0-arity
-%% function whose name begins with "`prop_'").
+%% @doc Tests all properties (i.e., all 0-arity functions whose name begins with
+%% `prop_')exported from module `Mod'.
-spec module(mod_name()) -> module_result().
module(Mod) ->
module(Mod, []).
%% @doc Same as {@link module/1}, but also accepts a list of options.
-%% For information on available option see the {@section Options} section.
-spec module(mod_name(), user_opts()) -> module_result().
module(Mod, UserOpts) ->
multi_test_prep(Mod, test, UserOpts).
-%% @doc Tests all exported functions of a module against their spec.
+%% @doc Tests all exported, `-spec'ed functions of a module `Mod' against their
+%% spec.
-spec check_specs(mod_name()) -> module_result().
check_specs(Mod) ->
check_specs(Mod, []).
%% @doc Same as {@link check_specs/1}, but also accepts a list of options.
-%% For information on available option see the {@section Options} section.
-spec check_specs(mod_name(), user_opts()) -> module_result().
check_specs(Mod, UserOpts) ->
multi_test_prep(Mod, spec, UserOpts).
@@ -876,23 +847,24 @@ peel_test(Test, Opts) ->
%% TODO: All of these should have a test() or outer_test() return type.
-%% @doc Specifies the number of tests to run. Default is 100.
+%% @doc Specifies the number `N' of tests to run when testing the property
+%% `Test'. Default is 100.
%% @spec numtests(pos_integer(), outer_test()) -> outer_test()
-spec numtests(pos_integer(), outer_test()) -> numtests_clause().
numtests(N, Test) ->
{numtests, N, Test}.
-%% @doc Specifies that we expect the property to fail for some input. The
+%% @doc Specifies that we expect the property `Test' to fail for some input. The
%% property will be considered failing if it passes all the tests.
%% @spec fails(outer_test()) -> outer_test()
-spec fails(outer_test()) -> fails_clause().
fails(Test) ->
{fails, Test}.
+%% @doc 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.
%% @spec on_output(output_fun(), outer_test()) -> outer_test()
-%% @doc Specifies an output function to be used by PropEr for all output
-%% printing. This wrapper is equivalent to the `on_output' option.
-%% (see the {@section Options} section for details).
-spec on_output(output_fun(), outer_test()) -> on_output_clause().
on_output(Print, Test) ->
{on_output, Print, Test}.
@@ -902,11 +874,10 @@ on_output(Print, Test) ->
forall(RawType, DTest) ->
{forall, RawType, DTest}.
-%% @doc Specifies a property is true only if all of its sub-properties are
-%% true. The tags must be distinct atoms. These are used when reporting the
-%% failure of a property (each failing sub-property is reported using its tag)
-%% and inside counterexamples (see the {@section Counterexamples} section
-%% for details).
+%% @doc 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.
%% @spec conjunction([{tag(),test()}]) -> test()
-spec conjunction([{tag(),test()}]) -> conjunction_clause().
conjunction(SubProps) ->
@@ -917,22 +888,20 @@ conjunction(SubProps) ->
implies(Pre, DTest) ->
{implies, Pre, DTest}.
-%% @doc The `Category' field can be an expression or statement block that
-%% evaluates to any term - the test case produced will be categorized under
-%% this 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.
+%% @doc 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.
%% @spec collect(term(), test()) -> test()
-spec collect(term(), test()) -> sample_clause().
collect(Category, Test) ->
collect(with_title(""), Category, Test).
-%% @doc Same as {@link collect/2}, but a takes a fun as an extra first argument.
-%% This fun will be called at the end of testing (in case no test fails) with
-%% a sorted list of collected terms. It is expected to print some statistics
-%% over the collected terms. See also {@link with_title/1}.
+%% @doc Same as {@link collect/2}, but also accepts a fun `Printer' to be used
+%% as the stats printer.
%% @spec collect(stats_printer(), term(), test()) -> test()
-spec collect(stats_printer(), term(), test()) -> sample_clause().
collect(Printer, Category, Test) ->
@@ -952,10 +921,10 @@ aggregate(Sample, Test) ->
aggregate(Printer, Sample, Test) ->
{sample, Sample, Printer, Test}.
-%% @doc Same as {@link collect/2}, but accepts both a single category and a list
-%% of categories. The first argument is a boolean flag. When it is `false', the
-%% produced test case is not counted.
-%% @spec classify(boolean(), term() | sample(), test()) -> test()
+%% @doc Same as {@link 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.
+%% @spec classify(Count::boolean(), term() | sample(), test()) -> test()
-spec classify(boolean(), term() | sample(), test()) -> sample_clause().
classify(false, _TermOrSample, Test) ->
aggregate([], Test);
@@ -964,9 +933,10 @@ classify(true, Sample, Test) when is_list(Sample) ->
classify(true, Term, Test) ->
collect(Term, Test).
-%% @doc The number (or numbers) provided are collected and some numeric
-%% 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.
+%% @doc 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.
%% @spec measure(title(), number() | [number()], test()) -> test()
-spec measure(title(), number() | [number()], test()) -> sample_clause().
measure(Title, Sample, Test) when is_number(Sample) ->
@@ -989,8 +959,8 @@ trapexit(DTest) ->
timeout(Limit, DTest) ->
{timeout, Limit, DTest}.
-%% @doc Returns `true' if `A =:= B', else returns `false' and prints
-%% "`A =/= B'" on screen.
+%% @doc A custom property that evaluates to `true' only if `A =:= B', else
+%% evaluates to `false' and prints "`A =/= B'" on the screen.
%% @spec equals(term(), term()) -> test()
-spec equals(term(), term()) -> whenfail_clause().
equals(A, B) ->
@@ -1799,7 +1769,7 @@ apply_stats_printer(Printer, SortedSample, Print) ->
%% @doc 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 above the statistics.
+%% the given title `Title' above the statistics.
-spec with_title(title()) -> stats_printer().
with_title(Title) ->
fun(S,O) -> plain_stats_printer(S, O, Title) end.
View
13 src/proper_dict.erl
@@ -44,13 +44,14 @@
%% Here are some valid symbolic calls that could be automatically produced using
%% this module's exported functions, for the type dict(atom(),integer()):
%% * {'$call',proper_dict,store,[aa,12,{'$call',proper_dict,new,[]}]}
-%% * {'$call',proper_dict,filter,[<fun>,{'$call',proper_dict,from_list,
-%% [[{a,1},{b,2}]]}]}
-%% * {'$call',proper_dict,merge,[<fun>, {'$call',proper_dict,from_list,[[]]},
-%% {'$call',proper_dict,update,
-%% [aa,<fun>,3,{'$call',proper_dict,new,[]}]}]}
+%% * {'$call',proper_dict,filter,[Fun,{'$call',proper_dict,from_list,
+%% [[{a,1},{b,2}]]}]}
+%% * {'$call',proper_dict,merge,[Fun,
+%% {'$call',proper_dict,from_list,[[]]},
+%% {'$call',proper_dict,update,
+%% [aa,Fun,3,{'$call',proper_dict,new,[]}]}]}
%% Notice that PropEr will never produce a call like this one:
-%% {'$call',proper_dict,update,[aa,<fun>,{'$call',proper_dict,new,[]}]}
+%% {'$call',proper_dict,update,[aa,Fun,{'$call',proper_dict,new,[]}]}
%% which would raise an exception if we tried to evaluate it.
%% This header is only included so that the strip_types parse transform will be
View
54 src/proper_gen.erl
@@ -20,12 +20,14 @@
%%% @copyright 2010-2011 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas
%%% @version {@version}
%%% @author Manolis Papadakis
-%%% @doc The generator subsystem and generators for basic types are contained
-%%% in this module. You can use the <a href="#index">these </a> functions
-%%% to try out the random instance generation and shrinking subsystems.
+
+%%% @doc Generator subsystem and generators for basic types.
+%%%
+%%% You can use <a href="#index">these</a> functions to try out the random
+%%% instance generation and shrinking subsystems.
%%%
-%%% CAUTION: <a href="#index">These </a> functions should never be used
-%%% inside properties. They are meant for demonstration purposes only.
+%%% 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]).
@@ -52,21 +54,30 @@
%% Types
%%-----------------------------------------------------------------------------
--type instance() :: term().
%% TODO: update imm_instance() when adding more types: be careful when reading
%% anything that returns it
+%% @private_type
-type imm_instance() :: proper_types:raw_type()
| instance()
| {'$used', imm_instance(), imm_instance()}
| {'$to_part', imm_instance()}.
+-type instance() :: term().
+%% A value produced by the random instance generator.
-type error_reason() :: 'arity_limit' | 'cant_generate' | {'typeserver',term()}.
+%% @private_type
-type sized_generator() :: fun((size()) -> imm_instance()).
+%% @private_type
-type nosize_generator() :: fun(() -> imm_instance()).
+%% @private_type
-type generator() :: sized_generator() | nosize_generator().
+%% @private_type
-type reverse_gen() :: fun((instance()) -> imm_instance()).
+%% @private_type
-type combine_fun() :: fun((instance()) -> imm_instance()).
+%% @private_type
-type alt_gens() :: fun(() -> [imm_instance()]).
+%% @private_type
-type fun_seed() :: {non_neg_integer(),non_neg_integer()}.
@@ -163,13 +174,14 @@ generate(Type, TriesLeft, Fallback) ->
{false,false} -> generate(Type, TriesLeft - 1, Fallback)
end.
-%% @doc Equivqlent to `pick(RawType, 10)'.
--spec pick(proper_types:raw_type()) -> {'ok',instance()} | 'error'.
+%% @equiv pick(Type, 10)
+-spec pick(Type::proper_types:raw_type()) -> {'ok',instance()} | 'error'.
pick(RawType) ->
pick(RawType, 10).
-%% @doc Generates a random instance of `RawType', of size `Size'.
--spec pick(proper_types:raw_type(), size()) -> {'ok',instance()} | 'error'.
+%% @doc Generates a random instance of `Type', of size `Size'.
+-spec pick(Type::proper_types:raw_type(), size()) ->
+ {'ok',instance()} | 'error'.
pick(RawType, Size) ->
proper:global_state_init_size(Size),
case clean_instance(safe_generate(RawType)) of
@@ -189,14 +201,14 @@ pick(RawType, Size) ->
error
end.
-%% @doc Equivalent to `sample(RawType, 10, 20)'.
--spec sample(proper_types:raw_type()) -> 'ok'.
+%% @equiv sample(Type, 10, 20)
+-spec sample(Type::proper_types:raw_type()) -> 'ok'.
sample(RawType) ->
sample(RawType, 10, 20).
-%% @doc Generates and prints one random instance of `RawType' for each size
-%% from `StartSize' up to `EndSize'.
--spec sample(proper_types:raw_type(), size(), size()) -> 'ok'.
+%% @doc Generates and prints one random instance of `Type' for each size from
+%% `StartSize' up to `EndSize'.
+-spec sample(Type::proper_types:raw_type(), size(), size()) -> 'ok'.
sample(RawType, StartSize, EndSize) when StartSize =< EndSize ->
Tests = EndSize - StartSize + 1,
Prop = ?FORALL(X, RawType, begin io:format("~p~n",[X]), true end),
@@ -204,15 +216,15 @@ sample(RawType, StartSize, EndSize) when StartSize =< EndSize ->
_ = proper:quickcheck(Prop, Opts),
ok.
-%% @doc Equivalent to `sampleshrink(RawType, 10)'.
--spec sampleshrink(proper_types:raw_type()) -> 'ok'.
+%% @equiv sampleshrink(Type, 10)
+-spec sampleshrink(Type::proper_types:raw_type()) -> 'ok'.
sampleshrink(RawType) ->
sampleshrink(RawType, 10).
-%% @doc Generates a random instance of `RawType', of size `Size', then shrinks
-%% it as far as it goes. The value produced on each step of the shrinking
-%% process is printed on the screen.
--spec sampleshrink(proper_types:raw_type(), size()) -> 'ok'.
+%% @doc Generates a random instance of `Type', of size `Size', then shrinks it
+%% as far as it goes. The value produced on each step of the shrinking process
+%% is printed on the screen.
+-spec sampleshrink(Type::proper_types:raw_type(), size()) -> 'ok'.
sampleshrink(RawType, Size) ->
proper:global_state_init_size(Size),
Type = proper_types:cook_outer(RawType),
View
120 src/proper_symb.erl
@@ -21,19 +21,20 @@
%%% @version {@version}
%%% @author Manolis Papadakis
-%%% @doc This module contains functions used when symbolically generating
-%%% datatypes. When writing properties that involve abstract data types,
-%%% such as dicts or sets, it is usually best to avoid dealing with the ADTs'
-%%% internal representations directly. Working, instead, with a symbolic
-%%% representation of an ADT's construction process (series of API calls)
-%%% has several benefits:
+%%% @doc Symbolic datatypes handling functions.
+%%%
+%%% == Symbolic datatypes ==
+%%% When writing properties that involve abstract data types, such as dicts or
+%%% sets, it is usually best to avoid dealing with the ADTs' internal
+%%% representation directly. Working, instead, with a symbolic representation of
+%%% the ADT's construction process (series of API calls) has several benefits:
%%% <ul>
-%%% <li>Failing testcases are easier to read and understand. Compare:<br/>
-%%% ```{call,sets,from_list,[[1,2,3]]}'''
+%%% <li>Failing testcases are easier to read and understand. Compare:
+%%% ``` {call,sets,from_list,[[1,2,3]]} '''
%%% with:
-%%% ```{set,3,16,16,8,80,48,
-%%% {[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]},
-%%% {{[],[3],[],[],[],[],[2],[],[],[],[],[1],[],[],[],[]}}}'''</li>
+%%% ``` {set,3,16,16,8,80,48,
+%%% {[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]},
+%%% {{[],[3],[],[],[],[],[2],[],[],[],[],[1],[],[],[],[]}}} '''</li>
%%% <li>Failing testcases are easier to shrink.</li>
%%% <li>It is especially useful when testing the datatype itself: Certain
%%% implementation errors may depend on some particular selection and
@@ -43,20 +44,23 @@
%%%
%%% PropEr supports the symbolic representation of datatypes, using the
%%% following syntax:
-%%% <ul>
-%%% <li>`{call,Module,Function,Arguments}': This represents a call to the
-%%% API function `Module:Function' with arguments `Arguments'. Each of
-%%% the arguments may be a symbolic call itself or contain other symbolic
-%%% calls in lists or tuples of arbitrary depth.</li>
-%%% <li>``{'$call',Module,Function,Arguments}'': Identical to the above,
-%%% but gets evaluated automatically before being applied to a property.</li>
-%%% <li>`{var,'{@type var_id()}`}': This contruct serves as a placeholder for
-%%% values that are not known at type construction time. It will be replaced
-%%% by the actual value of the variable during evaluation.</li>
-%%% </ul>
+%%% <dl>
+%%% <dt>`{call,Module,Function,Arguments}'</dt>
+%%% <dd>This represents a call to the API function `Module:Function' with
+%%% arguments `Arguments'. Each of the arguments may be a symbolic call itself
+%%% or contain other symbolic calls in lists or tuples of arbitrary
+%%% depth.</dd>
+%%% <dt id="$call">``{'$call',Module,Function,Arguments}''</dt>
+%%% <dd>Identical to the above, but gets evaluated automatically before being
+%%% applied to a property.</dd>
+%%% <dt id="var">`{var,'{@type var_id()}`}'</dt>
+%%% <dd>This contruct serves as a placeholder for values that are not known at
+%%% type construction time. It will be replaced by the actual value of the
+%%% variable during evaluation.</dd>
+%%% </dl>
%%%
-%%% When including the <code>"proper/include/proper.hrl"</code> header file,
-%%% all <a href="#index">API functions </a> of {@module} are automatically
+%%% When including the PropEr header file, all
+%%% <a href="#index">API functions</a> of this module are automatically
%%% imported, unless `PROPER_NO_IMPORTS' is defined.
%%%
%%% == Auto-ADT ==
@@ -65,21 +69,28 @@
%%% 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
+%%% defining module, which is expected to contain one or more `-spec'ed and
%%% exported functions that can be used to construct instances of the ADT.
%%% Specifically, PropEr will use all functions that return at least one
%%% instance of the ADT. As with recursive native types, the base case is
%%% automatically detected (in the case of ADTs, calls to functions like
%%% `new/0' and `from_list/1' would be considered the base case). The produced
-%%% symbolic calls will be `$call' tuples, which are automatically evaluated,
-%%% thus no call to `eval/1' is required inside the property. Produced instances
-%%% are guaranteed to evaluate successfully. Parametric ADTs are 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').