# OCL2FOL^{+}

OCL2FOL^{+} implements our mapping** ocl2fol ^{+}** from OCL to first-order logic.

The mapping **ocl2fol ^{+}** is available online. See here.

# 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 O2F^{env+}(*M*,*I*,*exp*) satisfy O2F^{true}(*exp*)

Eval(*exp*,*I*) = false if only if O2F^{env+}(*M*,*I*,*exp*) satisfy O2F^{false}(*exp*)

Eval(*exp*,*I*) = null if only if O2F^{env+}(*M*,*I*,*exp*) satisfy O2F^{null}(*exp*)

Eval(*exp*,*I*) = invalid if only if O2F^{env+}(*M*,*I*,*exp*) satisfy O2F^{inval}(*exp*)

where, Eval(*exp*, *I*) is the value returned by the evaluation of the expresion exp in the scenario I, and O2F^{env+}(*M*) is the union of the set of formulas resulting from calling three auxiliary mappings, O2F^{data+}(*M*), O2F^{inst+}(*I*), and O2F^{def+}(*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().
- ocIsTypeOf() and oclIsKindOf() are not allowed.
- oclAsType() is not allowed.
- asSet() is not allowed.
- ->size() is not allowed.
- min() and max() are not allowed.
- ->sum() 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

The tool OCL2FOL^{+} is available online here.

#### 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 (hypothesis) *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 the **OCL to FOL**-tab, and add an OCL expression *exp*_{n+1} (assertion) in H and select the type, by clicking the radio-bottom. Note that if you choose the types true and false, the OCL expression should be boolean.

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

5. Generate the environment O2F^{data+}(*M*) U {O2F^{true}(*exp _{1}*),...,O2F

^{true}(

*exp*)} U {O2F

_{n}^{def+}(

*exp*),...,O2F

_{1}^{def+}(

*M*,

*exp*

_{n}_{+1})} U {O2F

^{type}(exp

_{n+1})} with the syntax of the selected SMT solver.

##### From a stored project

An OCL2FOL^{+} **project** consists of a data model *M* in Δ (the context), a set of OCL boolean expressions *exp*_{1},..., *exp*_{n} in Η (the hipothesis), one OCL expression *exp*_{n+1 }in Η (the assertion) and a keyword (the type): *true*, *false*, *null*, *invalid*.

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

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).

entity Person {

Integer age

Set(Person) friendsOf oppositeTo friendsFor

Set(Person) friendsFor oppositeTo friendsOf

}

Consider the following set of assertions:

- Person.allInstances()->forAll(p|p.age>18)
- Person.allInstances()->exists(p|p.age<=18)
- Person.allInstances()->exists(p|p.age.oclIsUndefined())
- Person.allInstances()->exists(p|p.oclIsUndefined())
- Person.allInstances()->forAll(p|p.oclIsUndefined())
- Person.allInstances()->notEmpty()
- Person.allInstances()->collect(p|p.age)->asSet()->exists(a|a.oclIsUndefined())
- Person.allInstances()->any(p|p.age>16).oclIsUndefined()
- Person.allInstances()->any(p|p.age>16).age.oclIsInvalid()
- not(Person.allInstances()->any(p|p.age<16).age.oclIsInvalid())