OCL: Syntax, Semantics, and Tools

The Object Constraint Language OCL allows to formally specify constraints on a UML model. We present a formal syntax and semantics for OCL based on set theory including expressions, invariants and pre- and postconditions. A formal foundation for OCL makes the meaning of constraints precise and helps to eliminate ambiguities and inconsistencies. A precise language definition is also a prerequisite for implementing Case tools providing enhanced support for UML models and OCL constraints. We give a survey of some OCL tools and discuss one of the tools in some more detail. The design and implementation of the USE tool supporting the validation of UML models and OCL constraints is based on the formal approach presented in this paper.