OCL2MSFOL: A mapping from OCL constraints to Many-sorted First-order Logic

OCL2MSFOL is a pure Java application that generates a Many-Sorted First-Order Logic (MSFOL) theory from an Object Constraint Language (OCL) constraint with an underlying contextual model. The mapping is strictly based on the work of Carolina Dania et. al. at IMDEA Research Institute, Madrid, Spain. The detail of the mapping definition can be reviewed here.

OCL works with a four-value logic: true, false, null and invalid. While the first two values are understood universally, the last two represent undefinedness: null represents unknown or undefined value whereas invalid represents an error or exception. Given an OCL constraint (represented as a string) and its contextual model (represented as a JSON file), OCL2MSFOL generates a complete FOL theory in SMT-LIB2 language as a text file.

Supported language and features:

There are four modes that can be chosen from: TRUE, FALSE, NULL and INVALID. Each model corresponds to a different theory which can be interpreted differently. For example, given an OCL expression e, using the application with mode TRUE generates a MSFOL theory that defines scenarios in which evaluating e returns true.

Please be aware that neither the mapping definition nor the implementation is complete. The following items highlight the supported subset of OCL:

• literal: Boolean, Integer, String.
  • Boolean: true, false.
  • Integer: ..., -1, 0, 1, ...
  • String: "a string", ...
• predefined variables of permitted types.
  • caller, self, user, ...
• datamodel's attributes and association-ends.
  • user.age, user.accounts, ...
• datamodel classes's allInstances().
  • class.allInstances()
• logical operations: not, and, or, implies.
• comparison operations =, <, <=, >, >=, <>.
• collection's operations: isEmpty(), notEmpty(), isUnique(), forAll(), exists(), collect(), select().
• undefinedness opeartions: oclIsUndefined(), oclIsInvalid().

How to use

Requirements:

• (required) Maven 3 and Java 1.8 (or higher).
• (submodule) datamodel - branch: OCL2MSFOL.
• (submodule) JavaOCL submodule - branch: master.

The submodules will be automatically updates using Git commands as in the guideline.

Quick guideline:

git clone https://github.com/npbhoang/OCL2MSFOL.git
git submodule update --init --recursive

Have a quick look at the Runner.java class for a quick guideline.

Some examples:

Below provides a few OCL expression as examples:

//      Case 1: true
        String inv = "true";
        
//      Case 2: caller.students->isEmpty
        OCL2MSFOL.putAdhocContextualSet("caller", "Lecturer");
        String inv = "caller.students->isEmpty()";
        
//      Case 3: self.age >= 18
        OCL2MSFOL.putAdhocContextualSet("self", "Student");
        String inv = "self.age >= 18";
        
//      Case 4: Student.allInstances()->forAll(s|s.lecturers->forAll(l|l.age > s.age))
        String inv = "Student.allInstances()->forAll(s|s.lecturers->forAll(l|l.age > s.age))";

//      Case 5: caller.age = self.age
        OCL2MSFOL.putAdhocContextualSet("self", "Student");
        OCL2MSFOL.putAdhocContextualSet("caller", "Lecturer");
        String inv = "caller.age = self.age";
        
//      Case 6: self.name = user
        OCL2MSFOL.putAdhocContextualSet("self", "Student");
        OCL2MSFOL.putAdhocContextualSet("user", "String");
        String inv = "self.name = user";