Testing is one of the most important and most time-consuming tasks in the software developing process and thus techniques and systems to generate and check test cases have become crucial. For these reasons, when specifying a prototype of a programming language it may be very useful to have a tool that, beyond testing the semantics of the program, generates test cases for the programs written in the specified language. In this way, we could use the test cases generated in the prototyping stage to check the implementation. To build these prototypes we can use rewriting logic, which has been proposed as a logical framework where other logics can be represented, and as a semantic framework for the specification of languages and systems.
We present here a technique to generate test cases for programs written in programming languages specified in Maude, although it can be generalized to similar languages. In this way Maude becomes an even more powerful prototyping language providing a test-case generator (in addition to an interpreter of the language). The test cases can be generated in two ways: computing a set of test cases using all the instructions required by a given coverage criterion or trying to disprove a property over the program. This methodology has been implemented in a Maude prototype and its use is described by means of an example.
In order to use the command-line test case generator you have to download dd.maude.
WhileL semantics: a module where the semantics of a simple language, with
skip, assignment, If statement, While loop, and composition
of instructions, is defined: whilel-semantics.
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 select the module where testing takes place with the command
(semantics module MODULE .)
where MODULE is the module identifier. He can also introduce the sort of the
statements that we want to cover with:
(set sort statements SORT .)
where SORT is the chosen sort. Once these commands are introduced we can ask the
system to show how the module has been transformed to associate indices to each term of the given
sort with the command:
(show semantics rules .)
We can also ask the system to show the mapping between the rules and the executed statements with:
(show applied statements .)
If the tool fails to associate the appropriate information to a rule, the following commands can be used:
Maude> (rule Q is not associated to any statement .) The mapping for rule Q has been updated. Maude> (rule Q is associated to VL .) The mapping for rule Q has been updated.
where Q is a rule label and VL is the list of variables
identifying the applied statements.
We can now introduce the program we want to test with the following command:
Maude> (object program TERM .)
where TERM is the program written in the programming language specified in MODULE.
Since we may be interested in only covering some of the statements of the initial coverage (e.g., because
we want to know whether a specific one, such as an exception, is reached). The user can modify the statements
in the coverage with:
Maude> (statements in coverage NL .) The required coverage has been updated.
where NL is a list of natural numbers indicating the statements to be covered.
When all the options have been set, we can start the testing process with:
(start semantics testing .)
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.