Using semantics specified in Maude to generate test cases

Abstract

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. In this paper we propose 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. © 2012 Springer-Verlag.