RoZ automatically generates the Z schemas skeletons corresponding to a UML class diagram. To have a complete Z specification, you must add information like the definition of the type of the attributes and the constraints on the class diagram.
In the Rational Rose tool, each concept is complemented by a specification form to express additional information. We use these forms to express constraints, pre and post-conditions of operations etc. Constraints are written in the Z latex syntax in "Documentation" fields of forms.
On the contrary, the type definition cannot be done in the RoZ environment, you have to create a file containing it. The type declaration must be in the Z Latex format. In the example above, we have to define the types of the attributes i.e. NAME, TEL and DIGIT8.
From a UML class diagram and its annotations, RoZ generates a complete Z specification. The UML model is translated into Z formal skeletons which are completed by the annotations. So the UML model supplies the formal specification structure while the annotations provide the details. The UML translation into Z is made for the main concepts of UML class diagrams (class, operation, association, inheritance, aggregation and composition). Details about these translation rules are given in the documentation of RoZ.
For example, from the class "PERSON" and its annotations, RoZ generates two Z schemas. The static part of "PERSON" is represented by two Z schemas "PERSON" and "PersonExt". The first one defines attributes and the second one describes the set of existing persons. In the figure below, the "PERSON" schema contains the constraints expressed in the "Documentation" fields of "tel" and "cardnb". The first constraint expresses that the set of telephone numbers must not be empty and the constraint written in the form of "cardnb" specifies a checksum constraint on this card number.