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

Object-z is an extension of the z notation which facilitates specification of large, complexsoftware by defining a system as a collection of independent classes. a number of contributions havebeen made so far to map object-z to various object-oriented languages. however, the given mappingapproaches 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 rulesare given in a very abstract form. in other words, they do not consider all cases in a detailed way neededto automate the mapping procedure. in our previous work, we partially tackled these issues; however, inthis paper, we present a much more comprehensive way to animate object-z specifications using c++. thegiven method covers some constructs that have not been addressed in our previous work. also, mappingrules are described with enough details facilitating automation. finally, we consider some level of userinteraction in our new method which increases the flexibility and efficiency of final codes from the userpoint of view.