command()
), each
of which binds a symbolic variable to the result of a symbolic function call (except,
possibly, for a first command which initializes the state, see below).
For example,
{set,{var,1},{call,erlang,whereis,[a]}}is a command to set variable 1 to the result of calling erlang:whereis(a). When a test case is run, then symbolic variables (
var()
) are replaced
by the values they were set to, and symbolic calls (call()
) are
performed. In addition, the post-condition of each command is checked. Running
a list of commands generates a result which indicates whether
any post-condition failed, or any command raised an exception, or whether all
commands and checks completed successfully.
It is very important to keep in mind the difference between symbolic calls and variables, which are used during test case generation, and the values they represent, which are computed during test execution. We refer to the latter as dynamic values. The reason we use symbolic representations (rather than just working with their dynamic values) is to enable us to display, save, analyze, and above all simplify test cases before they are run.
[{var,1},{var,2},{var,3}]if the first three commands all spawned processes. During test execution the corresponding dynamic state is computed--in this case a list of three pids returned by the first three commands in the test case. Dynamic states always have the same structure as the corresponding symbolic states--the difference is just that symbolic variables and calls are replaced by their values.
Symbolic states are used to generate symbolic commands, or to decide whether a given symbolic command can be included in a test case. Dynamic states are used to check postconditions.
It is not usually necessary to track all relevant state information in the test case state--there is no need to include more information in the state than is necessary to generate and execute the command sequences we are interested in.
symbolic_state()
.
Returns the state in which each test case starts (unless a different initial state is supplied explicitly). This symbolic state is evaluated to construct the initial dynamic state before each test case is executed.
symbolic_state()
,C::call()
) :: bool()
Returns true if the symbolic call C can be performed in the state S. Preconditions are used to decide whether or not to include candidate commands in test cases, which is why only the symbolic state information is available when preconditions are checked.
symbolic_state()
) :: gen(call()
Generates an appropriate symbolic function call to appear next in a test case, if the symbolic state is S. Test sequences are generated by using command(S) repeatedly. However, generated calls are only included in test sequences if their precondition is also true.
dynamic_state()
,C::call()
,R::term()) :: bool()
Checks the postcondition of symbolic call C, executed in dynamic state S, with result R. The arguments of the symbolic call are the actual values passed, not any symbolic expressions from which they were computed. Thus when a postcondition is checked, we know the function called, the values it was passed, the value it returned, and the state in which it was called.
Of course, postconditions are checked during test execution, not test generation.
symbolic_state()
,R::var()
,C::call()
) :: symbolic_state()
This is the state transition function of the abstract state machine, and it is used during both test generation and test execution. The type above refers to calls during test generation.
In this case, it computes the symbolic state after symbolic call C, performed in symbolic state S, with result R. Because it is applied to symbolic states and symbolic calls, the result of the call must also be symbolic-- in fact, R is the symbolic variable which will be set to the result of the call. R can then be included in the next state if necessary. For example, if the state were a list of pids, and C spawned a new process, then the variable R could be added to the state to refer to the pid of the process just spawned. Symbolic function calls can also be included in the next state, to construct parts whose values will only be known during test execution.
The same function is used to compute the next dynamic state during test execution. In this case S is the previous dynamic state, C is a symbolic call in which the arguments are the actual values passed (not symbolic argument expressions), and R is the actual value returned--in other words, all the symbolic inputs are replaced by their values. A correctly written next_state function does not inspect symbolic inputs--it just includes them as symbolic parts of the result. Thus the same code can construct a dynamic state of the same shape, given actual values instead of symbolic ones. The only difficulty is that next_state may itself introduce symbolic function calls into its result, which would then be a kind of mixture of a symbolic and dynamic state. To ensure that the state remains dynamic during test execution, any such symbolic calls are performed, and replaced by their values, before test execution continues.
prop_statem_correct() -> ?FORALL(Cmds,commands(client), begin {H,S,Result} = run_commands(client,Cmds), Result==ok end).However, in any particular case we may wish to add a little to this basic form, for example to collect statistics, to clean up after test execution, or to print more information in the event of failure. It is to allow this flexibility that the properties to test are placed in the client module, rather than in this one.
call() = {call, atom(), atom(), list(expr())}
A symbolic function call: {call,M,F,Args} represents a call of function F in module M, with arguments Args.
command() = {set, var(), call()} | {init, symbolic_state()}
A symbolic
command, which when run either
performs a call and binds the result to a variable, or initialises
the state of the test case. (The latter appears only when commands/2
in used to generate a command sequence starting in a state other than
initial_state()).
abstract datatype: dynamic_state()
The type used by the client module to represent
the state of a test case during test execution. It is the same as
symbolic_state()
, except that symbolic variables and calls
are replaced by their values.
exit() = {'EXIT', term()}
The type of a caught exception.
expr() = term()
A symbolic expression, which is evaluated by
replacing any symbolic variables (var()
) or function calls
(call()
) in the term by their values.
history() = list({dynamic_state(), term()})
The history of a test execution, with one element for each command that was executed without an exception, containing the state before the command and the value it returned.
reason() = ok | initialization | {precondition, bool()} | {postcondition, bool() | exit()} | {exception, exit()}
The reason execution of a command sequence terminated.
All commands completed normally, and all postconditions were true.
There was an exception when computing the initial state--that is, converting the
result of initial_state() to a dynamic_state()
.
A precondition was false, or raised an exception, during test execution.
Since preconditions are checked when tests are generated, this should not normally
happen. It is possible
when using eqc:check/2
to rerun a saved test, after modifying the code,
or if one of the functions initial_state/0, next_state/3, or
precondition/2 behaves differently at generation time and test execution
time. For example, a pattern match on a symbolic variable ({var,N}) will
behave differently during test case generation and execution--so any such pattern
matching is a warning sign.
A postcondition was false or raised an exception.
One of the commands in the sequence raised an exception. In this case the
history()
contains all previous commands, and the final state is
the state just before the faulty command was executed.
abstract datatype: symbolic_state()
The type used by the client module to represent the state of a test case during test case generation.
var() = {var, integer()}
A symbolic variable, which is replaced
during test execution by the value bound by the corresponding command()
.
command_names/1 | Returns a list of the command names used in Cmds. |
commands/1 | Generates a list of commands, using the abstract state machine defined in module Mod. |
commands/2 | Behaves like commands/1 , but generates a list of
commands starting in state S. |
more_commands/2 | Increases the expected length of command sequences generated within Gen by a factor N. |
postconditions/3 | Given the values returned by a list of commands, checks that all pre- and postconditions are satisfied. |
run_commands/2 | Runs a list of commands specified by the abstract state machine in client module Mod. |
run_commands/3 | Behaves like run_commands/2 , but also takes an environment
containing values for additional variables that may be referred
to in test cases. |
zip/2 | Zips two lists together, but accepts lists of different lengths, stopping when the shorter list stops. |
command_names(Cmds::list(command())) -> list({atom(), atom(), integer()})
Returns a list of the command names used in Cmds. This function can be used in properties to measure the frequency with which each command actually occurs in the generated test cases, as follows:
?FORALL(Cmds,commands(...), begin {H,S,Res} = run_commands(...,Cmds), aggregate(command_names(Cmds), Res==ok) end)
Generates a list of commands, using the abstract state machine defined in module Mod. The commands in the sequence are generated by Mod:command/1, starting in the state Mod:initial_state(), and tracking state changes using Mod:next_state/3. Commands are only included in the sequence if their precondition (given by Mod:precondition/2) is satisfied. Sequences are shrunk by discarding commands in such a way that preconditions always hold, and all variables are set before they are used.
commands(Mod::atom(), S::symbolic_state()) -> gen(list(command()))
Behaves like commands/1
, but generates a list of
commands starting in state S. To ensure the correct state when the
commands are run, the first command is {init,S}.
Increases the expected length of command sequences generated within Gen by a factor N.
postconditions(Mod::atom(), Cmds::list(command()), Vals::list(term())) -> bool()
Given the values returned by a list of
commands, checks that all pre- and postconditions are satisfied. Mod
is a module defining a state machine, Cmds a list of commands
generated from it, and Vals the list of values returned by running
those commands. This function is useful when the list of commands
cannot be run just by calling run_commands/2
, for example
because the commands represent calls to functions in a different
programming language.
run_commands(Mod::atom(), Cmds::list(command())) -> {history(), dynamic_state(), reason()}
Runs a list of commands specified by the abstract state machine
in client module Mod. Before each command is run, its precondition is
checked by Mod:precondition/2, and after each command is executed, its
postcondition is checked by Mod:postcondition/3. The result contains the
history()
of execution, the state after the last command that was
executed successfully, and the reason()
execution stopped.
run_commands(Mod::atom(), Cmds::list(command()), Env::list({atom(), term()})) -> {history(), dynamic_state(), reason()}
Behaves like run_commands/2
, but also takes an environment
containing values for additional variables that may be referred
to in test cases. For example, if Env is [{x,32}],
then {var,x} may appear in the commands, and will evaluate
to 32. The variables names must be atoms (unlike generated variable
names, which are numbers).
zip(Xs::list(A), Ys::list(B)) -> list({A, B})
Zips two lists together,
but accepts lists of different lengths, stopping when the shorter
list stops. This is useful to zip together a list of commands with
the history returned by run_commands/2
, to display each
command together with its result in the output from QuickCheck.
Generated by EDoc, May 22 2009, 17:01:00.