Testing takes much of the time of the software development process, so several efforts have been devoted to automate it. Although initially much progress was done in testing for imperative languages, during the last years the gap has been filled. Following this line, this work presents a white-box (also known as glass-box, it takes into account the current implementation, in opposition to black-box) test case generator for Maude functional modules. This test case generator has been integrated with the Maude declarative debugger, allowing the user to debug the erroneous test cases at once. More information about this declarative debugger can be found here.
In order to use the command-line test case generator you have to download dd.maude.
In order to use the distributed version of the test case generator you have to download
ddd.maude.
The test case generator is initiated in Maude by loading the file dd.maude,
which starts an input/output loop that allows the user to interact with the
tool. Then, the user can enter Full Maude modules and commands, as well
as commands for the test case generator.
Once the tool is started, the user can choose whether he wants to check the test cases against a correct module or by himself. In the first case, a correct module has to be introduced with the command
(correct test module MODULE .)
where module is the module name. This module can be deselected with the command
(delete correct test module .)
If no correct module is selected, the tool will generate several test cases and some of them will be selected depending on a code coverage strategy. Currently, the user can use the global coverage and the function coverage strategies, being the former the default one. The user can switch between these strategies with the commands
(global coverage .) (function coverage .)
Moreover, the system coverage strategy can also be used when testing system modules by using the command
(system coverage .)
The user can choose between covering all the labeled statements in the testing process (by default) or selecting some of them by means of the command
(set test select on .)
Once this mode is activated, the user can select and deselect statements by using
(test select LABELS .) (test deselect LABELS .)where
LABELS is a list of statement labels separated by spaces.
Moreover, all the labels in statements of a flattened module can be selected or deselected with the commands
(test include MODULES .) (test exclude MODULES .)where
MODULES is a list of module names separated by spaces.
Similarly, the user can select to include or exclude from the coverage only a
certain kind of statements. The following commands include and exclude the
equations, memberships and rules of the list of modules MODULES:
(test include eqs MODULES .) (test exclude eqs MODULES .) (test include mbs MODULES .) (test exclude mbs MODULES .) (test include rls MODULES .) (test exclude rls MODULES .)
The selection mode can be switched off by using the command
(set test select off .)Before starting the testing process, the user can select the number of test cases with the following command, with
N the number
of steps used to produce such test cases:
(set test bound N .)
The testing process is started with the commands
(test [in MODULE-NAME :] OP1 [wrt OP2] .) (test sort [in MODULE-NAME :] SORT-NAME .)for testing operators (reduced by means of equations) and membership inferences, respectively.
OP1 is the operator we want to
test and, since the function coverage strategy tries to cover all the
recursive calls to a function, that could be different from the initial
one, OP2 allows the user to set it; SORT-NAME
is the sort to be tested; and
MODULE-NAME is the module where the reductions and membership
inferences make sense; if no module name is
given, the current module is used by default.
When checking the correctness of the test cases against a correct specification, the tool usually builds several terms, and thus it is impossible to show all of them at once. The user can use the command:
(show N incorrect .)
to see the first N terms incorrect with respect to the correct specification. To see the next M terms we provide the command:
(next N incorrect .)
Once the test cases are generated, the tool will distinguish all the possible results: the sort of the term is either bigger or smaller than the expected one, the term is not in normal form, the term is different from the expected one, or the user has to decide about its correctness. Each of these results can be directly debugged with the declarative debugger. The commands linking these tools are:
(invoke debugger with user test case N .)
(invoke debugger with normal form N .)
(invoke debugger with incorrect test case N .)
(invoke debugger with greater sort N .)
(invoke debugger with lesser sort N .)
where in all cases N refers to the index of the test case the user
wants to debug.
When testing system modules, the testing commands are very similar. A sort is tested with the command:
(test [in MODULE-NAME :] SORT .)If a correct module, introduced with the command shown above, has been previously introduced then the testing will consist in conformance testing, otherwise the tool will select some test cases following the coverage strategy. This command admits more options when dealing with invariants and linear temporal logic formulas:
(test [in MODULE-NAME :] SORT ARROW PATTERN s.t. NEGATED-INVARIANT .) (test [in MODULE-NAME :] SORT models PATTERN for FORMULA .)
When using narrowing to compute the set of test cases fulfilling a given coverage strategy, we can select whether we want a smaller set of possibly complicated test cases, or a bigger set of simpler terms. The user can switch between these two display techniques with:
(display small set .) (display simple set .)
We illustrate how to use the tool by means of examples. A session is started by
loading into Maude the file dd.maude (which already includes the Full Maude implementation).
Then, Full Maude modules and commands can be
entered, as well as commands for the test case generator.