An Innovative Teaching Tool for the Verification of Abstract Data Type Implementations from Formal Algebraic Specifications

• Published in: Procedia computer science 2012, Vol.9, p.1743-1752
• Main Authors: Víırseda, Rafael del Vado, Morente, Fernando Pérez
• Format: Article
• Language: English
• Subjects: Abstract data types; Formal algebraic specifications; Software testing tools; Tools to aid in teaching
• ISSN: 1877-0509; 1877-0509
• DOI: 10.1016/j.procs.2012.04.192

This paper presents an educational 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 advan-tages: firstly, we can test our specifications and, secondly, we can obtain the results of the test cases automatically. We focus our test cases on the correctness of the obtained data values generated from the Maude specification based on the data type constructors and the corresponding membership axioms. The observation of the implementation under test is done for each abstract data type through explicit methods defined by the user. The teaching 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 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 formal algebraic specification. This educational tool is being used during this academic year by the Computer Science students in a data types course. They have tested typical abstract data type implementations, like complex numbers, stacks, lists, and binary search trees, as well as other data types based on them.