At present, the OCL language includes two constants, null and invalid, to represent undefinedness. This effectively turns OCL into a four-valued logic. It makes also problematic its mapping to first-order logic and, as a consequence, hinders the use of first-order automated-reasoning tools for OCL reasoning. We address this problem and propose a solution, grounded on the same principles underlying OCL2FOL, in order to cope with undefinedness in OCL.
In the past decade, there has been a plethora of proposals to map OCL [11] into different formalisms for which reasoning tools may be readily available. By choosing a particular formalism each proposal commits to a different trade off between expressiveness and termination, automation, or completeness (see [12,5] and references). In particular, most of these proposals have not considered the OCL language parts that deal with undefinedness or generate it: basically, the constants null and invalid,1 the type-casting operator, the division operator, and the operators any, oclIsUndefined and oclIsInvalid. By doing so, these proposals try to turn OCL into a two-valued logic, so that it can be more easily mapped to different formalisms for which reasoning tools already exist. Notable exceptions to this trend are [3,4,2,10] though [2,10] only deals with null.
In [6] we proposed a mapping from OCL to first-order logic, and we implemented it in a tool called OCL2FOL. This mapping supports the direct use of SMT solvers (e.g., Z3 [7] or Yices [8]) to check the satisfiability of OCL expressions, but under specific restrictions both on the expressions that were allowed and on the instances of data models that were KuhlmannG12Models checked. 2 Not surprisingly, some of these restrictions were imposed to avoid the problem of coping with undefinedness in OCL. In particular, i) OCL2FOL only considers instances where all attributes are defined, and ii) it does not allow expressions containing operators that can generate undefined values. However, after experimenting with OCL2FOL, we have come to realize that these restrictions impose severe limitations on the applicability of the tool (and we conjecture that similar limitations will apply as well to other methodologies that are not prepared to deal with undefinedness).
In this paper we propose OCL2FOL + which, although grounded on the same principles underlying OCL2FOL, is designed to overcome the limitations of the latter with regard to undefinedness in OCL. 3 Let us explain the key difference in a nutshell. Under the aforementioned restrictions i) and ii), a Boolean OCL expression can only evaluate to either true or false. Thus, to reason in this context using Boolean OCL expressions it is sufficient to define a mapping that formalizes when a Boolean OCL expressions evaluates to true. This is precisely what we did in OCL2FOL. However, in the presence of undefinedness, Boolean OCL expressions can also evaluate to null or invalid. To cope with this fact, we now define in OCL2FOL + four different mappings which formalize, respectively, when a Boolean OCL expression evaluates to true, when to false, when to null, and when to invalid.
Organization. First, in Section 2, we recall the basic principles underlying the mapping from OCL to first-order logic which is implemented in OCL2FOL. Then, in Section 3, we discuss the key ideas behind the four mappings which are implemented in OCL2FOL + for coping with undefinedness in OCL. Next, in Section 4, we report on the status of OCL2FOL + , and on some experiments that we have carried out with this tool. Finally, we draw conclusions in Section 5.
In [6] we define a mapping, called OCL2FOL, from a subset of OCL4 into first-order logic. For the sake of space, we will refer here to this mapping as O2F * . The key property of O2F * is the following: Let M be a data model, let I be an instance of M (where all attributes values are defined) and let exp be a Boolean OCL expression (within the O2F * 's range), whose context is also M. Then, Eval(exp,I) = true ⇐⇒ O2F env (M, I, exp) | = O2F * (exp) (1) where Eval(exp,I) is the value returned by the evaluation of the expression exp for the instance I, and O2F env (M, I, exp) is the union of the set of formulas resulting from calling three auxiliary mappings, namely, O2F data , O2F inst , and O2F def , on, respectively, the data model M, the instance I, and the expression exp. That is,
Next, we briefly discuss these three auxiliary mappings, and then the key mapping O2F * . But before, consider the following remark, whose correctness is based on the correctness of (1) and on the assumption that the evaluation of exp cannot possible result in null or invalid. To simplify the presentation, we do not consider here class inheritance, multi-valued attributes, or association-ends with multiplicities different from *.
Classes are represented by predicates. In particular, for every two classes C and C in M, C C , the set O2F data (M) includes the following formula:
Then, attributes are represented as functions. Finally, association-ends are represented as binary predicates. In particular, for every association between two classes C and C , with association-ends assoc and assoc , the set O2F data (M) includes the formulas:
O2F inst (I): Mapping instances I Objects are represented by constants. In particular, for every object o in I of a class C, the set O2F inst (I) includes the following formula:
Then, attributes values are represented by equalities, which all-together define the corresponding functions. In particular, for every object o in I, if v is the value of its attribute attr, then the set O2F inst (I) includes the following equality:
• attr(o) = v Finally, links between objects are represented by formulas, which all-together define the corresponding predicates. In particular, for every two objects o and o in I, if o is linked to o through o's association-end assoc, then the set O2F inst (M) includes the following formula:
The OCL language includes operators (e.g., collect or select, but also union or including) that define new collections, without naming them, using a certain property. We represent these new collections by new predicates. In particular, for every sub-expression of exp which defines a new collection, the set O2F def (exp) includes the formula that formalizes that for every element for which the new predicate holds it also holds the property which defines the new collection. Example 1 below illustrates, among other things, this essential feature of our mapping from OCL to first-order logic.
There are also operators in OCL (e.g., max or any) that refer to objects, without naming it, using also a certain property. We represent these objects by new constants. In particular, for every sub-expression of exp that refers, without naming it, to an object using a property, then set O2F def (exp) includes the formula that formalizes that the aforementioned property holds for the element referred to by the new constant.
The map O2F * is defined recursively over the structure of OCL expressions, according to the following principles: First, each expression of the form C.allInstances() is translated by a predicate formula whose predicate is the one representing the class C. Second, each expression of type Boolean whose root symbol (the one at the root of the tree representing the expression) is not, and, or, implies, xor, =, >, <, ≤, ≥, forAll, exists, one, isUnique, isEmpty, notEmpty, includes, excludes, includesAll, excludesAll is translated into a formula which mirror its logical structure. Third, each expression of type Integer whose root symbol is +, −, * is translated by the corresponding functional expression. Fourth, each expression of type Set whose root symbol is select, reject, including, excluding, union, intersection, collect (followed by asSet) is translated by a predicate formula, whose predicate's definition is generated using O2F def . Finally, each expression of type Integer whose root symbol is max or min (over collections) is translated by a constant, whose definition is generated using O2F def .
The recursive definition of O2F * is rather technical, and we shall refer to [6,1] for further details. These technicalities are mainly due to the fact that, in order to capture the semantics of a number of OCL operators (including the iterator operators, but also others) we introduce fresh logical variables, which are then passed on to the subsequent recursive calls and are used when translating the arguments of these operators. This and other features of the mapping from OCL to first-order logic which is implemented in OCL2FOL are illustrated by the following example.
Example 1. Consider a simple data model Persons containing just one class Person, with one attribute age of type Integer and a self-association whose association-ends are friendsOf (x is a friend of y) and friendTo (y is considered a friend by x).
Let exp be Person.allInstances()→notEmpty(). Then, O2F * (exp) is the formula: ∃(x)(Person(x)) where Person is the predicate that represents the class Person and x is a logical variable introduced as part of the mapping of the operator notEmpty. Now, let exp be Person.allInstances()→exists(p|p.age ≤ 18). Then, O2F * (exp) is the following formula: ∃(x)(Person(x) ∧ age(x) ≤ 18) where age is the function that represents the attribute age and x is a logical variable introduced as part of the mapping of the operator exists.
Also, let exp be Person.allInstances()→select(p|p.age > 18) →isEmpty(). Then, O2F * (exp) is the following formula: ∀(x)(¬Select#1(x)) where x is a logical variable introduced as part of the mapping of the operator isEmpty and Select#1 is the predicate that represents the collection defined by the expression Person.allInstances()→select(p|p.age > 18). The predicate Select#1 is, in turn, defined, using the mapping O2F def , by the following formula: ∀(x)(Select#1(x) ⇔ (Person(x) ∧ age(x) > 18)) Finally, let exp be Person.allInstances()→collect(p|p.friendsOf)→asSet()→not-Empty(). Then, O2F * (exp) is the following formula:
where x is a logical variable introduced as part of the mapping of the operator notEmpty and Collect#1 is the predicate that represents the collection defined by the expression Person.allInstances()→collect(p|p.friendsOf)→asSet(). The predicate Collect#1 is, in turn, defined, using the mapping O2F def , by the following formula: ∀(x)(Collect#1(x) ⇔ ∃(y)(Person(y) ∧ friendsOf(y, x)) where friendsOf is the predicate that represents the association-end friendsOf.
In a nutshell, the problem of undefinedness in OCL when trying to use existing firstorder logic reasoning tools for OCL reasoning is the problem of mapping a four-valued logic (true, false, null, and invalid) a two-valued logic (true and false). In general, when evaluating a Boolean OCL expression for an instance of a data model, the result can be either true, false, null or invalid. However, when interpreting a formula in a first-order model, the result can only be true or false. In other words, in the presence of undefinedness, Remark 1 does not hold.
To cope with undefinedness while at the same time being able to use SMT solvers, as we did in OCL2FOL, to automatically carry out OCL reasoning, our solution consists on defining four mappings, namely, O2F true , O2F false , O2F null , and O2F inval , such that the following holds: Let M be a data model, let I be an instance of M (where now not all attributes values need to be defined), and let exp be a Boolean OCL expression whose context is M (within the O2F * 's range, extended now to include expressions built with the type-casting operators, the division operator, and the operators any, oclIsUndefined, and oclIsInvalid). where Eval(exp,I) is the value returned by the evaluation of the expression exp for the instance I, and O2F env+ (M, I, exp) is the union of the set of formulas resulting from calling three auxiliary mappings, namely, O2F data+ , O2F inst+ , and O2F def+ , on, respectively, the data model M, the instance I, and the expression exp. As their names suggest, these three mappings are extensions of the mappings O2F data , O2F inst , and O2F def . That is, O2F env+ (M, I, exp) = O2F data+ (M) ∪ O2F inst+ (I) ∪ O2F def+ (exp) Next, we briefly discuss the content of these extensions, and afterwards the four key mappings O2F true , O2F false , O2F null , and O2F inval .
The values null or invalid are represented, respectively, by the constants null and invalid. Moreover, we introduce two unary predicates IsNull and IsInvalid, to represent when an element is null or invalid, and we add to the set O2F data+ (M) the following formula:
• IsNull(null) ∧ ¬IsInvalid(null) ∧ ¬IsNull(invalid) ∧ IsInvalid(invalid) Objects are neither null nor invalid. 5 Therefore, for every class C in M, the set O2F data+ (M) contains the following additional formula:
O2F inst+ (I): Mapping instances I Attributes values may be undefined. Thus, for every object o in I, the value of its attribute attr is undefined, then the set O2F inst+ (I) includes the following equality:
• attr(o) = null On the other hand, attributes values may be defined. Thus, for every object o in I, if v is the (defined) value of its attribute attr, then the set O2F inst+ (I) includes the formula:
O2F def+ (exp): Mapping definitions in expressions exp Literals of primitive types are also neither null nor invalid. Thus, for every literal l in the given expression exp, the set O2F def+ (exp) contains the following additional formula:
Mapping expressions (aware of null and invalid)
For the sake of space limitation, we shall not provide here the full recursive definitions of our four mappings O2F true , O2F false , O2F null , O2F inval . Instead, we illustrate the main ideas using examples. In particular, since the new mappings follow the same principles than our original mapping O2F * , we use as examples the same expressions that we used in Example 1.
According to the OCL's semantics, if a collection contains invalid, the collection itself evaluates to invalid. Furthermore, for every operator, except of course oclIsInvalid and oclIsUndefined, if invalid happens to be passed as one of its arguments, the result is invalid. We now take these facts into account when mapping operators on collection, as shown in the following example. Notice, in particular, that we do not "reduce" a collection containing invalid to invalid, but instead we "keep" it in that collection. Then, when formalizing the semantics of operators on collections, we "check" if the given collections may contain invalid, and proceed accordingly.
Example 2. Let exp be Person.allInstances()→notEmpty().
Notice that, in the logical context provided by O2F env+ , some of the above expressions can be simplified. For example, ∀(x)(Person(x) ⇒ ¬IsInvalid(x)) can be reduced to , since objects are neither null nor invalid; for the same reason, ∃(x)(Person(x) ∧ IsInvalid(x)) can be reduced to ⊥. However, for the of clarity, we will not perform such optimizations in our examples. Now, if one of the elements in a disjunction is null, and the other element is neither true nor invalid, then the disjunction itself evaluates to null. Similarly, if one the elements in a disjunction is invalid, and the other element is not true, then the disjunction itself evaluates to invalid. Now, in the case of the operator ≤, if both arguments are null, then ≤ evaluates to true. But if only one of the arguments, but not the other, is null, then ≤ evaluates to invalid. And, if at least one element is invalid, or one argument is null, but not the other, then ≤ evaluates to invalid. We take these facts into account when mapping the iterator exists over collections and the operator ≤ between integers, as shown in the following examples.
Example 3. Let exp be Person.allInstances()→ exists(p|p.age ≤ 18). Next, recall that a collection resulting from the select-iterator contains every element of the source-collection for which the body evaluates to true. However, we now take into account that, if the source-collection contains invalid (and the same applies to the other iterator operators), then the resulting collection will also contain invalid, as shown in the following example.
Example 4. Let exp be Person.allInstances()→select(p|p.age > 18)→isEmpty().
O2F true (exp) = ∀(x)(¬Select#1(x)) ∧ ∀(x)(Select#1(x) ⇒ ¬IsInvalid(x))
where Select#1 is the predicate that represents the collection defined by the expression Person.allInstances()→select(p|p.age > 18). The predicate Select#1 is, in turn, defined by the following formula:
Finally, recall that oclIsUndefined returns true when its argument is either null or invalid, and false otherwise. Also, recall that the any-iterator returns null if no element in the source-collection satisfies the given property. As expected, if the source-collection contains invalid, the any-iterator also returns invalid. We now take into account all these three facts, as shown in the following example:
4 Tool support and case study
We have implemented our mappings in a tool, called OCL2FOL + [1]. OCL2FOL + takes as input a data model M (the context), a set of Boolean OCL expressions exp 1 , . . . , exp n (the hypothesis), a Boolean OCL expression exp n+1 (the assertion), and one of the following keywords (the type): true, false, null, inval. From the given input, the
To validate OCL2FOL + we have carried out a number of experiments. In particular, each column in Table 1 shows the result of checking, using Z3, the satisfiability of the set of formulas that results from calling OCL2FOL + with Persons (context), the empty set (hypothesis) and the conjunction of some formulas taken from Figure 1 plus the type true (assertion).
We have addressed the problem of coping with undefinedness in OCL while at the same time being able to use SMT solvers (e.g., Z3 and Yices) to automatically carry out OCL reasoning. Our solution follows the same principles underlying OCL2FOL, but consists now of four mappings which formalize, respectively, when an expression evaluates to true, when to false, when to null, and when to invalid. Our solution also differs from [3,4], since we pursue different goals. In particular, while we are able to support automated OCL reasoning, we can only cover a subset of OCL. On the other hand, the solution presented in [3,4], although it scovers the full OCL language, it can only provide interactive theorem-proving capabilities. As part of this work, we have also implemented our four mappings in a tool called OCL2FOL + [1] , and we have applied this tool for reasoning about OCL expressions in the presence of undefinedness. For this case study we have used a non-trivial benchmark that we would like to propose as an extension of [9], following their invitation to provide scenarios which are not currently covered: in particular, in their own words, "intensive use of the full semantics of OCL (like the undefined value or collection semantics); this poses a challenge for the lifting to two-valued logics."
Our future work will follow two main directions. On the one hand, we want to formally prove that our four mappings are correct with respect to the OCL semantics; unfortunately, the OCL semantics for undefinedness has been, in the past, in a constant state of flux. On the other hand, we want to apply OCL2FOL + for analyzing ActionGUI models [1], since they contain non-trivial Boolean OCL expressions which should never evaluate to null or invalid: e.g., authorization constraints in permissions or conditions in if-then-else statements (which are both expected to always evaluate to either true or false), and arguments in actions (which, when referring to the object upon which an action is to be executed, are expected to never evaluate to null or invalid).
Acknowledgements. We kindly thank Achim Brucker and Marco Guarnieri for our very helpful discussions on the semantics of OCL undefinedness, and we also thank our anonymous reviewers for their insightful comments and suggestions. This work is partially supported by the EU FP7-ICT Project "NESSoS: Network of Excellence on Engineering Secure Future Internet Software Services and Systems" (256980) by the Spanish Ministry of Science and Innovation Project "DESAFIOS-10" (TIN2009-14599-C03-01), and by Comunidad de Madrid Program "PROMETIDOS-CM" (S2009TIC-1465).