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.
[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.
[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.
@article{"International Journal of Information, Control and Computer Sciences:51231", author = "Mehrnaz Najafi and Hassan Haghighi", title = "Refinement of Object-Z Specifications Using Morgan-s Refinement Calculus", abstract = "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.", keywords = "Formal method, Formal specification, Formalprogram development, Morgan's Refinement Calculus, Object-Z", volume = "5", number = "11", pages = "1214-10", }