A formal mapping from Object-Z specication to C++ code

Object-z is an extension of z which provides specic constructs to facilitatespecication in an object-oriented style. a number of contributions have been made sofar to animate object-z with various object-oriented programming languages. however,none of the existing animation methods present their mapping rules formally. also, noneof these animation methods prove the correctness of their mapping rules. in our previouswork, we informally presented an animation method to map object-z specications intoc++ code. in this paper, we propose a formal mapping from object-z specications toc++ code. we also prove the correctness of the given mapping rules.