OCL FO : first-order expressive OCL constraints for efficient integrity checking

Abstract

OCL is the standard language for defining constraints in UML class diagrams. Unfortunately, as we show in this paper, full OCL is so expressive that it is not possible to check general OCL constraints efficiently. In particular, we show that checking general OCL constraints is not only not polynomial, but not even semidecidable. To overcome this situation, we identify OCL FO, a fragment of OCL which is expressively equivalent to relational algebra (RA). By equivalent we mean that any OCL FO constraint can be checked through a RA query (which guarantees that OCL FO checking is efficient, i.e., polynomial), and any RA query encoding some constraint can be written as an OCL FO constraint (which guarantees expressiveness of OCL FO). In this paper we define the syntax of OCL FO, we concisely determine its semantics through set theory, and we prove its equivalence to RA. Additionally, we identify the core of this language, i.e., a minimal subset of OCL FO equivalent to RA.