A Software Testing Tool for the Verification of Abstract Data Type Implementations from Formal Algebraic Specifications

This Work in Progress report presents an educational software tool for testing abstract data types implemented in C++ against formal algebraic specifications written in Maude, a formal specification language based on rewriting logic that allows the specification of abstract data types in a clear and concise manner. Maude specifications are executable, which provides two advantages: firstly, we can test our specifications and, secondly, we can obtain the results of the test cases automatically. Our software testing tool is fully integrated in the Eclipse programming environment and is platform-independent. We have developed an Eclipse plug-in that calls the Maude system to generate the test cases and translates them into a sequence of C++ instructions. The C++ instructions are compiled and executed, and the results are compared with the results obtained from the execution of the formal algebraic specification. Thus, the learning tool allows Software Engineering students to test their own implementations and correct their errors, encouraging the use of formal methods in their developments and resulting in an improved software quality.