Generating Java Skeletal Code with Design Contracts from Specifications in a Subset of Object Z

Object-Z is an object-oriented extension of the Z notation for formal specifications. Using Object-Z, structuring and developing large, complex software system specifications became possible by defining the systems as collections of independent classes and objects. The class schema framework in Object Z suggests that a one-to-one relationship exists between a class schema and a skeletal Java class with its design contract. The design contract for a Java class includes the invariant property of the class state, the pre and post conditions for the methods. This paper, demonstrates how Java skeletal code with design contracts can be generated from the specifications written in a subset of Object Z. Object Z class schema specification defined using a graphical user interface is converted to a XML representation. The Java skeletal code containing the design contracts is then generated by processing the XML representation