Faculty of Electrical and Computer Engineering, Shahid Beheshti University G. C., Tehran, P.O. Box 1983963113, Iran
Abstract
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.
)