An approach to animate Object-Z specifications using C++

Object-Z is an extension of the Z notation which facilitates specification of large, complex software by defining a system as a collection of independent classes. A number of contributions have been made so far to map Object-Z to various object-oriented languages. However, the given mapping approaches do not cover several Object-Z specification constructs, such as class union, object aggregation, object containment and some of the operation operators. Also, in much of the existing work, mapping rules are given in a very abstract form. In other words, they do not consider all cases in a detailed way needed to automate the mapping procedure. In our previous work, we partially tackled these issues; however, in this paper, we present a much more comprehensive way to animate Object-Z specifications using C++. The given method covers some constructs that have not been addressed in our previous work. Also, mapping rules are described with enough details facilitating automation. Finally, we consider some level of user interaction in our new method which increases the flexibility and efficiency of final codes from the user point of view.