# OCL2FOL

OCL2FOL implements our mapping **ocl2fol** from OCL to first-order logic.

This mapping follows (but also corrects and extends) the mapping originally introduced in Clavel et al. 2009.

# Specification

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(*M*, *exp*) holds in every model of ocl2fol_th(*M*) U ocl2fol_def(*M*, *exp*).

# Current limitations

### Data models in Δ:

- Generalizations between classes are not allowed
- Attributes can only have one of the following types: String and Integer.
- Association-ends can only have multiplicity 0..*
- There must be one isUser-entity.

### OCL expressions in Η:

With respect to **types**:

- Only expressions of class types, Set- and Bag-types over class types, and Set- and Bag-types over String and Integer are allowed.

**operations**and

**iterators**:

- Operations on String are not allowed, except = and <>.
- Operations on Bag-types are not allowed, except ->asSet().

- oclIsUndefined() and ->oclIsUndefined() are not allowed.
- oclIsInvalid() and ->oclIsInvalid() are not allowed.
- ocIsTypeOf() and oclIsKindOf() are not allowed.
- oclAsType() is not allowed.
- asSet() is not allowed.

- ->size() is not allowed.
- ->excludesAll() is not allowed.
- min() and ->min() are not allowed.
- max() and ->max() are not allowed.
- abs() is not allowed.
- ->sum() is not allowed.
- ->union() is not allowed.
- ->intersection() is not allowed.
- ->-() is not allowed.
- ->symmetricDifference() is not allowed.

- ->one() is not allowed.
- ->isUnique() is not allowed.
- ->iterate() is not allowed.
- ->closure() is not allowed.
- let is not allowed.
- if_then_else is not allowed.

# Web application

Our mapping **ocl2fol** is available at:

http://www.actiongui.org/apps/ocl2fol/

#### User manual

##### From scratch:

1. Select the **DTM**-tab, and type-in an ActionGUI data model *M* in Δ.

2. Select the **OCL to FOL**-tab, and add as many OCL boolean expressions *exp*_{1},..., *exp*_{n} in Η as you want by (repeatedly) clicking on the **Add**-button and typing-in the desired expression *exp*_{i}.

Notice that you can always modify or remove OCL boolean expressions already typed-in by clicking on the buttons **Remove** and **Modify**.

3. Select an SMT solver (currently, either Z3 or Yices).

4. Generate the theory ocl2fol(*M*) U {ocl2fol_def(*M*, *exp_1*),...,ocl2fol_def(*M*, *exp_n*)} U {ocl2fol_th(*M*, *exp_1*),...,ocl2fol_th(*M*, *exp_n*)} with the syntax of the selected SMT solver.

##### From a stored project

An OCL2FOL **project** consists of a data model *M* in Δ and a set of OCL boolean expressions *exp*_{1},..., *exp*_{n} in Η.

To store the data model and OCL expressions that you have typed in the OCL2FOL web application as an OCL2FOL project, simply click on the button **Store** and download the generated XML file (by default, memento.xml) to your local disk.

To restore an OCL2FOL project, simply click on the button **Restore** and upload the project from your local disk.

# Examples

- Library. This project consists of the data model and the OCL expressions which are used as a running example in the original paper about OCL2FOL.

# FAQ

*Why do you restrict your "theorem" to instances (of data models) such that all relevant attributes are defined? What is the problem with undefined attributes?*

Consider the following very simple data model **Persons**:

entity Person isUser{

Integer age

}

Consider also the following OCL boolean expression **PersonsAge**:

not(Person.allInstances()->exists(p|p.age = 40))

and not(Person.allInstances()->forAll(p|p.age < 40 or p.age > 40))

The set of sentences ocl2fol_th(**Persons**) U ocl2fol_def(**Persons**, **PersonsAge**) U ocl2fol_sen(**PersonsAge**) that our mapping generates is clearly unsatisfactory, i.e., there does not exist any first-order model which can satisfy every sentence in this set.

Consider now an instance of **Persons** that only contains one object of type Person and suppose that this object has its attribute age undefined. Notice that, for this instance of **Persons**, *due to the OCL semantics for the undefined value, * the OCL boolean expression **PersonsAge** will evaluate to true!

Therefore, we need to restrict our "theorem" to instances (of data models) such that all relevant attributes are defined. This restriction was not explicitly stated in our original paper Clavel et al. 2009.

We are currently working on a new mapping that will (try to) take into consideration the OCL semantics for the undefined value.