We focus our test cases on the correctness of the obtained data values, therefore they are generated from the Maude specification based on the data type constructors and the corresponding membership axioms. On the other hand, the observation of the implementation under test is done for each data type through explicit methods defined by the user. The tool is fully integrated in the Eclipse environment and is platform-independent. We have developed an Eclipse plug-in that calls the Maude system to generate the test cases and then translates them into a sequence of C++ instructions. The C++ instructions are compiled and executed, and the results are compared with the results from the specification.
The tool is being used during this academic year by the Computer Science students at the Universidad Complutense de Madrid in the data types course. They have tested typical data type implementations, like stacks, lists, and binary search trees, as well as other data types based on them. The experience is being very useful as it allows the students to test their implementations and correct their errors.