A collection of goodies for the property-based testing framework PropEr.
Both PropEr and QuickCheck offer their users the ability to "test stateful systems whose internal state and side-effects are specified via an abstract state machine". They do so via so-called statem behaviours. Whilst the basic idea is the same in both frameworks, QuickCheck's statem offers a few extra functionalities that are currently not available in PropEr. Among other things, the QuickCheck statem behaviour allows users to define an abstract state machines in a more convenient, organized format than PropEr.
The proper_contrib_statem.hrl header file contains some trivial
boilerplate that allows PropEr users to define their abstract state
machines with a syntax which is more similar to the QuickCheck one.
Specifically, the boilerplate allows the definition of a few
optional callback functions in a proper_statem callback module:
[COMMAND]_args/1[COMMAND]_next/3[COMMAND]_post/3[COMMAND]_pre/1[COMMAND]_pre/2
Those calls will replace the following ones:
next_state/3postcondition/3precondition/2
This makes the definition of abstract state machines a lot simpler, allowing all the logic (i.e. preconditions, postconditions, etc.) related to the same COMMAND to be grouped together, rather than be scattered across the entire statem callback module.
The boilerplate also makes the command/1 function not needed
anymore. The list of commands, in fact, are dynamically inferred by
convention (i.e. by looking at exported functions of arity 1 within
the same module whose name ends with _args). An optional weight/1
callback function allows users to specify a different frequency for
each command.
To get started, include the proper_contrib repo as a test dependency
for your project. For example, if you are using the rebar3 build
tool, you can add the following to your rebar.config:
{profiles, [{test, {deps, [{proper_contrib, "0.1.0"}]}}]}.Then, include the proper_contrib_statem.hrl file in your
proper_statem callback module:
-module(prop_sample).
-behaviour(proper_statem).
-include_lib("proper/include/proper.hrl").
-include_lib("stdlib/include/assert.hrl").
-include("proper_contrib_statem.hrl"). %% Yes, this is all!
prop_sample() ->
?FORALL(Cmds, proper_statem:commands(?MODULE),
begin
{_History, _S, Result} = proper_statem:run_commands(?MODULE, Cmds),
Result =:= ok
end).
And you are ready to go. The header will define the proper_statem
callback functions for you and will proxy calls to the new callback
functions whenever appropriate.
A traditional proper_statem may look like the following (extracted
from the PropEr official
documentation):
[...]
command(_S) ->
oneof([{call,?MODULE,create_account,[name()]},
{call,?MODULE,delete_account,[password()]}]).
[...]
next_state(S, Res, {call,_,create_account,[_Name]}) ->
S#state{users = [Res|S#state.users]};
next_state(S, _Res, {call,_,delete_account,[Password]}) ->
S#state{users = lists:delete(Password, S#state.users)}.
[...]
precondition(_, _) -> true.
[...]
postcondition(S, {call,_,create_account,[_Name]}, Result) ->
not lists:member(Result, S#state.users);
postcondition(_S, {call,_,delete_account,[_Password]}, Result) ->
Result =:= account_deleted;
[...]Thanks to the proper_contrib_statem.hrl boilerplate, the same
callback module will look like:
[...]
create_account_pre(_S, _Args) ->
true.
create_account_args(_S) ->
[name()].
create_account_next(S, Res, [_Name]) ->
S#state{users = [Res|S#state.users]}.
create_account_post(_S, [_Name], Res) ->
not lists:member(Res, S#state.users).
[...]
delete_account_pre(_S, _Args) ->
true.
delete_account_args(_S) ->
[password()].
delete_account_next(S, Res, [Password]) ->
S#state{users = lists:delete(Password, S#state.users)}.
delete_account_post(_S, [Password], Res) ->
Result =:= account_deleted.- Roberto Aloi
- Juan Facorro