Specification

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

For every data model M in Δ , and every expression exp in Η, with context M, I instance of M then,

Eval(exp,I) = true if only if O2Fenv+(M,I,exp) satisfy O2Ftrue(exp)
Eval(exp,I) = false if only if O2Fenv+(M,I,exp) satisfy O2Ffalse(exp)
Eval(exp,I) = null if only if O2Fenv+(M,I,exp) satisfy O2Fnull(exp)
Eval(exp,I) = invalid if only if O2Fenv+(M,I,exp) satisfy O2Finval(exp)

where, Eval(exp, I) is the value returned by the evaluation of the expresion exp in the scenario I, and O2Fenv+(M) is the union of the set of formulas resulting from calling three auxiliary mappings, O2Fdata+(M), O2Finst+(I), and O2Fdef+(exp).