From Object-Z Specification to Groovy Implementation

Document Type : Article


Faculty of Computer Science and Engineering, Shahid Beheshti University G.C., Tehran, 1983969411, Iran


So far, valuable researches have been conducted on mapping object-oriented specification notations, such as Object-Z, to different object-oriented programming languages, such as C++. However, the results of selecting JVM-based programming languages for mapping have not covered most of basic Object-Z structures. In this paper, the Groovy language, as a dynamic JVM-based language, is selected to overcome some of the existing limitations. As the main contribution, the rules required for mapping Object-Z specifications to executable Groovy code are introduced. The proposed rules cover notions such as multiple inheritance, inverse specification of functions, functions defined on generic definitions, and free type constructors. These notions have not been covered in previous methods for formal program development from object-oriented specifications, regardless of the selected formal specification language and target programming language. In addition, in this paper, the parallel composition construct is mapped to a parallel, executable code to improve the faithfulness of the final code to the initial specification. We also introduce a mapping rule for the class union construct, which has not yet been provided for any JVM-based language. Unlike previous works, instead of presenting the mapping rules in terms of natural languages, we present them in terms of some formal mapping rules.


Main Subjects

1. Woodcock, J., Larsen, PG., Bicarregui, J., et al.
Formal methods: Practice and experience", ACM
Computing Surveys (CSUR), 41(4), p. 19 (2009).
2. Fitzgerald, J., Bicarregui, J., Larsen, P.G., et al.
Industrial Deployment of Formal Methods: Trends
and Challenges", In Industrial Deployment of System
Engineering Methods, pp. 123-143, Springer (2013).
3. Naja , M., Haghighi, H., and Zohdi Nasab, T. A survey
on formal, object-oriented program development
approaches", Scientia Iranica, 22(3), pp. 1001-1007
4. Smith, G., The Object-Z Speci cation Language,
Springer Science & Business Media (2012).
5. Rose, G., Formal Object-Oriented Speci cation Using
Object-Z, Macmillan, United Kingdom (2000).
6. Woodcock, J. and Davies, J., Using Z: Speci cation,
Re nement and Proof, Prentice Hall, NJ (1996).
7. Ramkarthik, S. and Zhang, C. Generating Java
skeletal code with design contracts from speci cations
in a subset of object-Z", Computer and Information
Science, 2006 and 2006 1st IEEE/ACIS International
Workshop on Component-Based Software Engineering,
Software Architecture and Reuse. ICIS-COMSAR
2006. 5th IEEE/ACIS International Conference on,
Honolulu, HI, pp. 405-411, IEEE Computer Society
Press (2006).
8. Naja , M. and Haghighi, H. An animation approach
to develop c++ code from object-z speci cations",
Computer Science and Software Engineering (CSSE),
2011 CSI International Symposium on, pp. 9-16, IEEE
9. Naja , M. and Haghighi, H. An approach to animate
Object-Z speci cations using C++", Scientia Iranica,
19(6), pp. 1699-1721 (2012).
10. Naja , M. and Haghighi, H. An approach to develop
C++ code from object-Z speci cations", 2nd World
Conference on Information Technology (2011).
11. Ni, X. and Zhang, C. Converting speci cations in a
subset of Object-Z to skeletal spec# code for both
static and dynamic analysis", Journal of Object Technology,
7(8), pp. 165-185 (2008).
3438 F. Zaker et al./Scientia Iranica, Transactions D: Computer Science & ... 25 (2018) 3415{3441
12. Naja , M. and Haghighi, H. A formal mapping from
Object-Z speci cation to C++ code", Scientia Iranica.
Transaction D, Computer Science & Engineering,
Electrical Engineering, 20(6), p. 1953 (2013).
13. Rafsanjani, G.B. and Colwill, S.J. From Object-Z
to C++: A structural mapping", Z User Workshop,
London 1992, pp. 166-179, Springer (1993).
14. Griths, A. From Object-Z to Ei el: a rigorous
development method", Technology of Object-Oriented
Languages and Systems (TOOLS 18), pp. 293-308
15. Ramkarthik, S. and Zhang, C. Generating Java
skeletal code with design contracts from speci cations
in a subset of object Z", Computer and Information
Science, 2006 and 2006 1st IEEE/ACIS International
Workshop on Component-Based Software Engineering,
Software Architecture and Reuse. ICIS-COMSAR
2006. 5th IEEE/ACIS International Conference on,
pp. 405-411, IEEE (2006).
16. Johnston, W. and Rose, G. Guidelines for the manual
conversion of Object-Z to C++", SVRC Technical
Report, pp. 93-14 (1993).
17. Fukagawa, M., Hikita, T. and Yamazaki, H. A
mapping system from Object-Z to C++", Software Engineering
Conference, 1994. Proceedings., 1994 First
Asia-Paci c, pp. 220-228, IEEE (1994).
18. Wang, Z., Xie, M., and Zhao, Y. Transform mechanisms
of object-z based formal speci cation to Java",
Computational Intelligence and Software Engineering,
2009. CiSE 2009. International Conference on, pp. 1-
4, IEEE (2009).
19. Jackson, M. Developing Ada programs using the
Vienna development method (VDM)", Software: Practice
and Experience, 15(3), pp. 305-318 (1985).
20. Van Katwijk, J., Durr, E., and Goldsack, S. Hybrid
object-oriented real-time software development with
VDM++", Formal Engineering Methods., 1997. Proceedings.,
First IEEE International Conference on, pp.
17-26, IEEE (1997).
21. Albalooshi, F. and Long, F. Multiple view environment
supporting VDM and Ada", IEE Proceedings-
Software, 146(4), pp. 203-219 (1999).
22. Moulding, M. and Newton, A. Rapid prototyping
from VDM speci cations using Ada", Automating
Formal Methods for Computer Assisted Prototying,
IEE Colloquium on, pp. 11-21, IET (1992).
23. Chedgey, C., Kearney, S., and Kugler, H.-J. Using
VDM in an object-oriented development method for
Ada software", VDM'87 VDM-A Formal Method at
Work, pp. 63-76 (1987).
24. O'Neill, D. VDM development with Ada as the target
language", VDM'88 VDM-The Way Ahead, pp. 116-
123 (1988).
25. Lou, Y. VDM/C++: a design and implementation
framework", Thesis, Concordia University (1994).
26. Liu, H. and Zhu, B. Refactoring formal speci cations
in object-Z", Computer Science and Software Engineering,
2008 International Conference on, pp. 342-
345, IEEE (2008).
27. McComb, T. Refactoring object-z speci cations",
FASE, Berlin, Germany, pp. 69-83, Springer (2004).
28. McComb, T. and Smith, G. Architectural design
in Object-Z", Software Engineering Conference, 2004.
Proceedings. 2004 Australian, pp. 77-86, IEEE (2004).
29. McComb, T. and Smith, G. Compositional class
re nement in Object-Z", FM 2006: Formal Methods,
pp. 205-220 (2006).
30. McComb, T. and Smith, G. A minimal set of refactoring
rules for Object-Z", Lecture Notes in Computer
Science, 5051, pp. 170-184 (2008).
31. McComb, T. and Smith, G. Introducing objects
through re nement", FM 2008: Formal Methods, pp.
358-373 (2008).
32. Rasoolzadegan, A. and Barforoush, A.A. A new
approach to software development process with formal
modeling of behavior based on visualization", The
Sixth International Conference on Software Engineering
Advances (2011).
33. Rasoolzadegan, A. and Barforoush, A.A. Reliable yet

exible software through formal model transformation
(rule de nition)", Knowledge and Information Systems,
40(1), pp. 79-126 (2014).
34. Ruhroth, T. Refactoring Object-Z speci cations",
18th Nordic Workshop on Programming Theory (2006).
35. Smith, G. Introducing reference semantics via re nement",
ICFEM, pp. 588-599, Springer (2002).
36. Goldsack, S. and Lano, K. Annealing and data
decomposition in VDM", ACM Sigplan Notices, 31(4),
pp. 32-38 (1996).
37. Lu, J. Introducing data decomposition into VDM
for tractable development of programs", ACM Sigplan
Notices, 30(9), pp. 41-50 (1995).
38. Goldsack, S., Durr, E., and Plat, N. Object rei cation
in VDM++", ICSE-17: Workshop on Formal Methods
Application in Software Engineering Practice, pp. 194-
201 (1995).
39. Lano, K. and Goldsack, S. Re nement of distributed
object systems", Proc. of Workshop on Formal
Methods for Open Object-Based Distributed Systems,
Boston, MA, pp. 99-114, Springer (1997).
40. Lano, K. and Goldsack, S. Re nement, subtyping and
subclassing in VDM++", Theory and Formal Methods,
95, pp. 1-446 (1994).
41. Butler, M., Abrial, J.R., Damchoom, K., et al. Applying
Event-B and Rodin to the lestore........

Volume 25, Issue 6
Transactions on Computer Science & Engineering and Electrical Engineering (D)
November and December 2018
Pages 3415-3441