For a limited, but still significant class of data models Δ and OCL boolean expressions Η (see below), our mapping ocl2fol satisfies the following property:

For every data model M in Δ , and every boolean expression exp in Η, with context M,

  • ocl2fol_th(M) is a first-order logic theory.
  • ocl2fol_def(M, exp) is  a set of first-order sentences.
  • ocl2fol_sen(M, exp) is a first-order sentence.

Moreover, let Ω(M) be the set of all the instances I of M such that, for every attribute att occurring in exp, and every object obj in I, if obj owns att, then att has a defined value in obj

Then, exp evaluates to true in every instance of M in Ω(M) if and only if ocl2fol_sen(Mexp) holds in every model of ocl2fol_th(M) U ocl2fol_def(M, exp).