An animation approach to develop C++ code from Object-Z specifications

Object-Z is an extension of Z 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 rules do not cover some Object-Z specification constructs, such as class union, object aggregation, object containment and some operation operators. Also, most of the existing works propose rules in a general way. In other words, they do not consider all cases in a detailed way needed to automate the mapping. In this paper, we present a much more comprehensive way to animate Object-Z specifications using C⁺⁺ such that mapping rules are described with enough details that facilitate automation capability. Also, the given method covers some constructs that have not been considered in the literature yet.