科研之友
微信
新浪微博
Facebook
分享链接
摘要
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.
- 出版日期2013-12
