Comparison of formalisation approaches of UML class constructs in Z and Object-Z

UML, and other object-oriented approaches to system specification and design, are increasingly popular in industry. Many attempts have been made to formalise either the notations, the system models produced using these notations, or both. However, there have been no attempts to compare the expressiveness of the formal approaches. This paper compares Z and Object-Z approaches to object-oriented formalisation. The Z approaches reflect different formalisatiion goals (a formal model of the system, a formal model of a diagrammatic object-oriented model). The Object-Z approach produces compact formal models, but imposes a particular semantic interpretation on the UML notations.