Module eqc

This module defines functions for writing and testing QuickCheck properties.

Version: 1.162

Description

This module defines functions for writing and testing QuickCheck properties. Much of the interface is provided via macros (defined in eqc.hrl). These are documented below:

?FORALL(X,Gen,Prop)

Property that holds if Prop holds for all values X that can be generated by Gen. For example,
 prop_reverse() ->
   ?FORALL(Xs,list(int()),
      lists:reverse(lists:reverse(Xs)) == Xs).
 
Generators are defined using the module eqc_gen.

?IMPLIES(Pre,Prop)

Property that holds if Prop holds whenever the precondition Pre is true. The precondition must be a boolean, but Prop can be any QuickCheck property. An implication is tested by discarding test cases which do not satisfy the precondition. This can make testing slow, since many more test cases may need to be generated to find 100 which satisfy the precondition. In the worst case, QuickCheck may not be able to find enough test cases that do satisfy the precondition, in which case the number actually found is reported. Some preconditions may also skew the test data badly--for example, a precondition that a list is sorted skews the test data towards short lists, since random longer lists are extremely unlikely to be sorted just by chance. ?IMPLIES works well for preconditions which are true with a high probability, but if the precondition is unlikely to hold, then it is better to write a custom generator which generates test cases where the precondition is true.

?WHENFAIL(Action,Prop)

Property that is equivalent to Prop, but performs Action (for its side effects) when Prop fails. This can be used to print additional information when a test case fails.

?TRAPEXIT(Prop)

A property which tests Prop in a separate process, trapping exits and treating them as test failures. QuickCheck always catches locally raised exceptions in properties, but when a test exits because a linked process fails, then the exit is NOT caught unless the body of the property is enclosed in ?TRAPEXIT. Shrinking is disabled for any ?FORALLs enclosed by ?TRAPEXIT (although not, of course, for ?FORALLs which enclose it). Thus ?TRAPEXIT would typically be used inside the innermost ?FORALL of a property.

?ALWAYS(N,Prop)

A property which tests Prop repeatedly N times, failing as soon as any of the tests of Prop fails. Typically this is used as follows:
?FORALL(X,...,?ALWAYS(N,?FORALL(Y,...,...)))
which generates N values of Y for each value of X. This is useful if Don't use this macro at the top-level of a property: numtests/2 is more appropriate for this.

?SOMETIMES(N,Prop)

A property which tests Prop repeatedly N times, failing only if all of the tests fail. In other words, the property passes if Prop sometimes passes. This is used in situations where test outcomes are non-deterministic, to search for test cases that consistently fail. A property such as ?FORALL(X,...,?SOMETIMES(10,...)) will find test cases X for which the property inside ?SOMETIMES is very likely to fail.

Data Types

counterexample()

abstract datatype: counterexample()

A counter-example to a QuickCheck property, which can be obtained using counterexample/0 or counterexample/1, and used to repeat a test, or test a different property in the same case. Counterexamples are represented by the values bound by ?FORALL--for the counterexample to make sense independently, it's important that these were generated without side-effects.

property()

abstract datatype: property()

QuickCheck properties, which can either be boolean expressions, or constructed using the functions in this module. QuickCheck properties are tested using quickcheck/1.

Function Index

active_users/0Fetch a list of the currently active users of your licence.
aggregate/2Like collect/2, but collects a list of values from each test, rather than just one.
backtrace/0Displays a stack backtrace from the last exception QuickCheck caught.
check/2Tests the property in the case given.
classify/3Property which is logically equivalent to Prop, but also classifies test cases and displays the distribution of test case classes when testing is complete.
collect/2Equivalent to classify(true, S, Prop).
counterexample/0Returns the last counter-example found.
counterexample/1Tests the property in the same was as quickcheck/1, but if a test fails, then the failing test case is returned as a counterexample.
counterexample/2Nearly equivalent to counterexample(M:P()) (but see recheck/1).
counterexample/3Nearly equivalent to counterexample(apply(M,P,Xs)) (but see recheck/1).
counterexamples/0Returns a list of the counterexamples found by the last call of eqc:module, paired with the name of the property that failed.
fails/1A property which succeeds when its argument fails.
force_start/0Equivalent to start().
measure/3Collects the values of X while testing Prop, and if all tests pass, displays statistics such as the minimum, average, and maximum values, identified by the name Name.
module/1Tests all the properties exported from a module, given the module name.
numtests/2Property which is logically equivalent to Prop, but is tested N times rather than 100.
quickcheck/1Tests the property in 100 random cases, printing a counter-example if one is found.
quickcheck/2Nearly equivalent to quickcheck(M:P()) (but see recheck/1).
quickcheck/3Nearly equivalent to quickcheck(apply(M,P,Xs)) (but see recheck/1).
recheck/0Equivalent to recheck(1).
recheck/1Repeat the Nth-most-recent failed test, where N>=1 and recheck(1) repeats the most recent failure, so that (for example) tests can be repeated with tracing turned on.
registration/1Create a QuickCheck licence for the current user, using a one-time registration identifier.
reserve/1Reserve a QuickCheck licence for this machine.
reserved_until/0The local time that the currently active QuickCheck licence is reserved until.
start/0Equivalent to start(true).
start/1Starts the QuickCheck server.
stop/0Stops the QuickCheck server.
unlock_licence/0Unlock the Quviq licence files.
version/0Returns the version number of this version of QuickCheck.
watch_shrinking/0Equivalent to watch_shrinking(1).
watch_shrinking/1Repeats the N-th most recent failed test, like recheck/1, but displays all the test cases explored during shrinking.
withseed/2(Deprecated.) Run a test case with a given seed.

Function Details

active_users/0

active_users() -> term()

Fetch a list of the currently active users of your licence. The users are sorted by the expiry times of their current sessions; thus the user whose licence may first become free is first in the list. Of course, other users who continue running QuickCheck will automatically extend their sessions, so there is no guarantee that a licence will actually be released at the time indicated.

aggregate/2

aggregate(L::list(term()), Prop::property()) -> property()

Like collect/2, but collects a list of values from each test, rather than just one. The lists from each test are aggregated, and the statistics displayed show how often each list element occurred in the aggregated data.

A typical use would be to aggregate the list of command names generated by eqc_statem:commands/1, in order to see how often each individual command appeared in generated tests:

aggregate([F || {set,_,{call,_,F,_}} <- Cmds], ...) 

backtrace/0

backtrace() -> ok

Displays a stack backtrace from the last exception QuickCheck caught. Note that this is only possible if the exception is raised in the process in which the test case starts. If a test case fails because of an exception in another, linked, process, then no backtrace is available. Calls to functions in the implementation of QuickCheck itself are not included in the backtrace.

If you really need to see a backtrace from a linked process, then you can do so by catching the exception yourself in that process, using erlang:get_stacktrace() to obtain the backtrace, and printing it yourself.

check/2

check(P::property(), Values::counterexample()) -> bool()

Tests the property in the case given. Counterexamples are generated by testing a property using counterexample/1 or counterexample/0, and contain a list of the values bound by ?FORALL. A property tested by check should begin with the same sequence of ?FORALL s as the property from which the counterexample was generated, otherwise the results will be unpredictable. In particular, there is no check that the values in the counterexample could actually have been generated by the ?FORALL s in the property under test.

check/2 can be used without a QuickCheck licence, allowing anyone to run tests that a licenced user has generated.

classify/3

classify(B::bool(), S::term(), Prop::property()) -> property()

Property which is logically equivalent to Prop, but also classifies test cases and displays the distribution of test case classes when testing is complete. If the boolean is true then the current test case is labelled with the term S, and, after testing is complete, QuickCheck prints out the percentage of test cases carrying each label. This can be used to check that the space of possible test cases has been covered reasonably well. For example, classifying test cases according to the length of a list enables one to see whether unreasonably many lists were short. Classifying test cases is a way to discover skewed distributions, such as can arise from using ?IMPLIES. It is good practice to check the distribution of test data using classify or collect/2, at least while properties are being developed.

Each test case can be labelled with any number of labels: QuickCheck then displays the percentage of each label in the generated test data.

Calls of classify or collect can be nested, in which case each call generates its own table of distributions.

collect/2

collect(S::term(), Prop::property()) -> property()

Equivalent to classify(true, S, Prop).

counterexample/0

counterexample() -> true | counterexample()

Returns the last counter-example found. See counterexample/1.

counterexample/1

counterexample(P::property()) -> true | counterexample()

Tests the property in the same was as quickcheck/1, but if a test fails, then the failing test case is returned as a counterexample.

counterexample/2

counterexample() -> term()

Nearly equivalent to counterexample(M:P()) (but see recheck/1).

counterexample/3

counterexample() -> term()

Nearly equivalent to counterexample(apply(M,P,Xs)) (but see recheck/1).

counterexamples/0

counterexamples() -> list({atom(), counterexample()})

Returns a list of the counterexamples found by the last call of eqc:module, paired with the name of the property that failed.

fails/1

fails(P::property()) -> property()

A property which succeeds when its argument fails. Sometimes it is useful to write down properties which do not hold (even though one might expect them to). This can help prevent misconceptions. fails(P) is tested in the same way as P, but fails only if P succeeds 100 times. Thus fails(P) declares that QuickCheck should be able to find a counter-example to property P.

force_start/0

force_start() -> term()

Equivalent to start().

measure/3

measure(Name::atom() | string(), X::number() | list(number()), Prop::property()) -> property()

Collects the values of X while testing Prop, and if all tests pass, displays statistics such as the minimum, average, and maximum values, identified by the name Name. X can also be a list of values, in which case all of them are included in the measurements.

module/1

module(Mod::atom()) -> list(atom())

Tests all the properties exported from a module, given the module name. Any function with arity zero whose name begins with "prop_" is treated as a property. The result is a list of the names of the properties that failed.

numtests/2

numtests(N::int(), Prop::property()) -> property()

Property which is logically equivalent to Prop, but is tested N times rather than 100. If numtests appears more than once in a property, then the outermost use takes precedence.

quickcheck/1

quickcheck(P::property()) -> bool()

Tests the property in 100 random cases, printing a counter-example if one is found. Initially small test cases are generated, then the size increases as testing progresses (see eqc_gen, ?SIZED, eqc_gen:resize/2 for the way size affects test data generation). The result is true if all tests succeeded (or if one failed, and failure was expected). On success, quickcheck analyses the distribution of test case labels. On failure, quickcheck tries to simplify the counter-example found as far as possible (see shrinking, described in eqc_gen).

quickcheck/2

quickcheck() -> term()

Nearly equivalent to quickcheck(M:P()) (but see recheck/1).

quickcheck/3

quickcheck() -> term()

Nearly equivalent to quickcheck(apply(M,P,Xs)) (but see recheck/1).

recheck/0

recheck() -> bool()

Equivalent to recheck(1).

recheck/1

recheck(N::integer()) -> bool()

Repeat the Nth-most-recent failed test, where N>=1 and recheck(1) repeats the most recent failure, so that (for example) tests can be repeated with tracing turned on. The result is true if the test now succeeds, if the test case is now excluded by a modified precondition, or if the test is now expected to fail (i.e. is defined using fails/1). Test cases are not saved as data, they are regenerated using the same random seed when the test is repeated. If the generators have been modifed in the meantime, or if the generators used have side effects, then the generated data may not be the same as before.

The history of failed tests is collected by quickcheck/1. Tests which were expected to fail (see fails/1) are not recorded in the history. The history is not affected by recheck/1 itself.

A potential gotcha is that properties are saved in the history as values, not as names, with the result that repeating a test after loading recompiled code will use the old code, unless the property itself makes external calls. Properties saved in the history by quickcheck/2 and quickcheck/3, though, are saved "by name", and so rechecking them will call any newly loaded code.

registration/1

registration() -> term()

Create a QuickCheck licence for the current user, using a one-time registration identifier. The registration identifier can also be supplied the first time QuickCheck is started, via a dialogue box.

NOTE: this replaces your licence file with a new one; if your licence is currently installed and working, then eqc:registration/1 will destroy it! Registering your licence more than once is only useful if your licence file is corrupt--and only helps if your licence administrator resets your licence at the same time. You should therefore only use eqc:registration/1 when you receive an email from Quviq's licence server instructing you to do so.

In particular, if you encounter a problem related to the "tamperfree seal" on Quviq licence files, then calling eqc:registration/1 will not help--it will make the problem worse.

reserve/1

reserve() -> term()

Reserve a QuickCheck licence for this machine. Reservations can be made for up to seven days; once a licence is reserved, it cannot be used on another machine until the reservation has expired. Reserving a floating licence can be useful to ensure that another user does not begin using it at a critical time, or, since a reserved licence can be used without internet access, to prepare a laptop for a trip during which internet access will not be available.

Examples: eqc:reserve({3,days}), eqc:reserve({6,hours}), eqc:reserve(5). (If the unit, days or hours, is not specified, then it defaults to days).

This call always succeeds, and returns {reserved_until,Time}, where Time is the local time the licence is now reserved until.

reserved_until/0

reserved_until() -> term()

The local time that the currently active QuickCheck licence is reserved until.

start/0

start() -> term()

Equivalent to start(true).

start/1

start(Force::bool()) -> pid()

Starts the QuickCheck server. If it is already running on this node, nothing is done.

Each user can run only one instance of the QuickCheck server at a time. If the server is already running on another Erlang node, it will be terminated automatically if Force is true. If another instance is running, and Force is false, then the new instance will not start.

stop/0

stop() -> term()

Stops the QuickCheck server. QuickCheck properties are tested in the QuickCheck server process, which is spawned automatically when quickcheck is first called. Usually there is no need to stop the QuickCheck server explicitly, but if a need does arise then this function can be used. For example, if the shell process crashes and is restarted, then the QuickCheck server should be stopped and restarted too, since otherwise the server will crash when it attempts to write to the console.

unlock_licence/0

unlock_licence() -> term()

Unlock the Quviq licence files. The lock protects your licence from damage when the files are accessed by concurrent processes. However, if a node crashes while holding the lock, then you may need to unlock the licence files manually using this function. Make certain that no other process actually is running QuickCheck before calling this function, otherwise your licence may be corrupted.

version/0

version() -> term()

Returns the version number of this version of QuickCheck.

watch_shrinking/0

watch_shrinking() -> term()

Equivalent to watch_shrinking(1).

watch_shrinking/1

watch_shrinking(N::integer()) -> ok

Repeats the N-th most recent failed test, like recheck/1, but displays all the test cases explored during shrinking. The test cases are reported in the order they are tried, so each Failed test is followed by attempts to shrink it, while each OK test (or test skipped because a precondition failed) is followed by an alternative way to shrink the last Failed test. The last Failed test displayed is the final result of shrinking.

withseed/2

withseed() -> term()

This function is deprecated: Replaced by recheck/0 and recheck/1. Methods to save test cases more permanently are under development. withseed doesn't correctly repeat tests anyway, so don't use it.

Run a test case with a given seed.


Generated by EDoc, May 22 2009, 17:01:00.