From Object-Z specification to Groovy implementation

So far, valuable research studies have been conducted on mapping notations of object-oriented specification, such as Object-Z, in 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 execute Groovy code are introduced. The proposed rules cover notions such as multiple inheritance, inverse specification of functions, functions dened on generic denitions, and free-type constructors. Previous methods have not covered these notions for the formal development of program 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. A mapping rule for the class unio‎n construct is introduced, which has not yet been provided for any JVMbased language. Unlike previous works, instead of presenting the mapping rules in terms of natural languages, they are presented in terms of some formal mapping rules.