Refinement of Object-Z Specifications Using Morgan-s Refinement Calculus

Morgan-s refinement calculus (MRC) is one of the well-known methods allowing the formality presented in the program specification to be continued all the way to code. On the other hand, Object-Z (OZ) is an extension of Z adding support for classes and objects. There are a number of methods for obtaining code from OZ specifications that can be categorized into refinement and animation methods. As far as we know, only one refinement method exists which refines OZ specifications into code. However, this method does not have fine-grained refinement rules and thus cannot be automated. On the other hand, existing animation methods do not present mapping rules formally and do not support the mapping of several important constructs of OZ, such as all cases of operation expressions and most of constructs in global paragraph. In this paper, with the aim of providing an automatic path from OZ specifications to code, we propose an approach to map OZ specifications into their counterparts in MRC in order to use fine-grained refinement rules of MRC. In this way, having counterparts of our specifications in MRC, we can refine them into code automatically using MRC tools such as RED. Other advantages of our work pertain to proposing mapping rules formally, supporting the mapping of all important constructs of Object-Z, and considering dynamic instantiation of objects while OZ itself does not cover this facility.




References:
[1] S. Ramkarthik, and C. Zhang, "Generating java skeletal code with
design contracts from specifications in a subset of object-z, "in 5th
IEEE/ACIS International Conference on Computer and Information
Science, , pp. 405-411, 2006.
[2] X.Ni, and C.Zhang, "Converting specifications in a subset of object-z to
skeletal spec# code for both static and dynamic analysis, " in Journal of
Object Technology, Vol. 7, No. 8, pp.165-185, 2008.
[3] T.McComb, and G.Smith, "Animation of object-z specifications using a
z animator, "in First International Conference on Software Engineering
and Formal Methods, pp. 191-200, 2003.
[4] G. Smith, The Object-Z Specification Language: Advances in Formal
Methods, Kluwer Academic Publishers, 2000.
[5] R. Duke, and G. Rose, Formal Object-Oriented Specification Using
Object-Z, Macmillan, UK, 2000.
[6] G. Rafsanjani, and S. J. Colwill, "From object-z to c++: a structural
mapping," in Z User Meeting (ZUM-92), Springer-Verlag, pp. 166-179,
1992.
[7] M. Fukagawa, T. Hikita, and H. Yamazaki, "A mapping system from
object-z to c++," in 1st Asia-Pacific Software Engineering Conference
(APSEC94), IEEE Computer Society Press, pp. 220-228, 1994.
[8] W. Johnston, and G. Rose," Guidelines for the manual conversion of
object-z to c++, " in SVRC Technical Report 93-14, 1993.
[9] M. Najafi, and H. Haghighi, "An animation approach to develop c++
code from object-z specifications, " in International Symposium on
Computer Science and Software Engineering, pp. 9-16, 2011.
[10] C. Fischer, Combination and implementation of processes and data:
from csp-oz to java, PhD Thesis. University of Oldenburg, 2000.
[11] Z.Wang, M.Xia, and Y.Zhao, "Transform mechanisms of object-z based
formal specification to java," in International Conference on
Computational Intelligence and Software Engineering, pp. 1-4, 2009.
[12] A. Griffiths, "From object-z to eiffel: a rigorous development method,"
in Technology of Object-Oriented Languages and Systems: TOOLS 18,
Prentice-Hall, 1995.
[13] J. Derrick, and E. A. Boiten, "Refinement of objects and operations in
object-z, " in Formal Methods for Open Object-based Distributed
Systems IV, pp. 257-277, Kluwer Academic Publishers, 2000.
[14] J. Derrick, and E. A. Boiten, Refinement in z and object-z: foundations
and advanced applications, Formal Approaches to Computing and
Information Technology (FACIT), 1st edition, Springer-Verlag, 2001.
[15] C. Morgan, Programming from specifications, Prentice Hall, 1990.
[16] J. Woodcock, and J. Davies, Using z: specification, refinement, and
proof, Prentice-Hall, 1996.
[17] D. A. Carrington, and K. A. Robinson, "Tool support for the refinement
calculus, "in Computer-Aided Verification, Vol. 3 of DIMACS Series in
Discrete Mathematics and Theoretical Computer Science, pp. 381-394,
American Mathematical Society, 1991.