Focusing on object-oriented designs, this paper proposes a mapping
for translating systems modelled in the Unified Modelling Language (UML)
incorporating Object Constraint Language (OCL) constraints into formal
software specifications in Object-Z. Joint treatment of semi-formal model
constructs and constraints within a single translation framework and conversion
tool is novel, and leads to the generation of much richer formal specifications
than is otherwise possible. This paper complements previous analyses by
paying particular attention to the generation of complete Object-Z structures.
Integration of proposals to extend the OCL to include action constraints also
boosts the expressivity of the translated specifications. The main features of a
tool support are described.