Headline

Class diagrams with Language:OCL based on Technology:USE

Motivation

Some of the features involve constraints. Notably, Feature:Ranking imposes a constraint on the salary values. In a Language:UML-based contribution, such constraints may be modeled with the help of Language:OCL.

Illustration

When using USE (with OCL), a class diagram including all OCL constraints is represented in a textual syntax. The USE IDE visualizes this textual syntax when necessary. Here is how invariants are attached to a class:

context Company
    inv needs_a_name: self.Name.size() > 0
    inv comply_ranked_salary: self.complyRankedSalary()

In the class Company, the corresponding invariant is specified as follows:

class Company
attributes
    Name : String
operations
    total() : Real =
        self.departments->collect(d : Department | d.total())->sum()
    cut()
    complyRankedSalary() : Boolean =
        self.departments->forAll(d : Department | d.complyRankedSalary())
    containsEmployee(e: Employee) : Boolean =
        self.departments->forAll(d : Department | d.containsEmployee(e))
    containsDepartment(dep: Department) : Boolean =
        self.departments->includes(dep) or
        self.departments->one(d : Department | d <> dep and d.containsDepartment(dep))

    addDepartment(d : Department)
    removeDepartment(d : Department)
end

Thus, complyRankedSalary is delegated to the individual departments. A company complies with the ranking constraints when all its departments comply with it. We use OCL's universal quantification to this end.

In the class Department, the corresponding invariant is specified as follows:

    complyRankedSalary() : Boolean =
        self.employees->sortedBy(e : Employee | e.Salary)->last().oclIsTypeOf(Manager) and
        self.subdepartments->forAll(d : Department | d.complyRankedSalaryRec(self.employees->sortedBy(e : Employee | e.Salary)->first().Salary))

    complyRankedSalaryRec(max : Real) : Boolean =
        self.employees->sortedBy(e : Employee | e.Salary)->last().oclIsTypeOf(Manager) and
        self.employees->sortedBy(e : Employee | e.Salary)->last().Salary < max and
        self.subdepartments->forAll(d : Department | d.complyRankedSalaryRec(self.employees->sortedBy(e : Employee | e.Salary)->first().Salary))

The first condition of complyRankedSalary establishes that, when sorting employees of a department by salary, then the last employee, i.e., the employee with the maximum salary, is the manager of the given department. The second condition of complyRankedSalary, which ultimately invokes complyRankedSalaryRec, checks compliance for the subdepartments while passing in the minimum salary from the given department as the upper bound for salaries in the subdepartments. Finally, the recursive condition complyRankedSalaryRec is very similar to complyRankedSalary, except that it also enforces the received maximum as a bound.

Usage

Download and install

Download the contribution.

GitHub URL: https://github.com/cEhlen/OCL101Companies

Clone URL: git@github.com:cEhlen/OCL101Companies.git

Download and install USE OCL.

Download link: http://useocl.sourceforge.net/w/index.php/Main_Page#Download

At the time of writing, this meant to download a file "use-4.1.1.tar.gz".

Just unpack the file in a location convenient for software.

Running USE

Run the program.

In directory "bin", there are scripts for running the program on different platforms.

This will give you a terminal window and the USE window.

Type the following commands into the terminal window.

use> open /path/to/101companies.use
use> open testdata

Here "/path/to/" is the path to the GitHub directory that was cloned earlier.

These commands open the specification and load a sample company into memory.

The class and object diagrams can be rearanged and should look like the following images:

Using USE

Checking Class Invariants

The ⚡ button ("Create class invariant view") checks all invariants and shows the output. You can doubleclick every constraint and see the stacktrace of the execution.

Pre- And Postconditions

The testdata file also does all pre and postcondition checks for all operations executed. If you take a look at the output in the terminal window, you should find something like

testdata> !openter AcmeCorp addDepartment(ResearchDep)
precondition `department_not_in_company' is true
precondition `department_has_no_company' is true
testdata> !insert (ResearchDep, AcmeCorp) into DepartmentOf
testdata> !opexit
postcondition `department_has_company' is true
postcondition `department_was_added' is true

Here we enter the operation `addDerpartment` for our company. Then we execute the commands needed to execute the operation and exit the operation. USE checks each precondition when entering the operation and checks every postcondition when exiting. Here everything worked just fine and the department was added to the company.

You can type these commands into the terminal window yourself. Try running

use> !openter EmpKarl cut()
<<precondition check>>
use> !set EmpKarl.Salary := 1172.5
use> !opexit
<<postcondition check>>

This should execute sucessfully. But since Karl is the manager of the Development 1.1 department, the company does not comply to the ranked salary constraint anymore. Press ⚡ button ("Create class invariant view") to find the problem. Select the violated constraints to see the stack trace.