The Definition of Transitive Closure with OCL - Limitations and applications

The Object Constraint Language (OCL) is based on rst- order logic and set theory. As the most well-known application, OCL is used to formulate well-formedness rules in the UML metamodel. Here, the transitive closure of a relationship is de ned in terms of an OCL invariant, which seems to contradict classical results on the expressive power of rst-order logic. In this paper, we give su cient justi cation for the correctness of the def- inition of transitive closure. Our investigation reinforces some decisions made in the semantics of UML and OCL. Currently, there is a lively debate on the same issues in the semantics of the upcoming UML 2.0.