Module eqc_statem

This module provides functions for testing operations with side-effects, which are specified via an abstract state machine.

Description

This module provides functions for testing operations with side-effects, which are specified via an abstract state machine. The state machine is in turn specified by a client module (which implements the behaviour eqc_statem). Given such a client, this module can generate and run command sequences, checking that all postconditions are satisfied, and shrinking failing sequences by discarding commands which do not contribute to the failure. Thus it can be used to find minimal command sequences which elicit an unexpected behaviour. Modules which use this one should -include_lib("eqc/include/eqc_statem") to import the functions that eqc_statem provides.

Symbolic Commands

Generated test cases are lists of symbolic commands (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.

States

The client module defines an initial state in which test cases begin, and how each command changes that state. For example, if test cases spawn a number of processes, then the state might be a list of the pids that have been spawned. The state is used both during test case generation and during test execution. Obviously, at generation time the actual values returned by commands are not known--they must be represented symbolically. Thus during test generation a symbolic state is constructed---in this case it might be
[{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.

Callback Functions

The client module specifies an abstract state machine by defining the following functions:

What Property Should We Test?

This module does not define any properties to test, it only provides functions to make defining such properties easy. A client module will normally contain a property resembling this one, which generates a command sequence using the client state machine, and then tests it:
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.

Data Types

call()

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

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

dynamic_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() = {'EXIT', term()}

The type of a caught exception.

expr()

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

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

reason() = ok | initialization | {precondition, bool()} | {postcondition, bool() | exit()} | {exception, exit()}

The reason execution of a command sequence terminated.

symbolic_state()

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() = {var, integer()}

A symbolic variable, which is replaced during test execution by the value bound by the corresponding command().

Function Index

command_names/1Returns a list of the command names used in Cmds.
commands/1Generates a list of commands, using the abstract state machine defined in module Mod.
commands/2Behaves like commands/1, but generates a list of commands starting in state S.
more_commands/2Increases the expected length of command sequences generated within Gen by a factor N.
postconditions/3Given the values returned by a list of commands, checks that all pre- and postconditions are satisfied.
run_commands/2Runs a list of commands specified by the abstract state machine in client module Mod.
run_commands/3Behaves like run_commands/2, but also takes an environment containing values for additional variables that may be referred to in test cases.
zip/2Zips two lists together, but accepts lists of different lengths, stopping when the shorter list stops.

Function Details

command_names/1

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)
 

commands/1

commands(Mod::atom()) -> gen(list(command()))

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/2

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}.

more_commands/2

more_commands(N::int(), Gen::gen(A)) -> gen(A)

Increases the expected length of command sequences generated within Gen by a factor N.

postconditions/3

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/2

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/3

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/2

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.