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

This paper presents an educational tool for testing abstract data types implemented in C++ against formal algebraic specications written in Maude, a formal specication language based on rewriting logic that allows the specication of abstract data types in a clear and concise manner. Maude specications are executable, which provides two advan-tages: rstly, we can test our specications 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 specication 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 dened 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 specication. 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