%0 Journal Article %T A Formal Mapping fromObject-Z Specification to C++ Code %J Scientia Iranica %I Sharif University of Technology %Z 1026-3098 %A Najafi, Mehrnaz %A Haghighi, Hassan %D 2013 %\ 12/01/2013 %V 20 %N 6 %P 1953-1977 %! A Formal Mapping fromObject-Z Specification to C++ Code %K Formal program development %K Object-Oriented Programming %K Animation %K Object-Z %K C++ %R %X Object-Z is an extension of Z which provides specific constructs to facilitate specification in an object-oriented style. A number of contributions have been made so far to animate Object-Z with various object-oriented programming languages. However, none of the existing animation methods present their mapping rules formally. Also, none of these animation methods prove the correctness of their mapping rules. In our previous work, we informally presented an animation method to map Object-Z specifications into C++ code. In this paper, we propose a formal mapping from Object-Z specifications to C++ code. We also prove the correctness of the given mapping rules. %U https://scientiairanica.sharif.edu/article_3438_6931119be29ac3234bad4b7b5f58602a.pdf