## 5.5. OclIsTypeOf

### 5.5.1. Definition

```
constants OclIsTypeOf<OfclAny> :: 'α ⇒ Boolean ((-).oclIsTypeOf'(OclAny'))
```

```
constants OclIsTypeOf<Person> :: 'α ⇒ Boolean ((-).oclIsTypeOf'(Person'))
```

**def s (overloaded)** `OclIsTypeOf<OfclAny>-OfclAny`:

`(X::OfclAny) .oclIsTypeOf(OfclAny) ≡`

$$ (λτ. case X τ of \\ ⊥ ⇒ invalid τ \\ | ⊥_↓ ⇒ true τ (* invalid ?? *) \\ | mk<OfclAny> oid ⊥_↓ ⇒ true τ \\ | mk<OfclAny> oid ⊢_↓ ⇒ false τ) $$

**lemma** `OclIsTypeOf<OfclAny>-OfclAny`':

`(X::OfclAny) .oclIsTypeOf(OfclAny) =`

$$ (λ τ. if τ |= v X then (case X τ of \\ ⊥_↓ ⇒ true τ (* invalid ?? *) \\ | mk<OfclAny> oid ⊥_↓ ⇒ true τ \\ | mk<OfclAny> oid ⊢_↓ ⇒ false τ) \\ else invalid τ) $$

〈proof〉

**interpretation** `OclIsTypeOf<OfclAny>-OfclAny`:

`profile-mono-schemeV`

`OclIsTypeOf<OfclAny>::OfclAny ⇒ Boolean`

$$ λ X. (case X of \\ None_↓ ⇒ True_↓ (* invalid ?? *) \\ | mk<OfclAny> oid None_↓ ⇒ True_↓ \\ | mk<OfclAny> oid ⊢_↓ ⇒ False_↓) $$

〈proof〉

**def s (overloaded)** `OclIsTypeOf<OfclAny>-Person`:

`(X::Person) .oclIsTypeOf(Person) ≡`

$$ (λτ. case X τ of \\ ⊥ ⇒ invalid τ \\ | ⊥_↓ ⇒ true τ (* invalid ?? *) \\ | ⊢_↓ ⇒ false τ) $$

**def s (overloaded)** `OclIsTypeOf<Person>-OfclAny`:

`(X::OfclAny) .oclIsTypeOf(Person) ≡`

$$ (λτ. case X τ of \\ ⊥ ⇒ invalid τ \\ | ⊥_↓ ⇒ true τ \\ | mk<OfclAny> oid ⊥_↓ ⇒ false τ \\ | mk<OfclAny> oid ⊢_↓ ⇒ true τ) $$

**def s (overloaded)** `OclIsTypeOf<Person>-Person`:

`(X::Person) .oclIsTypeOf(Person) ≡`

$$ (λτ. case X τ of \\ ⊥ ⇒ invalid τ \\ | - ⇒ true τ) $$

### 5.5.2. Context Passing

**lemma** `cp-OclIsTypeOf<OfclAny>-Person-Person`: `cp P =⇒ cp(λX.(P(X::Person>::Person).oclIsTypeOf(OclAny))`

〈proof〉
lemma cp-OclIsTypeOfOclAny-OclAny-OclAny: cp P = cp(λX.(P(X::OclAny)::OclAny)).oclIsTypeOf(OclAny)
<proof>

lemma cp-OclIsTypeOfPerson-Person-Person: cp P = cp(λX.(P(X::Person)::Person)).oclIsTypeOf(Person)
<proof>

lemma cp-OclIsTypeOfPerson-OclAny-OclAny: cp P = cp(λX.(P(X::OclAny)::OclAny)).oclIsTypeOf(Person)
<proof>

lemma cp-OclIsTypeOfOclAny-Person-OclAny: cp P = cp(λX.(P(X::Person)::OclAny)).oclIsTypeOf(OclAny)
<proof>

lemma cp-OclIsTypeOfOclAny-OclAny-Person: cp P = cp(λX.(P(X::OclAny)::Person)).oclIsTypeOf(OclAny)
<proof>

lemma cp-OclIsTypeOfPerson-Person-OclAny: cp P = cp(λX.(P(X::Person)::OclAny)).oclIsTypeOf(Person)
<proof>

lemma cp-OclIsTypeOfPerson-OclAny-Person: cp P = cp(λX.(P(X::OclAny)::Person)).oclIsTypeOf(Person)
<proof>

lemmas [simp] =

cp-OclIsTypeOfOclAny-Person-Person

cp-OclIsTypeOfOclAny-OclAny-OclAny

cp-OclIsTypeOfPerson-Person-Person

cp-OclIsTypeOfPerson-OclAny-OclAny

cp-OclIsTypeOfOclAny-Person-OclAny

cp-OclIsTypeOfOclAny-OclAny-Person

cp-OclIsTypeOfPerson-Person-OclAny

cp-OclIsTypeOfPerson-OclAny-Person

### 5.5.3. Execution with Invalid or Null as Argument

lemma OclIsTypeOfOclAny-OclAny-strict1[simp]:
(invalid::OclAny) .oclIsTypeOf(OclAny) = invalid
<proof>

lemma OclIsTypeOfOclAny-OclAny-strict2[simp]:
(null::OclAny) .oclIsTypeOf(OclAny) = true
<proof>

lemma OclIsTypeOfOclAny-Person-strict1[simp]:
(invalid::Person) .oclIsTypeOf(OclAny) = invalid
<proof>

lemma OclIsTypeOfOclAny-Person-strict2[simp]:
(null::Person) .oclIsTypeOf(OclAny) = true
<proof>

lemma OclIsTypeOfPerson-OclAny-strict1[simp]:
(invalid::OclAny) .oclIsTypeOf(Person) = invalid
<proof>

lemma OclIsTypeOfPerson-OclAny-strict2[simp]:
(null::OclAny) .oclIsTypeOf(Person) = true
<proof>

lemma OclIsTypeOfPerson-Person-strict1[simp]:
(invalid::Person) .oclIsTypeOf(Person) = invalid
<proof>

lemma OclIsTypeOfPerson-Person-strict2[simp]:
(null::Person) .oclIsTypeOf(Person) = true
<proof>
### 5.5.4. Up Down Casting

**lemma actualType-larger-staticType:**

assumes isdef: $\tau \models (\delta X)$

shows $\tau \models (X::Person) .oclIsTypeOf(OclAny) \triangleq \text{false}$
$\langle\text{proof}\rangle$

**lemma down-cast-type:**

assumes isOclAny: $\tau \models (X::OclAny) .oclIsTypeOf(OclAny)$

and non-null: $\tau \models (\delta X)$

shows $\tau \models (X .oclAsType(Person)) \triangleq \text{invalid}$
$\langle\text{proof}\rangle$

**lemma down-cast-type':**

assumes isOclAny: $\tau \models (X::OclAny) .oclIsTypeOf(OclAny)$

and non-null: $\tau \models (\delta X)$

shows $\tau \models \text{not } (v (X .oclAsType(Person)))$
$\langle\text{proof}\rangle$

**lemma up-down-cast:**

assumes isdef: $\tau \models (\delta X)$

shows $\tau \models ((X::Person) .oclAsType(OclAny) .oclAsType(Person) \triangleq X)$
$\langle\text{proof}\rangle$

**lemma up-down-cast-Person-OclAny-Person [simp]:**

shows $((X::Person) .oclAsType(OclAny) .oclAsType(Person) = X)$
$\langle\text{proof}\rangle$

**lemma up-down-cast-Person-OclAny-Person':**

assumes $\tau \models v X$

shows $\tau \models (((X :: Person) .oclAsType(OclAny) .oclAsType(Person)) \doteq X)$
$\langle\text{proof}\rangle$

**lemma up-down-cast-Person-OclAny-Person'':**

assumes $\tau \models v (X :: Person)$

shows $\tau \models (X .oclIsTypeOf(Person) \text{ implies } (X .oclAsType(OclAny) .oclAsType(Person)) \doteq X)$
$\langle\text{proof}\rangle$

## 5.6. OclIsKindOf

### 5.6.1. Definition

const's OclIsKindOf<OclAny> :: 'α ⇒ Boolean ((-).oclIsKindOf'(OclAny'))

const's OclIsKindOf<Person> :: 'α ⇒ Boolean ((-).oclIsKindOf'(Person'))

**defs (overloaded) OclIsKindOf<OclAny>-OclAny:**

$(X::OclAny) .oclIsKindOf(OclAny) \equiv$

$(\lambda\tau. \text{ case } X \quad \tau \text{ of}$

$\perp \Rightarrow \text{invalid } \tau$

$| \Rightarrow \text{true } \tau)$

**defs (overloaded) OclIsKindOf<OclAny>-Person:**

$(X::Person) .oclIsKindOf(OclAny) \equiv$

$(\lambda\tau. \text{ case } X \quad \tau \text{ of}$

$\perp \Rightarrow \text{invalid } \tau$

$| \Rightarrow \text{true } \tau)$
### `defs` (overloaded) `OclIsKindOfPerson`-`OclAny`:

$$ (X::OclAny) .oclIsKindOf(Person) \equiv (\lambda\tau. \text{case } X \tau \text{ of} \quad \begin{array}{l} \perp \Rightarrow \text{invalid } \tau \\ | \perp \perp \Rightarrow \text{true } \tau \\ | \perp mk_{OclAny} \text{oid } \perp \perp \Rightarrow \text{false } \tau \\ | \perp mk_{OclAny} \text{oid } \perp \perp \Rightarrow \text{true } \tau) \end{array} ) $$

### `defs` (overloaded) `OclIsKindOfPerson`-`Person`:

$$ (X::Person) .oclIsKindOf(Person) \equiv (\lambda\tau. \text{case } X \tau \text{ of} \quad \begin{array}{l} \perp \Rightarrow \text{invalid } \tau \\ | \Rightarrow \text{true } \tau \end{array} ) $$

## 5.6.2. Context Passing

lemma `cp-OclIsKindOfOclAny`-`Person`-`Person`: `cp P` = `cp(\lambda X.(P(X::Person>::Person).oclIsKindOf(OclAny))` ` proof`

lemma `cp-OclIsKindOfOclAny`-`OclAny`-`OclAny`: `cp P` = `cp(\lambda X.(P(X::OclAny>::OclAny).oclIsKindOf(OclAny))` ` proof`

lemma `cp-OclIsKindOfPerson`-`Person`-`Person`: `cp P` = `cp(\lambda X.(P(X::Person>::Person).oclIsKindOf(Person))` ` proof`

lemma `cp-OclIsKindOfPerson`-`OclAny`-`OclAny`: `cp P` = `cp(\lambda X.(P(X::OclAny>::OclAny).oclIsKindOf(Person))` ` proof`

lemma `cp-OclIsKindOfOclAny`-`Person`-`OclAny`: `cp P` = `cp(\lambda X.(P(X::Person>::OclAny).oclIsKindOf(OclAny))` ` proof`

lemma `cp-OclIsKindOfOclAny`-`OclAny`-`Person`: `cp P` = `cp(\lambda X.(P(X::OclAny>::Person).oclIsKindOf(OclAny))` ` proof`

lemma `cp-OclIsKindOfPerson`-`Person`-`OclAny`: `cp P` = `cp(\lambda X.(P(X::Person>::OclAny).oclIsKindOf(Person))` ` proof`

lemma `cp-OclIsKindOfPerson`-`OclAny`-`Person`: `cp P` = `cp(\lambda X.(P(X::OclAny>::Person).oclIsKindOf(Person))` ` proof`

### lemmas [simp] =
* `cp-OclIsKindOfOclAny`-`Person`-`Person`
* `cp-OclIsKindOfOclAny`-`OclAny`-`OclAny`
* `cp-OclIsKindOfPerson`-`Person`-`Person`
* `cp-OclIsKindOfPerson`-`OclAny`-`OclAny`

* `cp-OclIsKindOfOclAny`-`Person`-`OclAny`
* `cp-OclIsKindOfOclAny`-`OclAny`-`Person`
* `cp-OclIsKindOfPerson`-`Person`-`OclAny`
* `cp-OclIsKindOfPerson`-`OclAny`-`Person`

## 5.6.3. Execution with Invalid or Null as Argument

lemma `OclIsKindOfOclAny`-`OclAny`-`strict1`[simp] : `(invalid::OclAny) .oclIsKindOf(OclAny) = invalid` ` proof`

lemma `OclIsKindOfOclAny`-`OclAny`-`strict2`[simp] : `(null::OclAny) .oclIsKindOf(OclAny) = true` ` proof`

lemma `OclIsKindOfOclAny`-`Person`-`strict1`[simp] : `(invalid::Person) .oclIsKindOf(OclAny) = invalid` ` proof`

lemma `OclIsKindOfOclAny`-`Person`-`strict2`[simp] : `(null::Person) .oclIsKindOf(OclAny) = true`
〈proof〉

lemma OclIsKindOfPerson-OclAny-strict1 [simp]: (invalid::OclAny) .oclIsKindOf(Person) = invalid
<proof>

lemma OclIsKindOfPerson-OclAny-strict2 [simp]: (null::OclAny) .oclIsKindOf(Person) = true
<proof>

lemma OclIsKindOfPerson-Person-strict1 [simp]: (invalid::Person) .oclIsKindOf(Person) = invalid
<proof>

lemma OclIsKindOfPerson-Person-strict2 [simp]: (null::Person) .oclIsKindOf(Person) = true
<proof>

5.6.4. Up Down Casting

lemma actualKind-larger-staticKind:

assumes isdef: τ ::= (δ X)

shows
  τ ::= ((X::Person) .oclIsKindOf(OclAny) ⇄ true)

<proof>

lemma down-cast-kind:

assumes isOclAny: ¬ (τ ::= ((X::OclAny) .oclIsKindOf(Person)))

and non-null τ ::= (δ X)

shows
  τ ::= ((X .oclAsType(Person)) ⇄ invalid)

<proof>

5.7. OclAllInstances

To denote OCL-types occuring in OCL expressions syntactically—as, for example, as “argument” of
oclAllInstances()—we use the inverses of the injection functions into the object universes; we show that
this is sufficient “characterization.”

definition Person ≡ OclAsTypePerson-Å

definition OclAny ≡ OclAsTypeOclAny-Å

lemmas [simp] = Person-def OclAny-def

lemma OclAllInstances-genericOclAny-exec: OclAllInstances-generic pre-post OclAny =
(λτ. Abs-Set<base> ⊓ Some ' OclAny ' ran (heap (pre-post τ)) ⊔)
<proof>

lemma OclAllInstances-at-postOclAny-exec: OclAny .allInstances() =
(λτ. Abs-Set<base> ⊓ Some ' OclAny ' ran (heap (snd τ)) ⊔)
<proof>

lemma OclAllInstances-at-preOclAny-exec: OclAny .allInstances@pre() =
(λτ. Abs-Set<base> ⊓ Some ' OclAny ' ran (heap (fst τ)) ⊔)
<proof>

5.7.1. OclIsTypeOf

lemma OclAny-allInstances-generic-oclIsTypeOf OclAny 1:

assumes [simp]: ⋀x. pre-post (x, x) = x

shows ∃τ. (τ ::= ((OclAllInstances-generic pre-post OclAny) → ∀All<Set>(X|X .oclIsTypeOf(OclAny))))
<proof>

lemma OclAny-allInstances-at-post-oclIsTypeOf OclAny 1:

∃τ. (τ ::= (OclAny .allInstances() → ∀All<Set>(X|X .oclIsTypeOf(OclAny))))
<proof>

lemma OclAny-allInstances-at-pre-oclIsTypeOf OclAny 1:
∃τ. (τ |= (OclAny .allInstances@pre() -> forAllSet(X|X .oclIsTypeOf(OclAny))))
<proof>

lemma OclAny-allInstances-generic-oclIsTypeOf OclAny 2:

assumes [simp]: A x. pre-post (x, x) = x

shows ∃τ. (τ |= not ((OclAllInstances-generic pre-post OclAny) -> forAllSet(X|X .oclIsTypeOf(OclAny))))
<proof>

lemma OclAny-allInstances-at-post-oclIsTypeOf OclAny 2:

∃τ. (τ |= not (OclAny .allInstances() -> forAllSet(X|X .oclIsTypeOf(OclAny)))))
<proof>

lemma OclAny-allInstances-at-pre-oclIsTypeOf OclAny 2:

∃τ. (τ |= not (OclAny .allInstances@pre() -> forAllSet(X|X .oclIsTypeOf(OclAny)))))
<proof>

lemma Person-allInstances-generic-oclIsTypeOf Person :

τ |= ((OclAllInstances-generic pre-post Person) -> forAllSet(X|X .oclIsTypeOf(Person))))
<proof>

lemma Person-allInstances-at-post-oclIsTypeOf Person :

τ |= (Person .allInstances() -> forAllSet(X|X .oclIsTypeOf(Person)))
<proof>

lemma Person-allInstances-at-pre-oclIsTypeOf Person :

τ |= (Person .allInstances@pre() -> forAllSet(X|X .oclIsTypeOf(Person)))
<proof>

5.7.2. OclIsKindOf

lemma OclAny-allInstances-generic-oclIsKindOf OclAny :

τ |= ((OclAllInstances-generic pre-post OclAny) -> forAllSet(X|X .oclIsKindOf(OclAny)))
<proof>

lemma OclAny-allInstances-at-post-oclIsKindOf OclAny :

τ |= (OclAny .allInstances() -> forAllSet(X|X .oclIsKindOf(OclAny)))
<proof>

lemma OclAny-allInstances-at-pre-oclIsKindOf OclAny :

τ |= (OclAny .allInstances@pre() -> forAllSet(X|X .oclIsKindOf(OclAny)))
<proof>

lemma Person-allInstances-generic-oclIsKindOf OclAny :

τ |= ((OclAllInstances-generic pre-post Person) -> forAllSet(X|X .oclIsKindOf(OclAny)))
<proof>

lemma Person-allInstances-at-post-oclIsKindOf OclAny :

τ |= (Person .allInstances() -> forAllSet(X|X .oclIsKindOf(OclAny)))
<proof>

lemma Person-allInstances-at-pre-oclIsKindOf OclAny :

τ |= (Person .allInstances@pre() -> forAllSet(X|X .oclIsKindOf(OclAny)))
<proof>

lemma Person-allInstances-generic-oclIsKindOf Person :

τ |= ((OclAllInstances-generic pre-post Person) -> forAllSet(X|X .oclIsKindOf(Person))))
<proof>
**lemma Person-allInstances-at-post-ocIsKindOfPerson:**
$$ \tau \models (Person .allInstances() \rightarrow \text{forallAllSet}(X|X .ocIsKindOf(Person))) \\ \langle\text{proof}\rangle $$

**lemma Person-allInstances-at-pre-ocIsKindOfPerson:**
$$ \tau \models (Person .allInstances@pre() \rightarrow \text{forallAllSet}(X|X .ocIsKindOf(Person))) \\ \langle\text{proof}\rangle $$

## 5.8. The Accessors (any, boss, salary)

Should be generated entirely from a class-diagram.

### 5.8.1. Definition

**definition eval-extract** :: ('A, ('a::object) option option) val
⇒ (oid ⇒ ('A, 'c::null) val)
⇒ ('A, 'c::null) val

**where eval-extract** X f = (λ τ. case X τ of
⊥ ⇒ invalid τ (* exception propagation *)
| ⊥ ⊥ ⇒ invalid τ (* dereferencing null pointer *)
| ⊥ obj ⊥ ⇒ f (oid-of obj) τ)

**definition deref-oidPerson** :: (A state × A state ⇒ A state)
⇒ (typePerson ⇒ (A, 'c::null) val)
⇒ oid
⇒ (A, 'c::null) val

**where deref-oidPerson** fst-snd f oid = (λτ. case (heap (fst-snd τ)) oid of
| ⊥ inPerson obj ] ⇒ f obj τ
| - ⇒ invalid τ)

**definition deref-oidOclAny** :: (A state × A state ⇒ A state)
⇒ (typeOclAny ⇒ (A, 'c::null) val)
⇒ oid
⇒ (A, 'c::null) val

**where deref-oidOclAny** fst-snd f oid = (λτ. case (heap (fst-snd τ)) oid of
| ⊥ inOclAny obj ] ⇒ f obj τ
| - ⇒ invalid τ)

pointer undefined in state or not referencing a type conform object representation

**definition selectOclAny** A N Y f = (λ X. case X of
(mkOclAny - ⊥) ⇒ null
| (mkOclAny - ⊥ any]) ⇒ f (λx . ⊥ x ⊥) any)

**definition selectPerson** BOSS f = (λ X. case X of
(mkPerson - - ⊥) ⇒ null (* object contains null pointer *)
| (mkPerson - - ⊥ boss]) ⇒ f (λx . - ⊥ x ⊥) boss)

**definition selectPerson** S A L A R Y f = (λ X. case X of
(mkPerson - ⊥ -) ⇒ null
| (mkPerson - salary) -) ⇒ f (λx. - x) salary)

definition in-pre-state = fst

definition in-post-state = snd

definition reconst-basetype = (λ convert x. convert x)

definition dotOclAnyANY :: OclAny ⇒ - ((1(-).any) 50)

where (X).any = eval-extract X
(deref-oidOclAny in-post-state
(selectOclAnyANY
reconst-basetype))

definition dotPersonBOSS :: Person ⇒ Person ((1(-).boss) 50)

where (X).boss = eval-extract X
(deref-oidPerson in-post-state
(selectPersonBOSS
(deref-oidPerson in-post-state)))

definition dotPersonSALARY :: Person ⇒ Integer ((1(-).salary) 50)

where (X).salary = eval-extract X
(deref-oidPerson in-post-state
(selectPersonSALARY
reconst-basetype))

definition dotOclAnyANY-at-pre :: OclAny ⇒ - ((1(-).any@pre) 50)

where (X).any@pre = eval-extract X
(deref-oidOclAny in-pre-state
(selectOclAnyANY
reconst-basetype))

definition dotPersonBOSS-at-pre:: Person ⇒ Person ((1(-).boss@pre) 50)

where (X).boss@pre = eval-extract X
(deref-oidPerson in-pre-state
(selectPersonBOSS
(deref-oidPerson in-pre-state)))

definition dotPersonSALARY-at-pre:: Person ⇒ Integer ((1(-).salary@pre) 50)

where (X).salary@pre = eval-extract X
(deref-oidPerson in-pre-state
(selectPersonSALARY
reconst-basetype))

lemmas dot-accessor =

dotOclAnyANY-def

dotPersonBOSS-def

dotPersonSALARY-def

dotOclAnyANY-at-pre-def

dotPersonBOSS-at-pre-def

dotPersonSALARY-at-pre-def

5.8.2. Context Passing

lemmas [simp] = eval-extract-def

lemma cp-dotOclAnyANY: ((X).any) τ = ((λ-. X τ).any) τ 〈proof〉
lemma cp-dotPersonBOSS: ((X).boss) τ = ((λ-. X τ).boss) τ ⟨proof⟩

lemma cp-dotPersonSALARY: ((X).salary) τ = ((λ-. X τ).salary) τ ⟨proof⟩

lemma cp-dotOclAnyANY-at-pre: ((X).any@pre) τ = ((λ-. X τ).any@pre) τ ⟨proof⟩

lemma cp-dotPersonBOSS-at-pre: ((X).boss@pre) τ = ((λ-. X τ).boss@pre) τ ⟨proof⟩

lemma cp-dotPersonSALARY-at-pre: ((X).salary@pre) τ = ((λ-. X τ).salary@pre) τ ⟨proof⟩

lemmas cp-dotOclAnyANY-I [simp, intro!]=
cp-dotOclAnyANY[THEN allI[THEN allI],
of λ X -. X λ - τ. τ, THEN cpI1]

lemmas cp-dotOclAnyANY-at-pre-I [simp, intro!]=
cp-dotOclAnyANY-at-pre[THEN allI[THEN allI],
of λ X -. X λ - τ. τ, THEN cpI1]

lemmas cp-dotPersonBOSS-I [simp, intro!]=
cp-dotPersonBOSS[THEN allI[THEN allI],
of λ X -. X λ - τ. τ, THEN cpI1]

lemmas cp-dotPersonBOSS-at-pre-I [simp, intro!]=
cp-dotPersonBOSS-at-pre[THEN allI[THEN allI],
of λ X -. X λ - τ. τ, THEN cpI1]

lemmas cp-dotPersonSALARY-I [simp, intro!]=
cp-dotPersonSALARY[THEN allI[THEN allI],
of λ X -. X λ - τ. τ, THEN cpI1]

lemmas cp-dotPersonSALARY-at-pre-I [simp, intro!]=
cp-dotPersonSALARY-at-pre[THEN allI[THEN allI],
of λ X -. X λ - τ. τ, THEN cpI1]

### 5.8.3. Execution with Invalid or Null as Argument

lemma dotOclAnyANY-nullstrict [simp]: (null).any = invalid
⟨proof⟩

lemma dotOclAnyANY-at-pre-nullstrict [simp] : (null).any@pre = invalid
⟨proof⟩

lemma dotOclAnyANY-strict [simp] : (invalid).any = invalid
⟨proof⟩

lemma dotOclAnyANY-at-pre-strict [simp] : (invalid).any@pre = invalid
⟨proof⟩

lemma dotPersonBOSS-nullstrict [simp]: (null).boss = invalid
⟨proof⟩

lemma dotPersonBOSS-at-pre-nullstrict [simp] : (null).boss@pre = invalid
⟨proof⟩

lemma dotPersonBOSS-strict [simp] : (invalid).boss = invalid
⟨proof⟩

lemma dotPersonBOSS-at-pre-strict [simp] : (invalid).boss@pre = invalid
⟨proof⟩

lemma dotPersonSALARY-nullstrict [simp]: (null).salary = invalid
⟨proof⟩

lemma dotPersonSALARY-at-pre-nullstrict [simp] : (null).salary@pre = invalid
⟨proof⟩

lemma dotPersonSALARY-strict [simp] : (invalid).salary = invalid
⟨proof⟩

lemma dotPersonSALARY-at-pre-strict [simp] : (invalid).salary@pre = invalid
<figure><img src="image_16.png" /><figcaption>Figure 5.2.: (a) pre-state $\sigma_1$ and (b) post-state $\sigma'_1$.</figcaption></figure>

〈proof〉

### 5.8.4. Representation in States

lemma dotPersonBOSS-def-mono:τ |= δ(X .boss) ⇒ τ |= δ(X)
<proof>

lemma repr-boss:

assumes A : τ ::= δ(x .boss)

shows is-represented-in-state in-post-state (x .boss) Person τ
<proof>

lemma repr-bossX :

assumes A : τ ::= δ(x .boss)

shows τ ::= ((Person .allInstances()) -> includes$_{Set}$(x .boss))
<proof>

## 5.9. A Little Infra-structure on Example States

The example we are defining in this section comes from the figure 5.2.

definition OclInt1000 (1000) where OclInt1000 = (λ - . ⌢ 1000_)

definition OclInt1200 (1200) where OclInt1200 = (λ - . ⌢ 1200_)

definition OclInt1300 (1300) where OclInt1300 = (λ - . ⌢ 1300_)

definition OclInt1800 (1800) where OclInt1800 = (λ - . ⌢ 1800_)

definition OclInt2600 (2600) where OclInt2600 = (λ - . ⌢ 2600_)

definition OclInt2900 (2900) where OclInt2900 = (λ - . ⌢ 2900_)

definition OclInt3200 (3200) where OclInt3200 = (λ - . ⌢ 3200_)

definition OclInt3500 (3500) where OclInt3500 = (λ - . ⌢ 3500_)

definition oid0 ≡ 0

definition oid1 ≡ 1

definition oid2 ≡ 2

definition oid3 ≡ 3

definition oid4 ≡ 4

definition oid5 ≡ 5

definition oid6 ≡ 6

definition oid7 ≡ 7

definition oid8 ≡ 8

definition person1 ≡ mkPerson oid0 ⌢ 1300_ ⌢ oid1_

definition person2 ≡ mkPerson oid1 ⌢ 1800_ ⌢ oid1_

definition person3 ≡ mkPerson oid2 None None
definition person4 ≡ mkPerson oid3 ⌊2900⌋ None

definition person5 ≡ mkPerson oid4 ⌊3500⌋ None

definition person6 ≡ mkPerson oid5 ⌊2500⌋ ⌊oid6⌋

definition person7 ≡ mkOclAny oid6 ⌊(3200), ⌊oid6⌋⌋

definition person8 ≡ mkOclAny oid7 None

definition person9 ≡ mkPerson oid8 ⌊0⌋ None

definition

$$
\sigma_1 \equiv (\leftarrow \text{heap} = \begin{array}{@{}l@{}} \text{empty}(oid0 \mapsto \text{inPerson}(mk\text{Person }oid0 \lfloor 1000 \rfloor \lfloor oid1 \rfloor)) \\ (oid1 \mapsto \text{inPerson}(mk\text{Person }oid1 \lfloor 1200 \rfloor \text{ None})) \\ (*oid2*) \\ (oid3 \mapsto \text{inPerson}(mk\text{Person }oid3 \lfloor 2600 \rfloor \lfloor oid4 \rfloor)) \\ (oid4 \mapsto \text{inPerson }\text{person5}) \\ (oid5 \mapsto \text{inPerson}(mk\text{Person }oid5 \lfloor 2300 \rfloor \lfloor oid3 \rfloor)) \\ (*oid6*) \\ (*oid7*) \\ (oid8 \mapsto \text{inPerson }\text{person9}), \\ \text{assocs} = \text{empty} \end{array})
$$

definition

$$
\sigma_1' \equiv (\leftarrow \text{heap} = \begin{array}{@{}l@{}} \text{empty}(oid0 \mapsto \text{inPerson }\text{person1}) \\ (oid1 \mapsto \text{inPerson }\text{person2}) \\ (oid2 \mapsto \text{inPerson }\text{person3}) \\ (oid3 \mapsto \text{inPerson }\text{person4}) \\ (*oid4*) \\ (oid5 \mapsto \text{inPerson }\text{person6}) \\ (oid6 \mapsto \text{inOclAny }\text{person7}) \\ (oid7 \mapsto \text{inOclAny }\text{person8}) \\ (oid8 \mapsto \text{inPerson }\text{person9}), \\ \text{assocs} = \text{empty} \end{array})
$$

definition $\sigma_0 \equiv (\leftarrow \text{heap} = \text{empty}, \text{assocs} = \text{empty})$

lemma basic-τ-wff: WFF(σ₁,σ₁')
<proof>

lemma [simp,code-unfold]: dom (heap σ₁) = {oid0,oid1,(*,oid2*)oid3,oid4,oid5(*,oid6,oid7*),oid8}
<proof>

lemma [simp,code-unfold]: dom (heap σ₁') = {oid0,oid1,oid2,oid3,(*,oid4*)oid5,oid6,oid7,oid8}
<proof> definition $X_{Person1}$ :: Person ≡ λ - .$_{⊥}$ person1 $_{⊥}$

definition $X_{Person2}$ :: Person ≡ λ - .$_{⊥}$ person2 $_{⊥}$

definition $X_{Person3}$ :: Person ≡ λ - .$_{⊥}$ person3 $_{⊥}$

definition $X_{Person4}$ :: Person ≡ λ - .$_{⊥}$ person4 $_{⊥}$

definition $X_{Person5}$ :: Person ≡ λ - .$_{⊥}$ person5 $_{⊥}$

definition $X_{Person6}$ :: Person ≡ λ - .$_{⊥}$ person6 $_{⊥}$

definition $X_{Person7}$ :: OclAny ≡ λ - .$_{⊥}$ person7 $_{⊥}$

definition $X_{Person8}$ :: OclAny ≡ λ - .$_{⊥}$ person8 $_{⊥}$

definition $X_{Person9}$ :: Person ≡ λ - .$_{⊥}$ person9 $_{⊥}$

lemma [code-unfold]: ((x::Person) = y) = StrictRefEqObject x y <proof>

lemma [code-unfold]: ((x::OclAny) = y) = StrictRefEqObject x y <proof>

lemmas [simp,code-unfold] =
OclAsTypeOclAny-OclAny
OclAsTypeOclAny-Person
OclAsTypePerson-OclAny

OclAsTypePerson-Person

OclIsTypeOfOclAny-OclAny

OclIsTypeOfOclAny-Person

OclIsTypeOfPerson-OclAny

OclIsTypeOfPerson-Person

OclIsKindOfOclAny-OclAny

OclIsKindOfOclAny-Person

OclIsKindOfPerson-OclAny

OclIsKindOfPerson-PersonAssert $\bigwedge_{spre} (s_{pre}, \sigma_1') \models (X_{Person1} .salary \doteq 1300)$

Assert $\bigwedge_{spre} (s_{pre}, \sigma_1') \models (X_{Person1} .salary \doteq 1300)$

Assert $\bigwedge_{spost.} (\sigma_1, s_{post}) \models (X_{Person1} .salary@pre \doteq 1000)$

Assert $\bigwedge_{spost.} (\sigma_1, s_{post}) \models (X_{Person1} .salary@pre \prec> 1300)$

Assert $\bigwedge_{spre} (s_{pre}, \sigma_1') \models (X_{Person1} .boss \prec> X_{Person1})$

Assert $\bigwedge_{spre} (s_{pre}, \sigma_1') \models (X_{Person1} .boss .salary \doteq 1800)$

Assert $\bigwedge_{spre} (s_{pre}, \sigma_1') \models (X_{Person1} .boss .boss \prec> X_{Person1})$

Assert $\bigwedge_{spre} (s_{pre}, \sigma_1') \models (X_{Person1} .boss .boss \doteq X_{Person2})$

Assert $(\sigma_1, \sigma_1') \models (X_{Person1} .boss@pre .salary \doteq 1800)$

Assert $\bigwedge_{spost.} (\sigma_1, s_{post}) \models (X_{Person1} .boss@pre .salary@pre \doteq 1200)$

Assert $\bigwedge_{spost.} (\sigma_1, s_{post}) \models (X_{Person1} .boss@pre .salary@pre \prec> 1800)$

Assert $\bigwedge_{spost.} (\sigma_1, s_{post}) \models (X_{Person1} .boss@pre \doteq X_{Person2})$

Assert $(\sigma_1, \sigma_1') \models (X_{Person1} .boss@pre .boss \doteq X_{Person2})$

Assert $\bigwedge_{spost.} (\sigma_1, s_{post}) \models (X_{Person1} .boss@pre .boss@pre \doteq null)$

Assert $\bigwedge_{spost.} (\sigma_1, s_{post}) \models (\text{not}(v(X_{Person1} .boss@pre .boss@pre .boss@pre)))$

lemma $(\sigma_1, \sigma_1') \models (X_{Person1} .oclIsMaintained())$

⟨proof⟩

lemma $\bigwedge_{spre} s_{post.} (s_{pre}, s_{post}) \models ((X_{Person1} .oclAsType(OclAny) .oclAsType(Person)) \doteq X_{Person1})$

⟨proof⟩

Assert $\bigwedge_{spre} s_{post.} (s_{pre}, s_{post}) \models (X_{Person1} .oclIsTypeOf(Person))$

Assert $\bigwedge_{spre} s_{post.} (s_{pre}, s_{post}) \models \text{not}(X_{Person1} .oclIsTypeOf(OclAny))$

Assert $\bigwedge_{spost.} (s_{pre}, s_{post}) \models (X_{Person1} .oclIsKindOf(Person))$

Assert $\bigwedge_{spost.} (s_{pre}, s_{post}) \models (X_{Person1} .oclIsKindOf(OclAny))$

Assert $\bigwedge_{spre} s_{post.} (s_{pre}, s_{post}) \models \text{not}(X_{Person1} .oclAsType(OclAny) .oclIsTypeOf(OclAny))$

Assert $\bigwedge_{spre} (s_{pre}, \sigma_1') \models (X_{Person2} .salary \doteq 1800)$

Assert $\bigwedge_{spost.} (\sigma_1, s_{post}) \models (X_{Person2} .salary@pre \doteq 1200)$

Assert $\bigwedge_{spre} (s_{pre}, \sigma_1') \models (X_{Person2} .boss \doteq X_{Person2})$

Assert $(\sigma_1, \sigma_1') \models (X_{Person2} .boss .salary@pre \doteq 1200)$

Assert $(\sigma_1, \sigma_1') \models (X_{Person2} .boss .boss@pre \doteq null)$

Assert $\bigwedge_{spost.} (\sigma_1, s_{post}) \models (X_{Person2} .boss@pre \doteq null)$

Assert $\bigwedge_{spost.} (\sigma_1, s_{post}) \models (X_{Person2} .boss@pre \prec> X_{Person2})$

Assert $(\sigma_1, \sigma_1') \models (X_{Person2} .boss@pre \prec> (X_{Person2} .boss))$

Assert $\bigwedge_{spost.} (\sigma_1, s_{post}) \models \text{not}(v(X_{Person2} .boss@pre .boss))$

Assert $\bigwedge_{spost.} (\sigma_1, s_{post}) \models \text{not}(v(X_{Person2} .boss@pre .salary@pre))$

lemma $(\sigma_1, \sigma_1') \models (X_{Person2} .oclIsMaintained())$

⟨proof⟩

Assert $\bigwedge_{spre} (s_{pre}, \sigma_1') \models (X_{Person3} .salary \doteq null)$

Assert $\bigwedge_{spost.} (\sigma_1, s_{post}) \models \text{not}(v(X_{Person3} .salary@pre))$

Assert $\bigwedge_{spre} (s_{pre}, \sigma_1') \models (X_{Person3} .boss \doteq null)$

Assert $\bigwedge_{spre} (s_{pre}, \sigma_1') \models \text{not}(v(X_{Person3} .boss .salary))$

Assert $\bigwedge_{spost.} (\sigma_1, s_{post}) \models \text{not}(v(X_{Person3} .boss@pre))$
lemma (σ₁,σ₁') ::= (XPerson3 .oclIsNew())
(proof)

Assert spost. (σ₁, spost) ::= (XPerson4 .boss@pre ≜ XPerson5)

Assert (σ₁,σ₁') ::= not(v(XPerson4 .boss@pre .salary))

Assert spost. (σ₁, spost) ::= (XPerson4 .boss@pre .salary@pre ≜ 3500)

lemma (σ₁,σ₁') ::= (XPerson4 .oclIsMaintained())
(proof)

Assert spre . (spre,σ₁') ::= not(v(XPerson5 .salary))

Assert spost. (σ₁, spost) ::= (XPerson5 .salary@pre ≜ 3500)

Assert spre . (spre,σ₁') ::= not(v(XPerson5 .boss))

lemma (σ₁,σ₁') ::= (XPerson5 .oclIsDeleted())
(proof)

Assert spre . (spre,σ₁') ::= not(v(XPerson6 .boss .salary@pre))

Assert spost. (σ₁, spost) ::= (XPerson6 .boss@pre ≜ XPerson4)

Assert (σ₁,σ₁') ::= (XPerson6 .boss@pre .salary ≜ 2900)

Assert spost. (σ₁, spost) ::= (XPerson6 .boss@pre .salary@pre ≜ 2600)

Assert spost. (σ₁, spost) ::= (XPerson6 .boss@pre .boss@pre ≜ XPerson5)

lemma (σ₁,σ₁') ::= (XPerson6 .oclIsMaintained())
(proof)

Assert spre spost. (spre, spost) ::= v(XPerson7 .oclAsType(Person))

Assert spost. (σ₁, spost) ::= not(v(XPerson7 .oclAsType(Person) .boss@pre))

lemma spre spost. (spre, spost) ::= ((XPerson7 .oclAsType(Person) .oclAsType(OclAny) .oclAsType(Person))
    ≜ (XPerson7 .oclAsType(Person)))
(proof)
lemma (σ₁,σ₁') ::= (XPerson7 .oclIsNew())
(proof)

Assert spre spost. (spre, spost) ::= (XPerson8 <> XPerson7)
Assert spre spost. (spre, spost) ::= not(v(XPerson8 .oclAsType(Person)))
Assert spre spost. (spre, spost) ::= (XPerson8 .oclIsTypeOf(OclAny))
Assert spre spost. (spre, spost) ::= not(XPerson8 .oclIsTypeOf(Person))
Assert spre spost. (spre, spost) ::= not(XPerson8 .oclIsKindOf(Person))
Assert spre spost. (spre, spost) ::= (XPerson8 .oclIsKindOf(OclAny))

Assert spre spost. (spre, spost) ::= (XPerson8 <> XPerson7)

Assert spre spost. (spre, spost) ::= not(v(XPerson8 .oclAsType(Person)))

Assert spre spost. (spre, spost) ::= (XPerson8 .oclIsTypeOf(OclAny))

Assert spre spost. (spre, spost) ::= not(XPerson8 .oclIsTypeOf(Person))

Assert spre spost. (spre, spost) ::= not(XPerson8 .oclIsKindOf(Person))

Assert spre spost. (spre, spost) ::= (XPerson8 .oclIsKindOf(OclAny))

lemma σ-modifiedonly: (σ₁,σ₁') ::= (Set{ XPerson1 .oclAsType(OclAny) , XPerson2 .oclAsType(OclAny) (*, XPerson3 .oclAsType(OclAny)*) , XPerson4 .oclAsType(OclAny) (*, XPerson5 .oclAsType(OclAny)*) , XPerson6 .oclAsType(OclAny) (*, XPerson7 .oclAsType(OclAny)*) (*, XPerson8 .oclAsType(OclAny)*) (*, XPerson9 .oclAsType(OclAny)*)} --> oclIsModifiedOnly())
(proof)

lemma (σ₁,σ₁') ::= ((XPerson9 @pre (λx. ⊢ OclAsTypePerson-α x)) ≜ XPerson9)
(proof)
lemma $(\sigma_1, \sigma_1') \models ((X_{Person} \ @post (\lambda x. \lfloor OclAsType_{Person} - \mathfrak{A} x \rfloor)) \triangleq X_{Person} \ 9)$
<proof>

lemma $(\sigma_1, \sigma_1') \models ((((X_{Person} \ .oclAsType(\mathit{OclAny})) \ @pre (\lambda x. \lfloor \mathit{OclAsType}_{\mathit{OclAny}} - \mathfrak{A} x \rfloor)) \triangleq ((X_{Person} \ .oclAsType(\mathit{OclAny})) \ @post (\lambda x. \lfloor \mathit{OclAsType}_{\mathit{OclAny}} - \mathfrak{A} x \rfloor)))$
<proof>

lemma perm-$\sigma_1'$ : $\sigma_1' = (\emptyset, \text{heap} = \text{empty})$
($\text{oid8} \mapsto \text{inPerson } \text{person9}$)
($\text{oid7} \mapsto \text{inOclAny } \text{person8}$)
($\text{oid6} \mapsto \text{inOclAny } \text{person7}$)
($\text{oid5} \mapsto \text{inPerson } \text{person6}$)
($\text{*oid4*}$)
($\text{oid3} \mapsto \text{inPerson } \text{person4}$)
($\text{oid2} \mapsto \text{inPerson } \text{person3}$)
($\text{oid1} \mapsto \text{inPerson } \text{person2}$)
($\text{oid0} \mapsto \text{inPerson } \text{person1}$)
, $\text{assocs} = \text{assocs } \sigma_1'$)

<proof>

declare const-ss [simp]

lemma $\bigwedge \sigma_1$.
$(\sigma_1, \sigma_1') \models (\mathit{Person} .\mathit{allInstances}() \doteq \mathit{Set}\{ X_{\mathit{Person}1}, X_{\mathit{Person}2}, X_{\mathit{Person}3}, X_{\mathit{Person}4}(*, X_{\mathit{Person}5}*),$
$X_{\mathit{Person}6},$
$X_{\mathit{Person}7} .\mathit{oclAsType}(\mathit{Person})(*, X_{\mathit{Person}8}*), X_{\mathit{Person}9} \})$
<proof>

lemma $\bigwedge \sigma_1$.
$(\sigma_1, \sigma_1') \models (\mathit{OclAny} .\mathit{allInstances}() \doteq \mathit{Set}\{ X_{\mathit{Person}1} .\mathit{oclAsType}(\mathit{OclAny}), X_{\mathit{Person}2} .\mathit{oclAsType}(\mathit{OclAny}),$
$X_{\mathit{Person}3} .\mathit{oclAsType}(\mathit{OclAny}), X_{\mathit{Person}4} .\mathit{oclAsType}(\mathit{OclAny})$
$(*, X_{\mathit{Person}5}*), X_{\mathit{Person}6} .\mathit{oclAsType}(\mathit{OclAny}),$
$X_{\mathit{Person}7}, X_{\mathit{Person}8}, X_{\mathit{Person}9} .\mathit{oclAsType}(\mathit{OclAny}) \})$
<proof>

end

theory
Design-OCL

imports
Design-UML

begin

5.10. OCL Part: Invariant

These recursive predicates can be defined conservatively by greatest fix-point constructions—
automatically. See [4, 6] for details. For the purpose of this example, we state them as axioms here.

context Person
inv label : self boss <> null implies (self salary \<le>
((self boss) .salary))

definition Person-label<sub>inv</sub> :: Person ⇒ Boolean
**where**
Person-label<sub>inv</sub> (self)equiv
(self .boss <> null implies (self .salary < int ((self .boss) .salary))))

**definition** Person-label<sub>invATpre</sub> :: Person ⇒ Boolean

**where**
Person-label<sub>invATpre</sub> (self)equiv
(self .boss@pre <> null implies (self .salary@pre < int ((self .boss@pre) .salary@pre))))

**definition** Person-label<sub>globalinv</sub> :: Boolean

**where**
Person-label<sub>globalinv</sub>equiv (Person .allInstances() -> forAll<Set>(x | Person-label<sub>inv</sub> (x)) and
(Person .allInstances@pre() -> forAll<Set>(x | Person-label<sub>invATpre</sub> (x))))

**lemma** $\tau \models \delta (X .\mathit{boss}) \implies \tau \models \mathit{Person} .\mathit{allInstances}() \rightarrow \mathit{includes}_{\mathit{Set}}(X .\mathit{boss}) \wedge$
$\tau \models \mathit{Person} .\mathit{allInstances}() \rightarrow \mathit{includes}_{\mathit{Set}}(X)$
$\langle\mathit{proof}\rangle$

**lemma** REC-pre : $\tau \models Person\text{-}label_{globalinv}$
$\implies \tau \models Person \text{-}allInstances() \rightarrow includes_{Set}(X) (* X represented object in state *)$
$\implies \exists REC. \tau \models REC(X) \triangleq (Person\text{-}label_{inv}(X) \text{ and } (X \text{.boss} <> \text{null implies REC(X. boss)}))$
$\langle\mathit{proof}\rangle$

This allows to state a predicate:

**axiomatization** $inv_{Person\text{-}label}$ :: Person $\Rightarrow$ Boolean

**where** $inv_{Person\text{-}label\text{-def}}$:

($\tau \models Person \text{-}allInstances() \rightarrow includes_{Set}(self)$) $\implies$
($\tau \models (inv_{Person\text{-}label}(self) \triangleq (self \cdot boss <> \text{null implies}$
(self .salary < int ((self .boss) .salary)) and
$inv_{Person\text{-}label}(self \cdot boss))))$

**axiomatization** $inv_{Person\text{-}labelATpre}$ :: Person $\Rightarrow$ Boolean

**where** $inv_{Person\text{-}labelATpre\text{-def}}$:

($\tau \models Person \text{-}allInstances@pre() \rightarrow includes_{Set}(self)$) $\implies$
($\tau \models (inv_{Person\text{-}labelATpre}(self) \triangleq (self \cdot boss@pre <> \text{null implies}$
(self .salary@pre < int ((self .boss@pre) .salary@pre)) and
$inv_{Person\text{-}labelATpre}(self \cdot boss@pre))))$

**lemma** inv-1 :

($\tau \models Person \text{-}allInstances() \rightarrow includes_{Set}(self)$) $\implies$
($\tau \models inv_{Person\text{-}label}(self) = ((\tau \models (self \cdot boss <> \text{null})) \lor$
($\tau \models (self \cdot boss <> \text{null}) \land$
$\tau \models ((self .salary) < int (self .boss .salary)) \land$
$\tau \models (inv_{Person\text{-}label}(self .boss))))$)
$\langle\mathit{proof}\rangle$

**lemma** inv-2 :

($\tau \models Person \text{-}allInstances@pre() \rightarrow includes_{Set}(self)$) $\implies$
($\tau \models inv_{Person\text{-}labelATpre}(self) = ((\tau \models (self \cdot boss@pre <> \text{null})) \lor$
($\tau \models (self .boss@pre <> \text{null}) \land$
($\tau \models (self .boss@pre .salary@pre < int self .salary@pre)) \land$
($\tau \models (inv_{Person\text{-}labelATpre}(self .boss@pre)))))$)
$\langle\mathit{proof}\rangle$

A very first attempt to characterize the axiomatization by an inductive definition - this can not be
the last word since too weak (should be equality!)
coinductive inv :: Person ⇒ (A)st ⇒ bool where

$$
\begin{align*}
(\tau \models (\delta \ self)) &\implies ((\tau \models (self . boss \doteq null)) \lor \\
&\phantom{(\tau \models (self . boss \doteq null)) \lor } (\tau \models (self . boss <> null) \land (\tau \models (self . boss . salary \leq_{int} self . salary))) \land \\
&\phantom{(\tau \models (self . boss <> null) \land (\tau \models (self . boss . salary \leq_{int} self . salary))) \land } ((inv(self . boss))\tau ))) \\
&\implies (inv self \tau)
\end{align*}
$$

5.11. OCL Part: The Contract of a Recursive Query

This part is analogous to the Analysis Model and skipped here.

end
# Part II.

## Conclusion
<figure><img src="image_17.png" /></figure>
# 6. Conclusion

## 6.1. Lessons Learned and Contributions

We provided a typed and type-safe shallow embedding of the core of UML [30, 31] and OCL [32]. Shallow embedding means that types of OCL were mapped by the embedding one-to-one to types in Isabelle/HOL [27]. We followed the usual methodology to build up the theory uniquely by conservative extensions of all operators in a denotational style and to derive logical and algebraic (execution) rules from them; thus, we can guarantee the logical consistency of the library and instances of the class model construction. The class models were given a closed-world interpretation as object-oriented datatype theories, as long as it follows the described methodology.<fnref n="1" /> Moreover, all derived execution rules are by construction type-safe (which would be an issue, if we had chosen to use an object universe construction in Zermelo-Fraenkel set theory as an alternative approach to subtyping.). In more detail, our theory gives answers and concrete solutions to a number of open major issues for the UML/OCL standardization:

1. the role of the two exception elements invalid and null, the former usually assuming strict evaluation while the latter ruled by non-strict evaluation.

2. the functioning of the resulting four-valued logic, together with safe rules (for example foundation9 - foundation12 in Section 2.1.5) that allow a reduction to two-valued reasoning as required for many automated provers. The resulting logic still enjoys the rules of a strong Kleene Logic in the spirit of the Amsterdam Manifesto [18].

3. the complicated life resulting from the two necessary equalities: the standard's "strict weak referential equality" as default (written _ =_ throughout this document) and the strong equality (written _ ≜ _), which follows the logical Leibniz principle that "equals can be replaced by equals." Which is not necessarily the case if invalid or objects of different states are involved.

4. a type-safe representation of objects and a clarification of the old idea of a one-to-one correspondence between object representations and object-id's, which became a state invariant.

5. a simple concept of state-framing via the novel operator _->oclIsModifiedOnly() and its consequences for strong and weak equality.

6. a semantic view on subtyping clarifying the role of static and dynamic type (aka *apparent* and *actual* type in Java terminology), and its consequences for casts, dynamic type-tests, and static types.

7. a semantic view on path expressions, that clarify the role of invalid and null as well as the tricky issues related to de-referentiation in pre- and post state.

8. an optional extension of the OCL semantics by *infinite* sets that provide means to represent "the set of potential objects or values" to state properties over them (this will be an important feature if OCL is intended to become a full-blown code annotation language in the spirit of JML [25] for semi-automated code verification, and has been considered desirable in the Aachen Meeting [14]).

<footnote n="1">¹Our two examples of Employee_AnalysisModel and Employee_DesignModel (see Chapter 4 and Figure 0.3.8 as well as Chapter 5 and Figure 0.3.8) sketch how this construction can be captured by an automated process; its implementation is described elsewhere.</footnote>
Moreover, we managed to make our theory in large parts executable, which allowed us to include me-
chanically checked value-statements that capture numerous corner-cases relevant for OCL implementors.
Among many minor issues, we thus pin-pointed the behavior of null in collections as well as in casts
and the desired isKindOf-semantics of allInstances().

6.2. Lessons Learned

While our paper and pencil arguments, given in [12], turned out to be essentially correct, there had
also been a lesson to be learned: If the logic is not defined as a Kleene-Logic, having a structure similar
to a complete partial order (CPO), reasoning becomes complicated: several important algebraic laws
break down which makes reasoning in OCL inherent messy and a semantically clean compilation of
OCL formulae to a two-valued presentation, that is amenable to animators like KodKod [34] or SMT-
solvers like Z3 [19] completely impractical. Concretely, if the expression not (null) is defined invalid
(as was the case in prior versions of the standard [32]), then standard involution does not hold, i. e.,
not(not(A)) = A does not hold universally. Similarly, if null and null is invalid, then not even
idempotence X and X = X holds. We strongly argue in favor of a lattice-like organization, where null
represents "more information" than invalid and the logical operators are monotone with respect to
this semantical "information ordering."

A similar experience with prior paper and pencil arguments was our investigation of the object-
oriented data-models, in particular path-expressions [15]. The final presentation is again essentially
correct, but the technical details concerning exception handling lead finally to a continuation-passing
style of the (in future generated) definitions for accessors, casts and tests. Apparently, OCL semantics
(as many other "real" programming and specification languages) is meanwhile too complex to be treated
by informal arguments solely.

Featherweight OCL makes several minor deviations from the standard and showed how the previous
constructions can be made correct and consistent, and the DNF-normalization as well as δ-closure laws
(necessary for a transition into a two-valued presentation of OCL specifications ready for interpretation
in SMT solvers (see [13] for details)) are valid in Featherweight OCL.

6.3. Conclusion and Future Work

Featherweight OCL concentrates on formalizing the semantics of a core subset of OCL in general and
in particular on formalizing the consequences of a four-valued logic (i. e., OCL versions that support,
besides the truth values true and false also the two exception values invalid and null ).

In the following, we outline the following future extensions to use Featherweight OCL for a concrete
fully fledged tool for OCL. There are essentially five extensions necessary:

* development of a compiler that compiles a textual or CASE tool representation (e. g., using XMI or the textual syntax of the USE tool [33]) of class models into an object-oriented data type theory automatically.

* Full support of OCL standard syntax in a front-end parser; Such a parser could also generate the necessary casts as well as converting standard OCL to Featherweight OCL as well as providing "normalizations" such as converting multiplicities of class attributes to into OCL class invariants.

* a setup for translating Featherweight OCL into a two-valued representation as described in [13]. As, in real-world scenarios, large parts of UML/OCL specifications are defined (e. g., from the default multiplicity 1 of an attributes x, we can directly infer that for all valid states x is neither invalid nor null ), such a translation enables both an integration of fast constraint solvers such as Z3 as well as test-case generation scenarios as described in [13].

* a setup in Featherweight OCL of the Nitpick animator [3]. It remains to be shown that the standard, Kodkod [34] based animator in Isabelle can give a similar quality of animation as the OCLexec Tool [24]
* a code-generator setup for Featherweight OCL for Isabelle's code generator. For example, the Isabelle code generator supports the generation of F#, which would allow to use OCL specifications for testing arbitrary .net-based applications.

The first two extensions are sufficient to provide a formal proof environment for OCL 2.5 similar to HOL-OCL while the remaining extensions are geared towards increasing the degree of proof automation and usability as well as providing a tool-supported test methodology for UML/OCL.

Our work shows that developing a machine-checked formal semantics of recent OCL standards still reveals significant inconsistencies—even though this type of research is not new. In fact, we started our work already with the 1.x series of OCL. The reasons for this ongoing consistency problems of OCL standard are manifold. For example, the consequences of adding an additional exception value to OCL 2.2 are widespread across the whole language and many of them are also quite subtle. Here, a machine-checked formal semantics is of great value, as one is forced to formalize all details and subtleties. Moreover, the standardization process of the OMG, in which standards (e. g., the UML infrastructure and the OCL standard) that need to be aligned closely are developed quite independently, are prone to ad-hoc changes that attempt to align these standards. And, even worse, updating a standard document by voting on the acceptance (or rejection) of isolated text changes does not help either. Here, a tool for the editor of the standard that helps to check the consistency of the whole standard after each and every modifications can be of great value as well.
<figure><img src="image_18.png" /></figure>
Bibliography

[1] P. B. Andrews. *Introduction to Mathematical Logic and Type Theory: To Truth through Proof*. Kluwer Academic Publishers, Dordrecht, 2nd edition, 2002. ISBN 1-402-00763-9.

[2] C. Barrett and C. Tinelli. Cvc3. In W. Damm and H. Hermanns, editors, *CAV*, volume 4590 of *Lecture Notes in Computer Science*, pages 298–302. Springer-Verlag, 2007. ISBN 978-3-540-73367-6. doi: 10.1007/978-3-540-73368-3_34.

[3] J. C. Blanchette and T. Nipkow. Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In M. Kaufmann and L. C. Paulson, editors, *ITP*, volume 6172 of *Lecture Notes in Computer Science*, pages 131–146. Springer-Verlag, 2010. ISBN 978-3-642-14051-8. doi: 10.1007/978-3-642-14052-5_11.

[4] A. D. Brucker. *An Interactive Proof Environment for Object-oriented Specifications*. PhD thesis, ETH Zurich, Mar. 2007. URL http://www.brucker.ch/bibliography/abstract/brucker-interactive-2007. ETH Dissertation No. 17097.

[5] A. D. Brucker and B. Wolff. A proposal for a formal OCL semantics in Isabelle/HOL. In V. A. Carreño, C. A. Muñoz, and S. Tahar, editors, *Theorem Proving in Higher Order Logics (TPHOLs)*, number 2410 in Lecture Notes in Computer Science, pages 99–114. Springer-Verlag, Heidelberg, 2002. ISBN 3-540-44039-9. doi: 10.1007/3-540-45685-6_8. URL http://www.brucker.ch/bibliography/abstract/brucker.ea-proposal-2002.

[6] A. D. Brucker and B. Wolff. The HOL-OCL book. Technical Report 525, ETH Zurich, 2006. URL http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-book-2006.

[7] A. D. Brucker and B. Wolff. An extensible encoding of object-oriented data models in hol. *Journal of Automated Reasoning*, 41:219–249, 2008. ISSN 0168-7433. doi: 10.1007/s10817-008-9108-3. URL http://www.brucker.ch/bibliography/abstract/brucker.ea-extensible-2008-b.

[8] A. D. Brucker and B. Wolff. HOL-OCL – A Formal Proof Environment for UML/OCL. In J. Fiadeiro and P. Inverardi, editors, *Fundamental Approaches to Software Engineering (FASE08)*, number 4961 in Lecture Notes in Computer Science, pages 97–100. Springer-Verlag, Heidelberg, 2008. doi: 10.1007/978-3-540-78743-3_8. URL http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-2008.

[9] A. D. Brucker and B. Wolff. Semantics, calculi, and analysis for object-oriented specifications. *Acta Informatica*, 46(4):255–284, July 2009. ISSN 0001-5903. doi: 10.1007/s00236-009-0093-8. URL http://www.brucker.ch/bibliography/abstract/brucker.ea-semantics-2009.

[10] A. D. Brucker, J. Doser, and B. Wolff. Semantic issues of OCL: Past, present, and future. *Electronic Communications of the EASST*, 5, 2006. ISSN 1863-2122. URL http://www.brucker.ch/bibliography/abstract/brucker.ea-semantic-2006-b.

[11] A. D. Brucker, J. Doser, and B. Wolff. A model transformation semantics and analysis methodology for SecureUML. In O. Nierstrasz, J. Whittle, D. Harel, and G. Reggio, editors, *MODELS 2006: Model Driven Engineering Languages and Systems*, number 4199 in Lecture Notes in Computer Science, pages 306–320. Springer-Verlag, Heidelberg, 2006. doi: 10.1007/11880240_22. URL http://www.brucker.ch/bibliography/abstract/brucker.ea-transformation-2006. An extended version of this paper is available as ETH Technical Report, no. 524.
[12] A. D. Brucker, M. P. Krieger, and B. Wolff. Extending OCL with null-references. In S. Gosh, editor, *Models in Software Engineering*, number 6002 in Lecture Notes in Computer Science, pages 261–275. Springer-Verlag, Heidelberg, 2009. doi: 10.1007/978-3-642-12261-3_25. URL http://www.brucker.ch/bibliography/abstract/brucker.ea-ocl-null-2009. Selected best papers from all satellite events of the MoDELS 2009 conference.

[13] A. D. Brucker, M. P. Krieger, D. Longuet, and B. Wolff. A specification-based test case generation method for UML/OCL. In J. Dingel and A. Solberg, editors, *MODELS Workshops*, number 6627 in Lecture Notes in Computer Science, pages 334–348. Springer-Verlag, Heidelberg, 2010. ISBN 978-3-642-21209-3. doi: 10.1007/978-3-642-21210-9_33. URL http://www.brucker.ch/bibliography/abstract/brucker.ea-ocl-testing-2010. Selected best papers from all satellite events of the MoDELS 2010 conference. Workshop on OCL and Textual Modelling.

[14] A. D. Brucker, D. Chiorean, T. Clark, B. Demuth, M. Gogolla, D. Plotnikov, B. Rumpe, E. D. Willink, and B. Wolff. Report on the Aachen OCL meeting. In J. Cabot, M. Gogolla, I. Rath, and E. Willink, editors, *Proceedings of the MODELS 2013 OCL Workshop (OCL 2013)*, volume 1092 of *CEUR Workshop Proceedings*, pages 23–32. CEUR-WS.org, 2013. URL http://www.brucker.ch/bibliography/abstract/brucker.ea-summary-aachen-2013.

[15] A. D. Brucker, D. Longuet, F. Tuong, and B. Wolff. On the semantics of object-oriented data structures and path expressions. In J. Cabot, M. Gogolla, I. Ráth, and E. D. Willink, editors, *Proceedings of the MODELS 2013 OCL Workshop (OCL 2013)*, volume 1092 of *CEUR Workshop Proceedings*, pages 23–32. CEUR-WS.org, 2013. URL http://www.brucker.ch/bibliography/abstract/brucker.ea-path-expressions-2013. An extended version of this paper is available as LRI Technical Report 1565.

[16] A. Church. A formulation of the simple theory of types. *Journal of Symbolic Logic*, 5(2):56–68, June 1940.

[17] T. Clark and J. Warmer, editors. *Object Modeling with the OCL: The Rationale behind the Object Constraint Language*, volume 2263 of *Lecture Notes in Computer Science*, Heidelberg, 2002. Springer-Verlag. ISBN 3-540-43169-1.

[18] S. Cook, A. Kleppe, R. Mitchell, B. Rumpe, J. Warmer, and A. Wills. The amsterdam manifesto on OCL. In Clark and Warmer [17], pages 115–149. ISBN 3-540-43169-1.

[19] L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In C. R. Ramakrishnan and J. Rehof, editors, *TACAS*, volume 4963 of *Lecture Notes in Computer Science*, pages 337–340, Heidelberg, 2008. Springer-Verlag. ISBN 978-3-540-78799-0. doi: 10.1007/978-3-540-78800-3_24.

[20] M. Gogolla and M. Richters. Expressing UML class diagrams properties with OCL. In Clark and Warmer [17], pages 85–114. ISBN 3-540-43169-1.

[21] F. Haftmann and M. Wenzel. Constructive type classes in isabelle. In T. Altenkirch and C. McBride, editors, *Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers*, volume 4502 of *Lecture Notes in Computer Science*, pages 160–174. Springer, 2006. ISBN 978-3-540-74463-4. doi: 10.1007/978-3-540-74464-1_11. URL http://dx.doi.org/10.1007/978-3-540-74464-1_11.

[22] A. Hamie, F. Civello, J. Howse, S. Kent, and R. Mitchell. Reflections on the Object Constraint Language. In J. Bézivin and P.-A. Muller, editors, *The Unified Modeling Language. «UML» '98: Beyond the Notation*, volume 1618 of *Lecture Notes in Computer Science*, pages 162–172, Heidelberg, 1998. Springer-Verlag. ISBN 3-540-66252-9. doi: 10.1007/b72309.

[23] P. Kosiuczenko. Specification of invariability in OCL. In O. Nierstrasz, J. Whittle, D. Harel, and G. Reggio, editors, *Model Driven Engineering Languages and Systems (MODELS)*, volume 4199 of *Lecture Notes in Computer Science*, pages 676–691, Heidelberg, 2006. Springer-Verlag. ISBN 978-3-540-45772-5. doi: 10.1007/11880240_47.
[24] M. P. Krieger, A. Knapp, and B. Wolff. Generative programming and component engineering. In E. Visser and J. Järvi, editors, *International Conference on Generative Programming and Component Engineering (GPCE 2010)*, pages 53–62. ACM, Oct. 2010. ISBN 978-1-4503-0154-1.

[25] G. T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby, D. R. Cok, P. Müller, J. Kiniry, and P. Chalin. JML reference manual (revision 1.2), Feb. 2007. Available from http://www.jmlspecs.org.

[26] L. Mandel and M. V. Cengarle. On the expressive power of OCL. In J. M. Wing, J. Woodcock, and J. Davies, editors, *World Congress on Formal Methods in the Development of Computing Systems (FM)*, volume 1708 of *Lecture Notes in Computer Science*, pages 854–874, Heidelberg, 1999. Springer-Verlag. ISBN 3-540-66587-0.

[27] T. Nipkow, L. C. Paulson, and M. Wenzel. *Isabelle/HOL—A Proof Assistant for Higher-Order Logic*, volume 2283 of *Lecture Notes in Computer Science*. Springer-Verlag, Heidelberg, 2002. doi: 10.1007/3-540-45949-9.

[28] Object Management Group. Object constraint language specification (version 1.1), Sept. 1997. Available as OMG document ad/97-08-08.

[29] Object Management Group. UML 2.0 OCL specification, Apr. 2006. Available as OMG document formal/06-05-01.

[30] Object Management Group. UML 2.4.1: Infrastructure specification, Aug. 2011. Available as OMG document formal/2011-08-05.

[31] Object Management Group. UML 2.4.1: Superstructure specification, Aug. 2011. Available as OMG document formal/2011-08-06.

[32] Object Management Group. UML 2.3.1 OCL specification, Feb. 2012. Available as OMG document formal/2012-01-01.

[33] M. Richters. *A Precise Approach to Validating UML Models and OCL Constraints*. PhD thesis, Universität Bremen, Logos Verlag, Berlin, BISS Monographs, No. 14, 2002.

[34] E. Torlak and D. Jackson. Kodkod: A relational model finder. In O. Grumberg and M. Huth, editors, *TACAS*, volume 4424 of *Lecture Notes in Computer Science*, pages 632–647, Heidelberg, 2007. Springer-Verlag. ISBN 978-3-540-71208-4. doi: 10.1007/978-3-540-71209-1_49.

[35] M. Wenzel and B. Wolff. Building formal method tools in the Isabelle/Isar framework. In K. Schneider and J. Brandt, editors, *TPHOLs 2007*, number 4732 in *Lecture Notes in Computer Science*, pages 352–367. Springer-Verlag, Heidelberg, 2007. doi: 10.1007/978-3-540-74591-4_26.

[36] M. M. Wenzel. *Isabelle/Isar — a versatile environment for human-readable formal proof documents*. PhD thesis, TU München, München, Feb. 2002. URL http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html.
<figure><img src="image_19.png" /></figure>
Part III.

Appendix
<figure><img src="image_20.png" /></figure>
# A. The OCL And Featherweight OCL Syntax

<table><caption>Table A.1.: Comparison of different concrete syntax variants for OCL</caption><thead><tr><th></th><th>OCL</th><th>Featherweight OCL</th><th>Logical Constant</th></tr></thead><tbody><tr><td rowspan="10">OclAny</td><td>- = -</td><td>op &Delta;</td><td>UML-Logic.StrongEq</td></tr><tr><td>- &lt;&gt; -</td><td>op &lt;&gt;</td><td>notequal</td></tr><tr><td>- &gt;&gt; oclAsSet( _ )</td><td></td><td></td></tr><tr><td>- .oclIsNew()</td><td>__ .oclIsNew()</td><td>UML-State.OclIsNew</td></tr><tr><td>not ( _ &gt;&gt; oclIsUndefined() )</td><td>&delta;</td><td>UML-Logic.defined</td></tr><tr><td>not ( _ &gt;&gt; oclIsInvalid() )</td><td>v__</td><td>UML-Logic valid</td></tr><tr><td>- &gt;&gt; oclAsType( _ )</td><td></td><td></td></tr><tr><td>- &gt;&gt; oclIsTypeOf( _ )</td><td></td><td></td></tr><tr><td>- &gt;&gt; oclIsKindOf( _ )</td><td></td><td></td></tr><tr><td>- &gt;&gt; oclIsInState( _ )</td><td></td><td></td></tr><tr><td>- &gt;&gt; oclType()</td><td></td><td></td></tr><tr><td>- &gt;&gt; oclLocale()</td><td></td><td></td></tr><tr><td rowspan="10">OclVoid</td><td>- = -</td><td>op &Delta;</td><td>UML-Logic.StrongEq</td></tr><tr><td>- &lt;&gt; -</td><td>op &lt;&gt;</td><td>notequal</td></tr><tr><td>- &gt;&gt; oclAsSet( _ )</td><td></td><td></td></tr><tr><td>- .oclIsNew()</td><td>__ .oclIsNew()</td><td>UML-State.OclIsNew</td></tr><tr><td>not ( _ &gt;&gt; oclIsUndefined() )</td><td>&delta;</td><td>UML-Logic.defined</td></tr><tr><td>not ( _ &gt;&gt; oclIsInvalid() )</td><td>v__</td><td>UML-Logic valid</td></tr><tr><td>- &gt;&gt; oclAsType( _ )</td><td></td><td></td></tr><tr><td>- &gt;&gt; oclIsTypeOf( _ )</td><td></td><td></td></tr><tr><td>- &gt;&gt; oclIsKindOf( _ )</td><td></td><td></td></tr><tr><td>- &gt;&gt; oclIsInState( _ )</td><td></td><td></td></tr><tr><td>- &gt;&gt; oclType()</td><td></td><td></td></tr><tr><td>- &gt;&gt; oclLocale()</td><td></td><td></td></tr><tr><td rowspan="10">OclInvalid</td><td>- = -</td><td>op &Delta;</td><td>UML-Logic.StrongEq</td></tr><tr><td>- &lt;&gt; -</td><td>op &lt;&gt;</td><td>notequal</td></tr><tr><td>- &gt;&gt; oclAsSet( _ )</td><td></td><td></td></tr><tr><td>- .oclIsNew()</td><td>__ .oclIsNew()</td><td>UML-State.OclIsNew</td></tr><tr><td>not ( _ &gt;&gt; oclIsUndefined() )</td><td>&delta;</td><td>UML-Logic.defined</td></tr><tr><td>not ( _ &gt;&gt; oclIsInvalid() )</td><td>v__</td><td>UML-Logic valid</td></tr><tr><td>- &gt;&gt; oclAsType( _ )</td><td></td><td></td></tr><tr><td>- &gt;&gt; oclIsTypeOf( _ )</td><td></td><td></td></tr><tr><td>- &gt;&gt; oclIsKindOf( _ )</td><td></td><td></td></tr><tr><td>- &gt;&gt; oclIsInState( _ )</td><td></td><td></td></tr><tr><td>- &gt;&gt; oclType()</td><td></td><td></td></tr><tr><td>- &gt;&gt; oclLocale()</td><td></td><td></td></tr><tr><td rowspan="3">Real</td><td>- + -</td><td>op +<sub>real</sub></td><td>UML-Real.OclAdd<sub>Real</sub></td></tr><tr><td>- - -</td><td>op -<sub>real</sub></td><td>UML-Real.OclMinus<sub>Real</sub></td></tr><tr><td>- * -</td><td>op *<sub>real</sub></td><td>UML-Real.OclMult<sub>Real</sub></td></tr></tbody></table>

*Continued on next page*
<table><thead><tr><th>OCL</th><th>Featherweight OCL</th><th>Logical Constant</th></tr></thead><tbody><tr><td>-</td><td></td><td></td></tr><tr><td>- / -</td><td></td><td></td></tr><tr><td>- .abs()</td><td></td><td></td></tr><tr><td>- .floor()</td><td></td><td></td></tr><tr><td>- .round()</td><td></td><td></td></tr><tr><td>- .max()</td><td></td><td></td></tr><tr><td>- .min()</td><td></td><td></td></tr><tr><td>- < -</td><td>op &lt;= real</td><td>UML-Real.OclLessReal</td></tr><tr><td>- > -</td><td></td><td></td></tr><tr><td>- &lt;= -</td><td>op &lt;= real</td><td>UML-Real.OclLeReal</td></tr><tr><td>- &gt;= -</td><td></td><td></td></tr><tr><td>- .toString()</td><td></td><td></td></tr><tr><td>- .div(_)</td><td>op divreal</td><td>UML-Real.OclDivisionReal</td></tr><tr><td>- .mod(_)</td><td>op modreal</td><td>UML-Real.OclModulusReal</td></tr><tr><td>- &gt;oclAsType(Integer)</td><td>__ &gt; oclAsTypeReal(Integer)</td><td>UML-Library.OclAsIntegerReal</td></tr><tr><td>- &gt;oclAsType(Boolean)</td><td>__ &gt; oclAsTypeReal(Boolean)</td><td>UML-Library.OclAsBooleanReal</td></tr><tr><td>0.0</td><td>0.0</td><td>UML-Real.OclReal0</td></tr><tr><td>1.0</td><td>1.0</td><td>UML-Real.OclReal1</td></tr><tr><td>2.0</td><td>2.0</td><td>UML-Real.OclReal2</td></tr><tr><td>3.0</td><td>3.0</td><td>UML-Real.OclReal3</td></tr><tr><td>4.0</td><td>4.0</td><td>UML-Real.OclReal4</td></tr><tr><td>5.0</td><td>5.0</td><td>UML-Real.OclReal5</td></tr><tr><td>6.0</td><td>6.0</td><td>UML-Real.OclReal6</td></tr><tr><td>7.0</td><td>7.0</td><td>UML-Real.OclReal7</td></tr><tr><td>8.0</td><td>8.0</td><td>UML-Real.OclReal8</td></tr><tr><td>9.0</td><td>9.0</td><td>UML-Real.OclReal9</td></tr><tr><td>10.0</td><td>10.0</td><td>UML-Real.OclReal10</td></tr><tr><td></td><td>π</td><td>UML-Real.OclRealpi</td></tr><tr><td>Integer</td><td></td><td></td></tr><tr><td>- - -</td><td>op -int</td><td>UML-Integer.OclMinusInteger</td></tr><tr><td>- + -</td><td>op +int</td><td>UML-Integer.OclAddInteger</td></tr><tr><td>- -</td><td></td><td></td></tr><tr><td>- * -</td><td>op *int</td><td>UML-Integer.OclMultInteger</td></tr><tr><td>- / -</td><td></td><td></td></tr><tr><td>- .abs()</td><td></td><td></td></tr><tr><td>- div ( _ )</td><td>op divint</td><td>UML-Integer.OclDivisionInteger</td></tr><tr><td>- mod ( _ )</td><td>op modint</td><td>UML-Integer.OclModulusInteger</td></tr><tr><td>- .max()</td><td></td><td></td></tr><tr><td>- .min()</td><td></td><td></td></tr><tr><td>- .toString()</td><td></td><td></td></tr><tr><td>- < -</td><td>op &lt;= int</td><td>UML-Integer.OclLessInteger</td></tr><tr><td>- &lt;= -</td><td>op &lt;= int</td><td>UML-Integer.OclLeInteger</td></tr><tr><td>- &gt;oclAsType(Real)</td><td>__ &gt; oclAsTypeInt(Real)</td><td>UML-Library.OclAsRealInt</td></tr><tr><td>- &gt;oclAsType(Boolean)</td><td>__ &gt; oclAsTypeInt(Boolean)</td><td>UML-Library.OclAsBooleanInt</td></tr><tr><td>0</td><td>0</td><td>UML-Integer.OclInt0</td></tr><tr><td>1</td><td>1</td><td>UML-Integer.OclInt1</td></tr><tr><td>2</td><td>2</td><td>UML-Integer.OclInt2</td></tr><tr><td>3</td><td>3</td><td>UML-Integer.OclInt3</td></tr><tr><td>4</td><td>4</td><td>UML-Integer.OclInt4</td></tr><tr><td>5</td><td>5</td><td>UML-Integer.OclInt5</td></tr></tbody></table>

Continued on next page
<table><thead><tr><th></th><th>OCL</th><th>Featherweight OCL</th><th>Logical Constant</th></tr></thead><tbody><tr><td></td><td>6</td><td>6</td><td>UML-Integer.OclInt6</td></tr><tr><td></td><td>7</td><td>7</td><td>UML-Integer.OclInt7</td></tr><tr><td></td><td>8</td><td>8</td><td>UML-Integer.OclInt8</td></tr><tr><td></td><td>9</td><td>9</td><td>UML-Integer.OclInt9</td></tr><tr><td></td><td>10</td><td>10</td><td>UML-Integer.OclInt10</td></tr><tr><td></td><td>- + -<br/>- .size()<br/>- .concat(_ )<br/>- .substring(_ , _ )<br/>- .toInteger()<br/>- .toReal()<br/>- .toUppercase()<br/>- .toMixedCase()<br/>- .indexOf()<br/>- .equals ignore Case(_ )<br/>- .at(_ )<br/>- .characters()<br/>- .toBoolean()<br/>- < -<br/>- > -<br/>- <= -<br/>- >= -</td><td>op +string</td><td>UML-String.OclAdd String</td></tr><tr><td></td><td>a<br/>b<br/>c</td><td>a<br/>b<br/>c</td><td>UML-String.OclStringa<br/>UML-String.OclStringb<br/>UML-String.OclStringc</td></tr><tr><td></td><td>- or -<br/>- xor -<br/>- and -<br/>- not -<br/>- implies -<br/>- .toString()<br/>if _ then _ else _ endif<br/>- = -<br/>- <> -</td><td>op or<br/>op and<br/>not<br/>op implies<br/>if _ then _ else _ endif<br/>op =<br/>op &lt;&gt;<br/>- |&ne; -<br/>- |&asymp; -<br/>- op =</td><td>UML-Logic.OclOr<br/>UML-Logic.OclAnd<br/>UML-Logic.OclNot<br/>UML-Logic.OclImplies<br/>UML-Logic.OclIf<br/>UML-Logic.StRICT Ref Eq<br/>notequal<br/>OclNonValid<br/>UML-Logic.OclValid<br/>UML-Logic.StrongEq</td></tr><tr><td></td><td>- = -</td><td></td><td></td></tr><tr><td></td><td>Set ( _ )<br/>Set{ }<br/>Set{ _ }<br/>- ->union( _ )<br/>- = -<br/>- ->intersection( _ )<br/>- -<br/>- ->including( _ )<br/>- ->excluding( _ )<br/>- ->symmetricDifference( _ )<br/>- ->count( _ )<br/>- ->flatten()</td><td>Set( type 0 )<br/>Set{ }<br/>Set{ args 0 }<br/>- ->unionSet( _ )<br/>op =<br/>- ->intersectionSet( _ )<br/>- ->includingSet( _ )<br/>- ->excludingSet( _ )<br/>- ->countSet( _ )</td><td>UML-Types.Set base type<br/>UML-Set.mtSet<br/>OclFinset<br/>UML-Set.OclUnion<br/>UML-Logic.StrongEq<br/>UML-Set.OclIntersection<br/>UML-Set.OclIncluding<br/>UML-Set.OclExcluding<br/>UML-Set.OclCount</td></tr></tbody></table>

Continued on next page
## Sequence and Iterators on Sequence

## Bag and Iterators on Bag

<table><thead><tr><th>OCL</th><th>Featherweight OCL</th><th>Logical Constant</th></tr></thead><tbody><tr><td>- ->selectByKind(_)</td><td></td><td></td></tr><tr><td>- ->selectByType(_)</td><td></td><td></td></tr><tr><td>- ->reject(_ | _)</td><td>— ->rejectSet(<b>id</b> | _)</td><td>OclRejectSet</td></tr><tr><td>- ->select(_ | _)</td><td>— ->selectSet(<b>id</b> | _)</td><td>OclSelectSet</td></tr><tr><td>- ->iterate(_; _ = _ | _)</td><td>— ->iterateSet(<b>id</b>; <b>id</b> = any | any)</td><td>OclIterateSet</td></tr><tr><td>- ->exists(_ | _)</td><td>— ->existsSet(<b>id</b> | _)</td><td>OclExistSet</td></tr><tr><td>- ->forAll(_ | _)</td><td>— ->forAllSet(<b>id</b> | _)</td><td>OclForAllSet</td></tr><tr><td>- ->asSequence()</td><td>— ->asSequenceSet()</td><td>UML-Library.OclAsSeqSet</td></tr><tr><td>- ->asBag()</td><td>— ->asBagSet()</td><td>UML-Library.OclAsBagSet</td></tr><tr><td>- ->asPair()</td><td>— ->asPairSet()</td><td>UML-Library.OclAsPairSet</td></tr><tr><td>- ->sum()</td><td>— ->sumSet()</td><td>UML-Set.OclSum</td></tr><tr><td>- ->excludesAll(_)</td><td>— ->excludesAllSet(_)</td><td>UML-Set.OclExcludesAll</td></tr><tr><td>- ->includesAll(_)</td><td>— ->includesAllSet(_)</td><td>UML-Set.OclIncludesAll</td></tr><tr><td>- ->any()</td><td>— ->anySet()</td><td>UML-Set.OclANY</td></tr><tr><td>- ->notEmpty()</td><td>— ->notEmptySet()</td><td>UML-Set.OclNotEmpty</td></tr><tr><td>- ->()</td><td>— ->isEmptySet()</td><td>UML-Set.OclIsEmpty</td></tr><tr><td>- ->size()</td><td>— ->sizeSet()</td><td>UML-Set.OclSize</td></tr><tr><td>- ->excludes(_)</td><td>— ->excludesSet(_)</td><td>UML-Set.OclExcludes</td></tr><tr><td>- ->includes(_)</td><td>— ->includesSet(_)</td><td>UML-Set.OclIncludes</td></tr><tr><td>Sequence(_)</td><td>Sequence(<b>type</b>)</td><td>UML-Types.Sequence<sub>base</sub> <b>type</b></td></tr><tr><td>Sequence{}</td><td>Sequence{}</td><td>UML-Sequence.mtSequence</td></tr><tr><td>Sequence{ _}</td><td>Sequence{ <b>args</b>}</td><td>OclFinsequence</td></tr><tr><td>- ->any()</td><td>— ->anySeq()</td><td>UML-Sequence.OclANY</td></tr><tr><td>- ->notEmpty()</td><td>— ->notEmptySeq()</td><td>UML-Sequence.OclNotEmpty</td></tr><tr><td>- ->empty()</td><td>— ->emptySeq()</td><td>UML-Sequence.OclIsEmpty</td></tr><tr><td>- ->size()</td><td>— ->sizeSeq()</td><td>UML-Sequence.OclSize</td></tr><tr><td>- ->select(_ | _)</td><td>— ->selectSeq(<b>id</b> | _)</td><td>OclSelectSeq</td></tr><tr><td>- ->collect(_ | _)</td><td>— ->collectSeq(<b>id</b> | _)</td><td>OclCollectSeq</td></tr><tr><td>- ->exists(_ | _)</td><td>— ->existsSeq(<b>id</b> | _)</td><td>OclExistSeq</td></tr><tr><td>- ->forAll(_ | _)</td><td>— ->forAllSeq(<b>id</b> | _)</td><td>OclForAllSeq</td></tr><tr><td>- ->iterate(_; _ : _ = _ | _)</td><td>— ->iterateSeq(<b>id</b>; <b>id</b> = any | any)</td><td>OclIterateSeq</td></tr><tr><td>- ->last()</td><td>— ->lastSeq(_)</td><td>UML-Sequence.OclLast</td></tr><tr><td>- ->first()</td><td>— ->firstSeq(_)</td><td>UML-Sequence.OclFirst</td></tr><tr><td>- ->at(_)</td><td>— ->atSeq(_)</td><td>UML-Sequence.OclAt</td></tr><tr><td>- ->union(_)</td><td>— ->unionSeq(_)</td><td>UML-Sequence.OclUnion</td></tr><tr><td>- ->append(_)</td><td>— ->appendSeq(_)</td><td>UML-Sequence.OclAppend</td></tr><tr><td>- ->excluding(_)</td><td>— ->excludingSeq(_)</td><td>UML-Sequence.OclExcluding</td></tr><tr><td>- ->including(_)</td><td>— ->includingSeq(_)</td><td>UML-Sequence.OclIncluding</td></tr><tr><td>- ->prepend(_)</td><td>— ->prependSeq(_)</td><td>UML-Sequence.OclPrepend</td></tr><tr><td>- ->asSet()</td><td>— ->asSetSeq()</td><td>UML-Library.OclAsSetSeq</td></tr><tr><td>- ->asBag()</td><td>— ->asBagSeq()</td><td>UML-Library.OclAsBagSeq</td></tr><tr><td>- ->asPair()</td><td>— ->asPairSeq()</td><td>UML-Library.OclAsPairSeq</td></tr><tr><td>Bag(_)</td><td>Bag(<b>type</b>)</td><td>UML-Types.Bag<sub>base</sub> <b>type</b></td></tr><tr><td>Bag{}</td><td>Bag{}</td><td>UML-Bag.mtBag</td></tr><tr><td>Bag{ _}</td><td>Bag{ <b>args</b>}</td><td>OclFinbag</td></tr><tr><td>- ->sum()</td><td>— ->sumBag()</td><td>UML-Bag.OclSum</td></tr><tr><td>- ->count(_)</td><td>— ->countBag(_)</td><td>UML-Bag.OclCount</td></tr><tr><td>- ->intersection(_)</td><td>— ->intersectionBag(_)</td><td>UML-Bag.OclIntersection</td></tr><tr><td>- ->union(_)</td><td>— ->unionBag(_)</td><td>UML-Bag.OclUnion</td></tr></tbody></table>

Continued on next page
<table><thead><tr><th>OCL</th><th>Featherweight OCL</th><th>Logical Constant</th></tr></thead><tbody><tr><td>- ->excludesAll(_)</td><td>— ->excludesAllBag(_)</td><td>UML-Bag.OclExcludesAll</td></tr><tr><td>- ->includesAll(_)</td><td>— ->includesAllBag(_)</td><td>UML-Bag.OclIncludesAll</td></tr><tr><td>- ->reject(_ | _)</td><td>— ->rejectBag(<u>id</u> | _)</td><td>OclRejectBag</td></tr><tr><td>- ->select(_ | _)</td><td>— ->selectBag(<u>id</u> | _)</td><td>OclSelectBag</td></tr><tr><td>- ->iterate(_; _ = _ | _)</td><td>— ->iterateBag(<u>id</u> | _; <u>id</u> = any | any)</td><td>OclIterateBag</td></tr><tr><td>- ->exists(_ | _)</td><td>— ->existsBag(<u>id</u> | _)</td><td>OclExistBag</td></tr><tr><td>- ->forall(_ | _)</td><td>— ->forallBag(<u>id</u> | _)</td><td>OclForAllBag</td></tr><tr><td>- ->any()</td><td>— ->anyBag()</td><td>UML-Bag.OclANY</td></tr><tr><td>- ->notEmpty()</td><td>— ->notEmptyBag()</td><td>UML-Bag.OclNotEmpty</td></tr><tr><td>- ->()</td><td>— ->isEmptyBag()</td><td>UML-Bag.OclIsEmpty</td></tr><tr><td>- ->size()</td><td>— ->sizeBag()</td><td>UML-Bag.OclSize</td></tr><tr><td>- ->excludes(_)</td><td>— ->excludesBag(_)</td><td>UML-Bag.OclExcludes</td></tr><tr><td>- ->includes(_)</td><td>— ->includesBag(_)</td><td>UML-Bag.OclIncludes</td></tr><tr><td>- ->excluding(_)</td><td>— ->excludingBag(_)</td><td>UML-Bag.OclExcluding</td></tr><tr><td>- ->including(_)</td><td>— ->includingBag(_)</td><td>UML-Bag.OclIncluding</td></tr><tr><td>- ->asSet()</td><td>— ->asSetBag()</td><td>UML-Library.OclAsSetBag</td></tr><tr><td>- ->asSeq()</td><td>— ->asSeqBag()</td><td>UML-Library.OclAsSeqBag</td></tr><tr><td>- ->asPair()</td><td>— ->asPairBag()</td><td>UML-Library.OclAsPairBag</td></tr><tr><td>Pair</td><td>Pair(<u>type</u>, <u>type</u>)<br/>Pair{_, _}<br/>— .Second()</td><td>UML-Types.Pairbase <u>type</u></td></tr><tr><td>- ->asSequence()</td><td>— ->asSequencePair()</td><td>UML-Pair.OclSecond</td></tr><tr><td>- ->asSet()</td><td>— ->asSetPair()</td><td>UML-Pair.OclFirst</td></tr><tr><td>State Access</td><td>— .allInstances()</td><td>UML-Library.OclAsSeqPair</td></tr><tr><td>- .allInstances()</td><td>— .allInstances()</td><td>UML-State.OclAllInstances-at-post</td></tr><tr><td>- .oclsDeleted()</td><td>— .oclsDeleted()</td><td>UML-State.OclAllInstances-at-pre</td></tr><tr><td>- .oclsMaintained()</td><td>— .oclsMaintained()</td><td>UML-State.OclIsDeleted</td></tr><tr><td>- .oclsAbsent()</td><td>— .oclsAbsent()</td><td>UML-State.OclIsMaintained</td></tr><tr><td>- ->oclsModifiedOnly()</td><td>— ->oclsModifiedOnly()</td><td>UML-State.OclIsAbsent</td></tr><tr><td>- @pre-</td><td>— @pre-</td><td>UML-State.OclSelf-at-pre</td></tr><tr><td>- @post-</td><td>— @post-</td><td>UML-State.OclSelf-at-post</td></tr></tbody></table>