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

Authors: Mehrnaz Najafi, Hassan Haghighi

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

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1056456

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.