A formal mapping from Object-Z speci cation to C++ code

Object-Z is an extension of Z which provides specic constructs to facilitate specication 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 specications into C++ code. In this paper, we propose a formal mapping from Object-Z specications to C++ code. We also prove the correctness of the given mapping rules.