proper-testing / proper

PropEr: a QuickCheck-inspired property-based testing tool for Erlang

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, Eirini Arvaniti, and Kostis Sagonas. The base PropEr system was written mainly by Manolis Papadakis, and the stateful code testing subsystem by Eirini Arvaniti. Kostis Sagonas has been actively maintaining its code base since 2012.

You can reach PropEr's developers in the following ways:

• on the web: at the project's home page or the project's github page
• by email: take the tool's name (all lowercase), add a @ followed by softlab dot ntua dot gr

We welcome user contributions and feedback (comments, suggestions, feature requests, bug reports, patches, etc.).

Copyright 2010-2022 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. You can either get a tagged version of the tool (look under Tags on github) or you can clone the current code base:

  git clone [email protected]:proper-testing/proper.git

• Compile PropEr: Simply run make if you just want to build PropEr. If you want to do some changes to PropEr or submit some pull request you most likely will want to issue a make test to run its unit tests and a make dialyzer call to also run dialyzer on PropEr's code base. To do the above but also build PropEr's documentation issue a make all call; in that case, you are going to need the syntax_tools application and a recent version of EDoc).

• If you are using Homebrew, you can simply:

  brew install proper

  and continue following the instructions below.

• 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()).

  See also the section common problems below if you want to run PropEr from EUnit.

Where to go from here

To get started on using PropEr, see the tutorials and testing tips provided on PropEr's home page. 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.

Another issue is that EUnit captures standard output, so normally PropEr output is not visible when proper:quickcheck() is invoked from EUnit. You can work around this by passing the option {to_file, user} to proper:quickcheck/2. For example:

?assertEqual(true, proper:quickcheck(your_mod:some_prop(), [{to_file, user}])).

This will make PropEr properties visible also when invoked from EUnit.

Incompatibilities with QuviQ's QuickCheck

PropEr's notation and output format has been kept quite similar to that of QuviQ's QuickCheck in order to ease the reuse of existing testing code written for that tool. However, incompatibilities are to be expected, since we never run or owned a copy of QuviQ's QuickCheck and 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; this is for consistency with other module/2 functions in Erlang/OTP.

All the above are from circa 2010. Most likely, there exist many more incompatibilities between the two tools by now.

proper's Issues

why proper not returning error when can't produce enough satisfies instances?

why proper not returning error when can't produce enough satisfies instances?

I mean in proper:module, proper:check_spec, proper:check_specs...

I have just [] ... as result of (proper:check_specs(example):

Testing example:size/1
.........................................................................................................................................................................................
Error: Couldn't produce an instance that satisfies all strict constraints after 50 tries.

Testing example:is_empty/1
..............................................................................................................................................................
Error: Couldn't produce an instance that satisfies all strict constraints after 50 tries.

Testing example:new/0
........................................................................................................................................................................................................
OK: Passed 200 test(s).

Testing example:safe_pop/1
................................................................................................................................................
Error: Couldn't produce an instance that satisfies all strict constraints after 50 tries.

Testing example:pop/1
........................................................................................................................................................................................................
OK: Passed 200 test(s).

Testing example:push/2
...............................................................................................................................................................................
Error: Couldn't produce an instance that satisfies all strict constraints after 50 tries.

[]

Dialyzer warning: call 'breaks the contract' when combining proper with eunit.

user_opts() type does not contain: {'to_file', 'user'}.
Even though this option is the suggested way to integrate proper with eunit.

Below are two examples:
The call proper:check_spec({'module_name', 'function_name', 0},[{'to_file','user'},...]) breaks the contract (mfa(),user_opts()) -> result()

The call proper:quickcheck({'forall',,fun(() -> any())},[{'to_file','user'},...]) breaks the contract (outer_test(),user_opts()) -> result()

?TRAPEXIT creates separate process, which limits use of ets tables in statem

If initial state of the test creates a digraph and we want to clean it up later on inside of ?TRAPEXIT block, it is impossible due to the fact that TRAPEXIT creates a separate process and digraph doesn't provide [public] option when creating digraph.

initial_state() ->
  io:format("Init: ~p~n", [self()]),
  digraph:new().

prop_digraph() ->
    ?FORALL(Cmds, commands(?MODULE),
            ?TRAPEXIT(begin
                io:format("Tester: ~p~n", [self()]),
                {H, DG, Res} = run_commands(?MODULE, Cmds),
                true = digraph:delete(DG),
                ?WHENFAIL(
                   io:format("History: ~w\nState: ~w\nRes: ~w\n",
                             [H, S, Res]),
                   aggregate(command_names(Cmds), Res =:= ok))
            end)).

Bug updating state for statem post conditions

Unless I'm completely misunderstanding how post conditions are supposed to work, this appears to be a bug in passing the old state to the postcondition function:

https://github.com/manopapad/proper/blob/master/src/proper_statem.erl#L537

Seems like it should really be using State2 from line 534.

edoc warnings

The following warnings are reported when generating proper's edocs (via rebar) using R14B04. I didn't try with older Erlang/OTP versions.

==> proper (doc)
./src/proper_typeserver.erl, function start/0: at line 262: warning: tag @private_type not recognized.
./src/proper_typeserver.erl, function start/0: at line 265: warning: tag @private_type not recognized.
./src/proper_typeserver.erl, function start/0: at line 284: warning: tag @private_type not recognized.
./src/proper_typeserver.erl, function start/0: at line 286: warning: tag @alias not recognized.
./src/proper_typeserver.erl, function start/0: at line 290: warning: tag @alias not recognized.
./src/proper_types.erl, function cook_outer/1: at line 210: warning: tag @alias not recognized.
./src/proper_types.erl, function cook_outer/1: at line 212: warning: tag @private_type not recognized.
./src/proper_types.erl, function cook_outer/1: at line 213: warning: tag @alias not recognized.
./src/proper_types.erl, function cook_outer/1: at line 215: warning: tag @private_type not recognized.
./src/proper_types.erl, function cook_outer/1: at line 216: warning: tag @alias not recognized.
./src/proper_gen.erl, function safe_generate/1: at line 59: warning: tag @private_type not recognized.
./src/proper_gen.erl, function safe_generate/1: at line 68: warning: tag @private_type not recognized.
./src/proper_gen.erl, function safe_generate/1: at line 70: warning: tag @private_type not recognized.
./src/proper_gen.erl, function safe_generate/1: at line 72: warning: tag @private_type not recognized.
./src/proper_gen.erl, function safe_generate/1: at line 74: warning: tag @private_type not recognized.
./src/proper_gen.erl, function safe_generate/1: at line 76: warning: tag @private_type not recognized.
./src/proper_gen.erl, function safe_generate/1: at line 78: warning: tag @private_type not recognized.
./src/proper_gen.erl, function safe_generate/1: at line 80: warning: tag @private_type not recognized.
./src/proper.erl, function grow_size/1: at line 375: warning: tag @alias not recognized.
./src/proper.erl, function grow_size/1: at line 377: warning: tag @alias not recognized.
./src/proper.erl, function grow_size/1: at line 499: warning: tag @alias not recognized.
./src/proper.erl, function grow_size/1: at line 505: warning: tag @private_type not recognized.

R13B03 compilation fails

Hi,

james@perfidy:~/etorrent/deps/proper$ git checkout origin/HEAD
HEAD is now at 00abb4d... Fix formatting in README.md
james@perfidy:~/etorrent/deps/proper$ make clean
./clean_temp.sh
james@perfidy:~/etorrent/deps/proper$ make
./rebar compile
==> proper (compile)
src/proper_fsm.erl:178: type state() undefined
make: *** [compile] Error 1

Attempting to build etorrent, which depends on PropEr, ran into this little snag. Tried monkeypatching but I'm not an Erlangger at heart just yet. Environment is Ubuntu 10.10, Erlang R13B03.

Quickstart guide does not mention rebar (or other build tool) and suggests manual running of all property tests.

PropEr's quick-start instructions in the project README do not:

• detail integrating with rebar or old-style project makefile,
• show running a property test suite as opposed to single property tests in the erlang shell, by hand and
• link to resources that address the above (I note the website's User Guide is the project README and the Tutorials do not clearly address this, either).

Detail integrating with rebar or old-style project makefile

To the first point, I note that rebar's ta-qc branch which provides support for PropEr hasn't seen any action in a year. It seems reasonable to me that PropEr should:

• be integrated into rebar,
• piggy back on eunit (see poolboy_eqc.erl ) or
• provide a utility to run proper tests without relying on an external build tool.

Setting up paths appropriately and finding the property tests to run is somewhat involved but is doable without recourse to rebar. I note that Haskell's QuickCheck supports no discovery of tests, but providing out-of-the-box running for tests placed in a well-known area is increasingly a feature of modern test tools.

Show running a property test suite as opposed to single property tests in the erlang shell, by hand.

The resolution of this sub-problem is highly dependent on the resolution of the above. Most pragmatic to the PropEr project is probably piggy-backing on eunit, but that is annoyingly verbose and of poor work saving utility to subsequent developers.

Link to resources that address the above

An example project--not necessarily complex--would do wonders.

dict/0, set/0, queue/0, gb_tree/0, gb_set/0, array/0 deprecated

On compiling proper under r17, one gets a wall of messages of the form /gigantic/path/lib/proper/src/proper_typeserver.erl:235: Warning: type dict/0 is deprecated and will be removed in OTP 18.0; use use dict:dict/0 or preferably dict:dict/2

I assume you're already aware of this and have accounted for it in r18, but I'm filing this just in case, because I don't see any closed tickets about this.

Behaviour specs aren't used by check_specs

Given the following behaviour

-module(bar).

-callback behaviour_spec(integer()) -> integer().

and module

-module(foo).

-behaviour(bar).

-export([normal_spec/1, behaviour_spec/1]).

-spec normal_spec(integer()) -> integer().
normal_spec(A) ->
    A + 1.

behaviour_spec(A) ->
    [A].

Dialyzer gives

~/src/pt $ dialyzer -r .
  Checking whether the PLT /Users/puzza/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis...
foo.erl:11: The inferred return type of behaviour_spec/1 ([any(),...]) has nothing in common with integer(), which is the expected return type for the callback of bar behaviour
 done in 0m5.04s
done (warnings were emitted)

But PropEr gives:

~/src/pt $ erl -pa ../proper/ebin
Erlang R16B02 (erts-5.10.3) [source] [64-bit] [smp:4:4] [async-threads:10] [kernel-poll:false]

Eshell V5.10.3  (abort with ^G)
1> proper:check_specs(foo).
Testing foo:normal_spec/1
....................................................................................................
OK: Passed 100 test(s).

[]

Crashing on stateful tests

Hi,

While running PropEr agains a gen_server (like in your tutorial), the test crashed after stopping the server. The problem was that the stop function in the server didn't return the 4 elements tuple {stop, Reason, Reply, State}, it did the 3 elements one {stop, Reason, State}.

Is this the intended behaviour? If so, why?

proper:quickcheck/1 returns missing_type

Test case is called from unit using proper:quickcheck/1.
Source was compiled with debug_info.
Type dht_query is defined inside a module.

{error,
                  {typeserver,
                      {missing_type,etorrent_dht_net,{type,dht_query,0}}}}

Eunit helpers

We want to run PropEr from within eunit, but there are 2 problems:

1. eunit captures stdout
2. proper:quickcheck/2 does not return eunit generator :)

I am overcoming these problems with these eunit helpers:
https://github.com/Motiejus/z_string/blob/master/src/proper_utils.erl

Example:

z_string_test_() ->
    [
        proper_utils:qc_(test1()),
        proper_utils:qc_(test2())
    ].

test1() -> ?FORALL(I, pos_integer(), 0 < I).
test2() -> ?FORALL( ... ).

Might be useful for others?

If yes, please let me know if "proper_eunit" module name is fine, I will submit a pull request.

Combine efforts with triq

Excellent lib! Could we combine efforts with triq?

Consider using a more permissive license

Problem compiling latest code from master on R13B04

./rebar compile
==> proper (compile)
src/proper_statem.erl:191: function min/2 undefined
make: *** [compile] Error 1

Thx.

Rebar compile fails when trying to install chicago boss

==> proper (compile)
INFO: sh info:
cwd: "/home/erlangdeveloper/ChicagoBoss-0.8.14/deps/proper"
cmd: make include/compile_flags.hrl
sh: 1: exec: make: not found
ERROR: Command [compile] failed!

I dont see compile_flags.hrl under include folder. Please advise if i am missing any steps.

Consider making PropEr a community managed project.

At the time of this writing PropEr has two open pull requests and 12 open issues, many of those having attached code and ready contributors.

It would seem, from comments left in other issues, that the original authors are short on time. Please consider creating a GitHub Organization for proper and adding interested parties as managers. I am interested.

PropEr is a well-crafted tool. It should not rot.

make doc filed at 17.0

Hi,

please find full log here http://paste.opensuse.org/14131907

It seems to be related to OTP-11787

run_parallel_commands doesn't handle postcondition result the same way run_commands does

run_commands handles exceptions by wrapping them into a postcondition result, while run_parallel_commands (through check/6) only checks for true and false.

Compile Always Happens

doing ./rebar compile in proper even if proper has already been compiled causes proper to compile again.

This is extremely annoying when building projects that have proper as a rebar dep.

Tag it

Hi,

would it be possible to tag one of the more recent versions of PropEr?

PropEr 1.0 is too old for R15B (does not clean stack traces properly), and it's really nice to have a tag in rebar.config, instead of "HEAD" or {branch, "master"}.

Thanks!

Could u add support for the module() type?

Usage of GPL v3

Must I licence my test code in GPL v3 as well? And if my test code uses my production code, must I licence that in GPL v3 as well?

next_state is evaluated before checking postcondition in statem

The expected (to me at least) flow in the execution phase of statem would be:

(1) check precondition
(2) run command
(3) check postcondition
(4) update next_state

However, next_state is evaluated before checking the postcondition, which basically means the next_state cannot be certain that this update is legit.

The statem code uses the very same state value in both the call to postcondition and to next_state (as it should) => (3) and (4) can be reordered without affecting any existing proper clients.

But changing them so that (4) is not evaluated if (3) is false make next_state not have to check the postcondition as well.

Internal error: An error occured while shrinking.

Internal error: An error occured while shrinking.
Please notify the maintainers about this error.

When this occurs, what should I extract from my scenario in order to help you with the issue?

Thanks!

Compiling under R13B03

Hi guys

I am using R13B03 since it is the version my cusomter uses. However when running make all I get this error using the following rebar.config. Any help would be nice. :)

./rebar compile
ERROR: Failed to load /opt/local/erlang/lib/proper/rebar.config: {error,
{8,
erl_parse,
"bad term"}}
make: *** [compile] Error 1

rebar.config
% WARNING: Our version of rebar doesn't automatically report warnings, nor does
% it add erl_opts to eunit_compile_opts.

% WARNING: To compile on versions of Erlang/OTP older than R13B4, add
% {d,'NO_TYPES'} to erl_opts.

{erl_first_files, ["strip_types.erl"]}.
{erl_opts, [{d,NO_TYPES},debug_info, report_warnings, {warn_format,1}, warn_export_vars,
warn_obsolete_guard, warn_unused_import, warn_missing_spec,
warn_untyped_record]}.
{edoc_opts, [{dialyzer_specs,all}, {report_missing_type,true},
{report_type_mismatch,true}, {pretty_print,erl_pp},
{preprocess,true}]}.
{dialyzer_opts, [{warnings,[unmatched_returns]}]}.
{clean_post_script, "./clean_doc.sh"}.

Did I not follow the instructions correctly?

proper.app.src missing proper_gen

The modules attribute in propoer.app.src does not contain proper_gen

Native erlang:timestamp() type triggers error under Erlang/OTP 17.3

The following has been compiled and run under both R16B03-1 and 17.3.

-module(example).

-include_lib("proper/include/proper.hrl").
-include_lib("eunit/include/eunit.hrl").

native_test() ->
    proper:quickcheck(
      ?FORALL(_Timestamp, erlang:timestamp(), begin true end)).

%% Not sure why, by the native timestamp doesn't work in 17.3+.
-type timestamp() :: {MegaSecs :: non_neg_integer(),
                      Secs :: non_neg_integer(),
                      MicroSecs :: non_neg_integer()}.

internal_test() ->
    proper:quickcheck(
      ?FORALL(_Timestamp, timestamp(), begin true end)).

In the case of native_test, then the following error will be raised:

=ERROR REPORT==== 3-Nov-2014::15:23:08 ===
** Generic server <0.47.0> terminating 
** Last message in was {translate_type,{example,"erlang:timestamp()"}}
** When Server state == {state,{dict,0,16,16,8,80,48,
                                     {[],[],[],[],[],[],[],[],[],[],[],[],[],
                                      [],[],[]},
                                     {{[],[],[],[],[],[],[],[],[],[],[],[],[],
                                       [],[],[]}}},
                               {dict,0,16,16,8,80,48,
                                     {[],[],[],[],[],[],[],[],[],[],[],[],[],
                                      [],[],[]},
                                     {{[],[],[],[],[],[],[],[],[],[],[],[],[],
                                       [],[],[]}}},
                               {dict,0,16,16,8,80,48,
                                     {[],[],[],[],[],[],[],[],[],[],[],[],[],
                                      [],[],[]},
                                     {{[],[],[],[],[],[],[],[],[],[],[],[],[],
                                       [],[],[]}}},
                               {dict,0,16,16,8,80,48,
                                     {[],[],[],[],[],[],[],[],[],[],[],[],[],
                                      [],[],[]},
                                     {{[],[],[],[],[],[],[],[],[],[],[],[],[],
                                       [],[],[]}}}}
** Reason for termination == 
** {function_clause,
       [{proper_typeserver,'-update_vars/3-lc$^1/1-1-',
            [any],
            [{file,"src/proper_typeserver.erl"},{line,1079}]},
        {proper_typeserver,update_vars,3,
            [{file,"src/proper_typeserver.erl"},{line,1079}]},
        {proper_typeserver,'-unbound_to_any/2-lc$^0/1-0-',2,
            [{file,"src/proper_typeserver.erl"},{line,821}]},
        {proper_typeserver,unbound_to_any,2,
            [{file,"src/proper_typeserver.erl"},{line,821}]},
        {dict,map_bucket,2,[{file,"dict.erl"},{line,453}]},
        {dict,map_bucket,2,[{file,"dict.erl"},{line,453}]},
        {dict,map_bkt_list,2,[{file,"dict.erl"},{line,449}]},
        {dict,map_seg_list,2,[{file,"dict.erl"},{line,444}]}]}
undefined
*unexpected termination of test process*
::{function_clause,
      [{proper_typeserver,'-update_vars/3-lc$^1/1-1-',
           [any],
           [{file,"src/proper_typeserver.erl"},{line,1079}]},
       {proper_typeserver,update_vars,3,
           [{file,"src/proper_typeserver.erl"},{line,1079}]},
       {proper_typeserver,'-unbound_to_any/2-lc$^0/1-0-',2,
           [{file,"src/proper_typeserver.erl"},{line,821}]},
       {proper_typeserver,unbound_to_any,2,
           [{file,"src/proper_typeserver.erl"},{line,821}]},
       {dict,map_bucket,2,[{file,[...]},{line,...}]},
       {dict,map_bucket,2,[{file,...},{...}]},
       {dict,map_bkt_list,2,[{...}|...]},
       {dict,map_seg_list,2,[...]}]}

Pretty-printing of shrinked testcase

Is there any reason to not represent things like

[{init,{state,undefined,{array,0,10,empty,10},208740,large,last}},{set,{var,1},{call,ecirca,new,[208740,last,large]}},{set,{var,4},{call,ecirca,set,[{call,erlang,element,[2,{var,1}]},158910,256964645335393280]}},{set,{var,6},{call,ecirca,slice,[{call,erlang,element,[2,{var,1}]},207505,131476]}}]

as

A = ecirca:new(208740,last,large),
B = ecirca:set(erlang:element(2, A), 158910, 256964645335393280),
C = ecirca:slice(erlang:element(2, A), 207505,131476)

?
And, of course, thanks for an awesome job :)

Provide a wiki to allow community documentation PropEr.

I note that the Github wiki is disabled and that the documentation in the project tree is largely mirrored on the project website. I suggest enabling the Github wiki, or similar:

• the current documentation is inadequate as a practical introduction to PropEr,
• the current documentation reads less as a manual and more as a defense and introduction to property testing (I am especially referring to the Introduction of the README and the 'Tutorial' section of the website) and
• allowing community involvement in documenting a open tool benefits everyone.

Compare PropEr's documentation and website to, say, Cucumber. Short, to the point README which links immediately to the project documentation that provides significant material (even if it's in need of editing and organization). Compare, as well, to the node README etc.

I do concede that Haskell QuickCheck has little more than the official API documentation (though third-party materials abound, especially Real World Haskell), but no one said Haskell has great documentation. :)

problems with includes whilst launching PropEr from eunit

Originally in mailing list:
http://groups.google.com/group/erlang-programming/browse_thread/thread/efd33f75702bb5e8

I have problems running PropEr:check_spec/1 from Eunit.
With this line in module file:
-include("bp_app/include/log_utils.hrl").
PropEr stops working. After removing it, PropEr starts working properly.

Error message I get from PropEr:

motiejus:~/mll/gateway_app$ make test_gateway_specs_tests
ERL_FLAGS="-sname eunit -config ../bp_app/config/default.config
+P1000000 -env ERL_MAX_ETS_TABLES 20000" ../rebar verbose=2
skip_deps=true suite=gateway_specs_tests eunit
==> gateway_app (eunit)
Compiled tests/gateway_specs_tests.erl
Compiled tests/gateway_app_tests.erl
======================== EUnit ========================
gateway_specs_tests: yadda_test (module 'gateway_specs_tests')...
=INFO REPORT==== 27-Jun-2011::17:03:39 ===
   pid: <0.475.0>
   source: "tests/gateway_specs_tests.erl:29"
   message: "checkspec says"
   error: {typeserver,
              {cant_load_code,gateway_helpers,
                  {cant_find_object_file,
                      {cant_compile_source_file,

[{"/home/motiejus/code/mll/gateway_app/.eunit/gateway_helpers.erl",
                            [{16,epp,
                              {include,file,
                                  "bp_app/include/log_utils.hrl"}}]}]}}}}
[0.029 s] ok
 Test passed.

I suspect PropEr recompiles those modules and does not add include paths
properly.

Relevant Code:

gateway_helpers.erl

-module(gateway_helpers).
-include("bp_app/include/log_utils.hrl").
-export([demo/1]).
-spec demo(integer()) -> integer().
demo(Item) ->
   case Item of
       1 -> undefined;
       R when is_integer(R) ->
           Item
   end.

gateway_specs_tests.erl

-module(gateway_specs_tests).
-include_lib("proper/include/proper.hrl").
-include_lib("eunit/include/eunit.hrl").
-include("bp_app/include/log_utils.hrl").

yadda_test() ->
   ?info("checkspec says", [proper:check_spec({gateway_helpers, demo, 1})]).

Relevant tree

bp_app
├── include
│   ├── log_utils.hrl
gateway_app
├── include
│   ├── consts.hrl
│   └── types.hrl
├── src
│   └── gateway_helpers.erl
└── tests
   └── gateway_specs_tests.erl

Versions:
Erlang R14A (from Squeeze apt)
PropEr v1.0-1-g5fe56e9

dialyzer called in default make target

in my opinion standard behaviour of calling 'make' is to just building/compile project, calling here dialyze task, breaking it.

any test, dialyze, etc.. targets could not be part of default build in my opinion.

we could always call make test in CI, but defualt build could be just compile and nothing else.

@kostis what do you thinking about remove dialyze from default target?

The use of ?IMPLIES cuts down on test cases without replacement.

I have a BSON encoder/decoder that I've tested with PropEr, specifically by creating a bunch of bson:document()s and asserting that bson:decode/1 composed with bson:encode/1 is the identity function. See here.

The problem is this: not all bson:documents()s generated purely from type information are valid. I use ?IMPLIES coupled with bson_validate:valid/1 to remove invalid documents, but this chops down the total number of test cases that get run, by about half, in my experience.

How can I:

• create documents from type information with constraints without heavy duplication of constraint code or
• ensure that a fixed number of test cases are generated, even if some are necessarily discarded.

I note that mm.erl composes smaller functions to generate its test cases, but duplicating this approach in my library would make for relatively heavyweight tests and duplicate contextual information in my library, which I'd like to avoid if possible.

Cannot fine-tune the behaviour of the type system integration component

I noticed these 2 compiler warnings. Not sure if this is intentional or not.

src/proper_types.erl:213: Warning: missing specification for function from_binary/1
src/proper_types.erl:310: Warning: missing specification for function unwrap/1

$ erl --version
Erlang R14B01 (erts-5.8.2) [source] [64-bit] [smp:2:2] [rq:2] [async-threads:0] [hipe] [kernel-poll:false]

Eshell V5.8.2 (abort with ^G)
1>

resize(...) incompatibility with eqc

Support for recursive generators. I'm aware this is a known issue - documenting for tracking purposes.

The property "gmt_eqc_gen_eqc_tests:prop_ubf_gen_any/0" triggers an infinite spin loop.

gmt_eqc: eunit_module...Testing gmt_eqc_gen_eqc_tests:prop_ubf_gen_any/0
^Cmake: *** [eunit] Interrupt

How to repeat:

$ wget -O - http://android.git.kernel.org/repo > ~/bin/repo
$ chmod a+x ~/bin/repo
$ mkdir workdir
$ cd workdir 
$ yes | repo init -q -u git://github.com/hibari/manifests.git -m hibari-default.xml 
$ repo sync -q
$ cd hibari/hibari
$ make
$ make test

I have added proper to my ~/.erlang file as described here https://github.com/norton/erlang-starter-kit

thanks

No OTP app file

Without an OTP application file, it is awkward to include/install proper as a dependency using tools such as rebar and/or epm.

check_spec() + maybe_improper_list() => failure

The following fail on current master.

-module(x).
-export([n/0]).
-export([f/2]).
-export_type([t/0]).
-record(x,{a=[]::maybe_improper_list()}).
-opaque t()::#x{}.
-spec n() -> t().
n() -> #x{}.
-spec f(binary(),t()) -> {boolean(),t()}.
f(B,#x{a=A}=X) -> {true,X#x{a=list_to_binary([A|B])}}.

-include_lib("eunit/include/eunit.hrl").

proper_spec_test_() ->
    application:ensure_all_started(proper),
    {inparallel,
     [?_assertEqual({Function,Arity,true},{Function,Arity,proper:check_spec({?MODULE,Function,Arity})})
      || {Function,Arity} <- module_info(exports),
         lists:member(Function,[n,f])
     ]}.

However, it will succeed if I do the following (less optimal) change:

f(B,#x{a=A}=X) -> {true,X#x{a=[list_to_binary(A++[B])]}}.

after pull it doesn't compile

==> proper (compile)
include/proper_internal.hrl:26: can't find include file "compile_flags.hrl"

Version bump

Maybe it's time for the release of a new version? What about '1.1'?

Increasing max_size significantly degrades performance.

Here's a simple contrived example:

-module(perf_ex).                                                                  
-compile(export_all).                                                              
-include_lib("proper/include/proper.hrl").                                         

-record(msg, {                                                                     
  a = 0 :: 0..16#ffffffff,                                                         
  b = 0 :: 0..16#f                                                                 
}).                                                                                
-type(msg() :: #msg{}).                                                            

-spec encode(msg()) -> binary().                                                   
encode(#msg{a = A, b = B}) -> <<A:32, B:4>>.                                       

-spec decode(binary()) -> msg().                                                   
decode(<<A:32, B:4>>) -> #msg{a=A, b=B}.                                           

prop_identity() -> ?FORALL(Msg, msg(), Msg =:= decode(encode(Msg))).               

And the results:

1> timer:tc(fun() -> proper:quickcheck(perf_ex:prop_identity(), [5, {max_size, 42}]) end).
.....                                                                              
OK: Passed 5 test(s).                                                              
{8170,true}                                                                        

2> timer:tc(fun() -> proper:quickcheck(perf_ex:prop_identity(), [5, {max_size, 16#ffffffff}]) end).
.....                                                                           
OK: Passed 5 test(s).                                                              
{658751072,true}                                                                   

I haven't been able to determine what's causing the slowdown, but it's significant. Any suggestions?

error buildig under windows without make.

patch for rebar.config:

- {pre_hooks, [{compile, "escript write_compile_flags"}]}.

+ {pre_hooks, [{"(linux|bsd|darwin|solaris)", compile, "make include/compile_flags.hrl"},{"win32", compile, "escript write_compile_flags include/compile_flags.hrl"}]}.

integer generator can't generate very large integers

Because it uses floats, it seems.

1> proper_gen:integer_gen(1, -(1 bsl 2000), 1 bsl 2000).
** exception error: an error occurred when evaluating an arithmetic expression
     in function  random:uniform/1 (random.erl, line 112)
     in call from proper_arith:rand_int/2 (src/proper_arith.erl, line 242)

where:

-spec rand_int(integer(), integer()) -> integer().
rand_int(Low, High) when is_integer(Low), is_integer(High), Low =< High ->
    Low + random:uniform(High - Low + 1) - 1.

Do you have any plans to implement eqc_statem?

The state machine model support in the commercial product is quite compelling. I've recently started working on libtest, which aims support verifying message passing between processes and/or OTP behaviours and possibly doing some simple instrumentation to ease the wiring required to set up such tests. A model based on eqc_statem (both for sequential and parallel testing) makes a lot of sense for this, but ultimately I'd like to be integrated with PropEr so it's done "the quickcheck way" and there's no point in doing this if you're already implementing eqc_statem.

Please do let me know what plans you have (if any) and if I end up doing this myself I'll keep you informed to ensure that compatibility with PropEr is easy.

Execution time varies?

I am using the repo from tag v1.1 and have noticed that some runs of the test https://github.com/CloudI/CloudI/blob/develop/src/lib/cloudi_service_quorum/test_ct/cloudi_service_quorum_SUITE.erl exceed the timeout (30 minutes with numtests == 1) when ran virtualized in an automated build (at https://travis-ci.org/CloudI/CloudI/). I was wondering if any of the proper source code would be creating potentially large variation in execution time (similar to dialyzer's -Wrace_conditions possibly in this different context due to the PropEr analysis)?

Proposal: tags

Hi,

When I am using "master", I am getting errors like this one:

==> proper (compile)
DEBUG: Matched required ERTS version: 5.9.2 -> .*
DEBUG: Matched required OTP release: R15B02 -> R13B03|R13B04|R14|R15
DEBUG: erl_opts [debug_info,debug_info,report_warnings,
                 {warn_format,1},
                 warn_export_vars,warn_obsolete_guard,warn_unused_import,
                 warn_missing_spec,warn_untyped_record]
INFO:  Skipped src/strip_types.erl
include/proper_internal.hrl:26: can't find include file "compile_flags.hrl"

It is a good idea to mark stable revisions with tags. The issue is that there is only one tag for this repository and it is too old. My proposal is to create tags more regularly.

Can't compile HEAD on R13B03

Running make NOTYPES=1 fails with the following:

t4@zeph:proper $ make NOTYPES=1 | tee build.output
erlc -W2 +debug_info -I include -pa util +{parse_transform,strip_types} -o ebin src/proper.erl
src/proper.erl:51: type test() undefined
src/proper.erl:52: type numtests_clause() undefined
src/proper.erl:53: type fails_clause() undefined
src/proper.erl:54: type on_output_clause() undefined
src/proper.erl:56: type forall_clause() undefined
src/proper.erl:57: type implies_clause() undefined
src/proper.erl:58: type sample_clause() undefined
src/proper.erl:59: type whenfail_clause() undefined
src/proper.erl:60: type trapexit_clause() undefined
src/proper.erl:61: type timeout_clause() undefined
src/proper.erl:64: type apply_clause() undefined
src/proper.erl:125: type pass_reason() undefined
src/proper.erl:126: type counterexample() undefined
src/proper.erl:127: type single_run_error_reason() undefined
src/proper.erl:130: type exc_kind() undefined
src/proper.erl:130: type exc_reason() undefined
src/proper.erl:130: type stacktrace() undefined
src/proper.erl:139: type error_reason() undefined
src/proper.erl:144: type counterexample() undefined
src/proper.erl:146: type counterexample() undefined
src/proper.erl:147: type counterexample() undefined
src/proper.erl:148: type counterexample() undefined
src/proper.erl:73: Warning: type implies_clause() is unused
src/proper.erl:76: Warning: type trapexit_clause() is unused
src/proper.erl:77: Warning: type timeout_clause() is unused
src/proper.erl:80: Warning: type apply_clause() is unused
src/proper.erl:128: Warning: type pass_reason() is unused
src/proper.erl:131: Warning: type exc_kind() is unused
src/proper.erl:132: Warning: type exc_reason() is unused
src/proper.erl:133: Warning: type stacktrace() is unused
src/proper.erl:134: Warning: type single_run_error_reason() is unused
src/proper.erl:140: Warning: type error_reason() is unused

Looks like a missing header/include. Running on OSX Snow Leopard. Let me know if you need any further details.

Integration with McErlang

QuickCheck/ProTest appears to have fairly good integration with the Erlang Model Checking Library produced by the same group. This uses a state machine model for verification. I plan on providing some level of API support for this in libtest (probably in the form of a hamcrest-erlang based DSL for defining monitors).

Have you looked at the commercial QuickCheck integration with this product and do/would you have any plans to integrate with PropEr in the future? There is some good coverage of the tool here.

PS: I'm a willing contributor if needed, but I would want clear guidance on how you wanted the API to look and any particular implementation details that matter to PropEr.

Undefined Values in records

I am having a problem where proper seems to be createing records with undefined values despite the fact that the spec for the record does not permit it

-type name() :: {name, binary()}.
-record(test_rec,
        {
          name ::name()
        }).
-type test_rec() :: #test_rec{}.

prop_name() ->
    ?FORALL(Rec,
            test_rec(),
            Rec#test_rec.name /= undefined
            ).

When I run the above property I get this

!
Failed: After 1 test(s).
{test_rec,undefined}

Shrinking (0 time(s))
{test_rec,undefined}

CEAN package broken

When I try to install proper via CEAN, it says:

cean:install(proper).
failed to get dependencies: {[112,114,111,112,101,114],depends,no_pub_file}
! proper Error: {badmatch,{error,no_pub_file}}
error

System:

• CEAN 2.0
• Erlang R15B03
• Homebrew 0.9.4
• Xcode 4.6.2
• Mac OS X 10.8.3 x64

proposal: utf8 generator

For a project I am working on I created a PropEr utf8 generator:

https://github.com/Motiejus/z_string/blob/master/test/z_string_test.erl#L79

I guess it might be useful for others if they need UTF8 binaries for some reason. Would you consider including it to PropEr? If yes, I can make a proper pull request. If not, I will not bother.