Assert $\tau \neq$ (invalid $\triangleq$ 10.0)

Assert $\tau \neq$ (null $\triangleq$ 10.0)

Assert $\tau \neq$ (invalid $\dot{=}$(invalid::('A)Real))

Assert $\tau \neq v$ (invalid $\dot{=}$(invalid::('A)Real))

Assert $\tau \neq$ (invalid $<>$(invalid::('A)Real))

Assert $\tau \neq v$ (invalid $<>$(invalid::('A)Real))

Assert $\tau =$(null $\dot{=}$(null::('A)Real))

Assert $\tau =$(null $\dot{=}$(null::('A)Real))

Assert $\tau =$(4.0 $\dot{=}$(4.0))

Assert $\tau \neq$ (4.0 $<>$ 4.0)

Assert $\tau \neq$ (4.0 $\dot{=}$(10.0))

Assert $\tau =$(4.0 $<>$ 10.0)

Assert $\tau \neq$ (0.0 $<_{real}$ null)

Assert $\tau \neq$ ($\delta$ (0.0 $<_{real}$ null))

end

theory UML-String

imports ../UML-PropertyProfiles

begin

## 2.6. Basic Type String: Operations

### 2.6.1. Fundamental Properties on Strings: Strict Equality

The last basic operation belonging to the fundamental infrastructure of a value-type in OCL is the weak equality, which is defined similar to the 'A Boolean-case as strict extension of the strong equality:

def s (overloaded) StrictRefEq$_{String}$[code-unfold] :

$$ 
\begin{align*}
(x::('A)String) \dot{=} y &\equiv \lambda \tau. \text{ if } (v x) \tau = \text{ true } \tau \land (v y) \tau = \text{ true } \tau \\
&\text{ then } (x \triangleq y) \tau \\
&\text{ else invalid } \tau
\end{align*}
$$

Property proof in terms of profile-bin$_{StrongEq-v-v}$

interpretation StrictRefEq$_{String}$ : profile-bin$_{StrongEq-v-v}$ $\lambda x y. (x::('A)String) \dot{=} y$ 
<proof>

### 2.6.2. Basic String Constants

Although the remaining part of this library reasons about integers abstractly, we provide here as example some convenient shortcuts.

definition OclStringa ::= ('A)String (a) where a = (λ - . $_{\bot}$''a''$_{\bot}$)

definition OclStringb ::= ('A)String (b) where b = (λ - . $_{\bot}$''b''$_{\bot}$)

definition OclStringc ::= ('A)String (c) where c = (λ - . $_{\bot}$''c''$_{\bot}$)

Etc.

### 2.6.3. Validity and Definedness Properties

lemma $\delta$(null::('A)String) = false <proof>

lemma $v$(null::('A)String) = true <proof>

lemma [simp, code-unfold]: $\delta$ ($\lambda$ - . $_{\bot}$n$_{\bot}$ ) = true
〈proof〉

**lemma** [simp,code-unfold]: $v (\lambda. \underset{\downarrow}{n_{\downarrow}}) = true$
<u>proof</u>

lemma [simp,code-unfold]: δ a = true <proof>

lemma [simp,code-unfold]: v a = true <proof>

2.6.4. String Operations

**Definition**

Here is a common case of a built-in operation on built-in types. Note that the arguments must be both
defined (non-null, non-bot).

Note that we can not follow the lexis of the OCL Standard for Isabelle technical reasons; these
operators are heavily overloaded in the HOL library that a further overloading would lead to heavy
technical buzz in this document.

definition OclAdd$_{String}$ ::= (‘A)String ⇒ (‘A)String ⇒ (‘A)String (infix +$_{string}$ 40)

where $x +_{string} y \equiv \lambda \tau. \text{ if } (\delta x) \tau = \text{ true } \tau \wedge (\delta y) \tau = \text{ true } \tau$

then $\perp concat [\overline{\pi x \tau^\top}, \overline{\pi y \tau^\top}]_{\perp}$

else invalid τ

interpretation OclAdd$_{String}$ : profile-bin$_{d}$$_{-}$$_{d}$ op +$_{string}$ λ x y. $\bot$concat [πx$^{⊺}$, πy$^{⊺}$]$_{⊥}$
<proof>

Basic Properties

lemma OclAdd$_{String}$-not-commute : ∃ X Y. (X +$_{string}$ Y ) ≠ ( Y +$_{string}$ X )
<proof>

2.6.5. Test Statements

Here follows a list of code-examples, that explain the meanings of the above definitions by compilation to code and execution to *True*.

Here follows a list of code-examples, that explain the meanings of the above definitions by compilation to code and execution to True.

Elementary computations on String

Assert τ |= a <> b

Assert τ |= b <> a

Assert τ |= b = b

Assert τ |= v a

Assert τ |= δ a

Assert τ |= v (null::('A)String)

Assert τ |:= (invalid ⇝ invalid)

Assert τ |:= (null ⇝ null)

Assert τ |= (a ⇝ a)

Assert τ |≠ (a ⇝ b)

Assert τ |≠ (invalid ⇝ b)

Assert τ |≠ (null ⇝ b)

Assert τ |≠ (invalid = (invalid::(‘A)String))

Assert τ |≠ v (invalid = (invalid::(‘A)String))

Assert τ |≠ (invalid <> (invalid::(‘A)String)))

Assert τ |≠ v (invalid <> (invalid::(‘A)String)))

Assert τ |= (null = (null::(‘A)String))
Assert $\tau \models (null \doteq (null::('A)String))$

Assert $\tau \models (b \doteq b)$

Assert $\tau \models (b <> b)$

Assert $\tau \models (b \doteq c)$

Assert $\tau \models (b <> c)$

end

theory UML-Pair

imports ../UML-PropertyProfiles

begin

## 2.7. Collection Type Pairs: Operations

The OCL standard provides the concept of *Tuples*, i. e. a family of record-types with projection functions. In FeatherWeight OCL, only the theory of a special case is developed, namely the type of Pairs, which is, however, sufficient for all applications since it can be used to mimick all tuples. In particular, it can be used to express operations with multiple arguments, roles of n-ary associations, ...

### 2.7.1. Semantic Properties of the Type Constructor

lemma $A[\mathit{simp}]: \mathit{Rep-Pair}_{\mathit{base}} x \neq \mathit{None} \implies \mathit{Rep-Pair}_{\mathit{base}} x \neq \mathit{null} \implies (\mathit{fst} \ \mathit{Rep-Pair}_{\mathit{base}} x) \neq \mathit{bot}$
$\langle\mathit{proof}\rangle$

lemma $A'[\mathit{simp}]: x \neq \mathit{bot} \implies x \neq \mathit{null} \implies (\mathit{fst} \ \mathit{Rep-Pair}_{\mathit{base}} x) \neq \mathit{bot}$
$\langle\mathit{proof}\rangle$

lemma $B[\mathit{simp}]: \mathit{Rep-Pair}_{\mathit{base}} x \neq \mathit{None} \implies \mathit{Rep-Pair}_{\mathit{base}} x \neq \mathit{null} \implies (\mathit{snd} \ \mathit{Rep-Pair}_{\mathit{base}} x) \neq \mathit{bot}$
$\langle\mathit{proof}\rangle$

lemma $B'[\mathit{simp}]: x \neq \mathit{bot} \implies x \neq \mathit{null} \implies (\mathit{snd} \ \mathit{Rep-Pair}_{\mathit{base}} x) \neq \mathit{bot}$
$\langle\mathit{proof}\rangle$

### 2.7.2. Fundamental Properties of Strict Equality

After the part of foundational operations on sets, we detail here equality on sets. Strong equality is inherited from the OCL core, but we have to consider the case of the strict equality. We decide to overload strict equality in the same way we do for other value's in OCL:

defns (overloaded) StrictRefEqPair :

$$ ((x::('A, 'a::null, 'b::null)Pair) \doteq y) \equiv (\lambda \tau. \ if \ (v x) \tau = true \ \tau \land (v y) \tau = true \ \tau \\ \qquad \text{then } (x \triangleq y)\tau \\ \qquad \text{else invalid } \tau) $$

Property proof in terms of *profile-bin<sub>StrongEq-v-v</sub>*

interpretation StrictRefEqPair : profile-bin<sub>StrongEq-v-v</sub> $\lambda x y. (x::('A, 'a::null, 'b::null)Pair) \doteq y$
$\langle\mathit{proof}\rangle$

### 2.7.3. Standard Operations Definitions

This part provides a collection of operators for the Pair type.
**Definition: Pair Constructor**

definition OclPair::('A, 'α) val ⇒

( 'A, 'β) val ⇒

( 'A, 'α::null, 'β::null) Pair (Pair{(-), (-)})

where

Pair{X,Y} ≡ (λ τ. if (v X) τ = true τ ∧ (v Y) τ = true τ
then Abs-Pair<sub>base</sub> ⊔(X τ, Y τ)
else invalid τ)

interpretation OclPair : profile-bin<sub>v-v</sub>

OclPair λ x y. Abs-Pair<sub>base</sub> ⊔(x, y)⊓

<proof>

**Definition: First**

definition OclFirst:: ('A, 'α::null, 'β::null) Pair ⇒ ('A, 'α) val ( - .First'('))

where

X .First() ≡ (λ τ. if (δ X) τ = true τ
then fst <sup>Π</sup> Rep-Pair<sub>base</sub> (X τ)<sup>Π</sup>
else invalid τ)

interpretation OclFirst : profile-monod OclFirst λx. fst <sup>Π</sup> Rep-Pair<sub>base</sub> (x)<sup>Π</sup>

<proof>

**Definition: Second**

definition OclSecond:: ('A, 'α::null, 'β::null) Pair ⇒ ('A, 'β) val ( - .Second'('))

where

X .Second() ≡ (λ τ. if (δ X) τ = true τ
then snd <sup>Π</sup> Rep-Pair<sub>base</sub> (X τ)<sup>Π</sup>
else invalid τ)

interpretation OclSecond : profile-monod OclSecond λx. snd <sup>Π</sup> Rep-Pair<sub>base</sub> (x)<sup>Π</sup>

<proof>

2.7.4. Logical Properties

lemma 1 : τ ⊧ v Y =⇒ τ ⊧ Pair{X,Y} .First() ≜ X

<proof>

lemma 2 : τ ⊧ v X =⇒ τ ⊧ Pair{X,Y} .Second() ≜ Y

<proof>

2.7.5. Algebraic Execution Properties

lemma proj1-exec [simp, code-unfold] : Pair{X,Y} .First() = (if (v Y) then X else invalid end if)

<proof>

lemma proj2-exec [simp, code-unfold] : Pair{X,Y} .Second() = (if (v X) then Y else invalid end if)

<proof>

2.7.6. Test Statements

instantiation Pair<sub>base</sub> :: (equal, equal) equal

begin

definition HOL equal k l ←→ (k::( 'a::equal , 'b::equal )Pair<sub>base</sub> ) = l

instance <proof>

end
**definition** `Integer` :: (`'A'`, `Integer$_{base}$`) `Bag`

**where** `Integer` $\equiv$ ($\lambda \tau$. (Abs-Bag$_{base}$ o Some o Some) ($\lambda$ None $\Rightarrow$ 0 | Some None $\Rightarrow$ 0 | - $\Rightarrow$ 1))

**definition** `Integer$_{null}$` :: (`'A'`, `Integer$_{base}$`) `Bag`

**where** `Integer$_{null}$` $\equiv$ ($\lambda \tau$. (Abs-Bag$_{base}$ o Some o Some) ($\lambda$ None $\Rightarrow$ 0 | - $\Rightarrow$ 1))

**lemma** `Integer-defined` : $\delta$ `Integer` = true
`<proof>`

**lemma** `Integer$_{null}$-defined` : $\delta$ `Integer$_{null}$` = true
`<proof>`

This allows the theorems:

$\tau$ $\models$ $\delta$ $x$ $\implies$ $\tau$ $\models$ (Integer$\rightarrow$includes$_{Bag}$(x)) $\tau$ $\models$ $\delta$ $x$ $\implies$ $\tau$ $\models$ Integer $\triangleq$
(Integer$\rightarrow$including$_{Bag}$(x))

and

$\tau$ $\models$ $\nu$ $x$ $\implies$ $\tau$ $\models$ (Integer$_{null}$$\rightarrow$includes$_{Bag}$(x)) $\tau$ $\models$ $\nu$ $x$ $\implies$ $\tau$ $\models$ Integer$_{null}$ $\triangleq$
(Integer$_{null}$$\rightarrow$including$_{Bag}$(x))

which characterize the infiniteness of these bags by a recursive property on these bags.

In the same spirit, we proceed similarly for the remaining base types:

**definition** `Void$_{null}$` :: (`'A'`, `Void$_{base}$`) `Bag`

**where** `Void$_{null}$` $\equiv$ ($\lambda \tau$. (Abs-Bag$_{base}$ o Some o Some) ($\lambda$ x. if x = Abs-Void$_{base}$ (Some None) then 1 else 0))

**definition** `Void$_{empty}$` :: (`'A'`, `Void$_{base}$`) `Bag`

**where** `Void$_{empty}$` $\equiv$ ($\lambda \tau$. (Abs-Bag$_{base}$ o Some o Some) ($\lambda$- 0))

**lemma** `Void$_{null}$-defined` : $\delta$ `Void$_{null}$` = true
`<proof>`

**lemma** `Void$_{empty}$-defined` : $\delta$ `Void$_{empty}$` = true
`<proof>`

**lemma** assumes $\tau$ $\models$ $\delta$ (`V` :: (`'A'`, `Void$_{base}$`) `Bag`)

shows $\tau$ $\models$ `V` $\cong$ `Void$_{null}$` $\lor$ $\tau$ $\models$ `V` $\cong$ `Void$_{empty}$`
`<proof>`

**definition** `Boolean` :: (`'A'`, `Boolean$_{base}$`) `Bag`

**where** `Boolean` $\equiv$ ($\lambda \tau$. (Abs-Bag$_{base}$ o Some o Some) ($\lambda$ None $\Rightarrow$ 0 | Some None $\Rightarrow$ 0 | - $\Rightarrow$ 1))

**definition** `Boolean$_{null}$` :: (`'A'`, `Boolean$_{base}$`) `Bag`

**where** `Boolean$_{null}$` $\equiv$ ($\lambda \tau$. (Abs-Bag$_{base}$ o Some o Some) ($\lambda$ None $\Rightarrow$ 0 | - $\Rightarrow$ 1))

**lemma** `Boolean-defined` : $\delta$ `Boolean` = true
`<proof>`

**lemma** `Boolean$_{null}$-defined` : $\delta$ `Boolean$_{null}$` = true
`<proof>`

**definition** `String` :: (`'A'`, `String$_{base}$`) `Bag`

**where** `String` $\equiv$ ($\lambda \tau$. (Abs-Bag$_{base}$ o Some o Some) ($\lambda$ None $\Rightarrow$ 0 | Some None $\Rightarrow$ 0 | - $\Rightarrow$ 1))

**definition** `String$_{null}$` :: (`'A'`, `String$_{base}$`) `Bag`

**where** `String$_{null}$` $\equiv$ ($\lambda \tau$. (Abs-Bag$_{base}$ o Some o Some) ($\lambda$ None $\Rightarrow$ 0 | - $\Rightarrow$ 1))

**lemma** `String-defined` : $\delta$ `String` = true
`<proof>`

**lemma** `String null-defined`: `δ String null = true`
`<proof>`

**definition** `Real` :: (`'A`, `Real base`) Bag
**where** `Real` = (`λ τ. (Abs-Bag base o Some o Some)` (`λ None ⇒ 0 | Some None ⇒ 0 | - ⇒ 1`))

**definition** `Real null` :: (`'A`, `Real base`) Bag
**where** `Real null` = (`λ τ. (Abs-Bag base o Some o Some)` (`λ None ⇒ 0 | - ⇒ 1`))

**lemma** `Real-defined`: `δ Real = true`
`<proof>`

**lemma** `Real null-defined`: `δ Real null = true`
`<proof>`

## 2.8.2. Basic Properties of the Bag Type

Every element in a defined bag is valid.

**lemma** `Bag-inv-lemma`: `τ |= (δ X) ⇒ ⊑ Rep-Bag base (X τ) ⊕ bot = 0`
`<proof>`

**lemma** `Bag-inv-lemma'` :
*assumes* `x-def`: `τ |= δ X`
*and* `e-mem`: ` Rep-Bag base (X τ) ⊕ e ≥ 1`
*shows* `τ |= v (λ-. e)`
`<proof>`

**lemma** `abs-rep-simp'` :
*assumes* `S-all-def`: `τ |= δ S`
*shows* `Abs-Bag base ⊑ Rep-Bag base (S τ) ⊕ = S τ`
`<proof>`

**lemma** `invalid-bag-OclNot-defined` `[simp, code-unfold]`: `δ(invalid::('A, 'α::null) Bag) = false`
`<proof>`

**lemma** `null-bag-OclNot-defined` `[simp, code-unfold]`: `δ(null::('A, 'α::null) Bag) = false`
`<proof>`

**lemma** `invalid-bag-valid` `[simp, code-unfold]`: `v(invalid::('A, 'α::null) Bag) = false`
`<proof>`

**lemma** `null-bag-valid` `[simp, code-unfold]`: `v(null::('A, 'α::null) Bag) = true`
`<proof>`

... which means that we can have a type (`'A`, (`'A`, (`'A` Integer) Bag) Bag` corresponding exactly to `Bag(Bag Integer)` in OCL notation. Note that the parameter `'A` still refers to the object universe; making the OCL semantics entirely parametric in the object universe makes it possible to study (and prove) its properties independently from a concrete class diagram.

## 2.8.3. Definition: Strict Equality

After the part of foundational operations on bags, we detail here equality on bags. Strong equality is inherited from the OCL core, but we have to consider the case of the strict equality. We decide to overload strict equality in the same way we do for other value's in OCL:

**def s (overloaded)** `StrictRefEqBag` :
`(x::('A, 'α::null)Bag) := y ≡ λ τ. if (v x) τ = true τ ∧ (v y) τ = true τ`
*then* `(x ≜ y)τ`
*else* `invalid τ`
One might object here that for the case of objects, this is an empty definition. The answer is no, we will restrain later on states and objects such that any object has its oid stored inside the object (so the ref, under which an object can be referenced in the store will represented in the object itself). For such well-formed stores that satisfy this invariant (the WFF-invariant), the referential equality and the strong equality—and therefore the strict equality on bags in the sense above—coincides.

Property proof in terms of *profile-bin<sub>StrongEq-v-v</sub>*

**interpretation** *StrictRefEqBag* : *profile-bin<sub>StrongEq-v-v</sub>* $\lambda x y$. ($x::('\mathfrak{A}',\alpha::null)Bag \doteq y$ 
*⟨proof⟩*

**2.8.4. Constants: mtBag**

**definition** *mtBag*::('A, 'α::null) *Bag* (*Bag*{})

**where** *Bag*{} = (λτ. Abs-*Bag*<sub>base</sub> ⊔λ-. 0::nat<sub>⊥</sub>)

**lemma** *mtBag-defined*[simp, code-unfold]: $\delta(\mathit{Bag}\{\}) = \mathit{true}$
*⟨proof⟩*

**lemma** *mtBag-valid*[simp, code-unfold]: $v(\mathit{Bag}\{\}) = \mathit{true}$
*⟨proof⟩*

**lemma** *mtBag-rep-bag*: $\top \mathit{Rep-Bag}_{base} (\mathit{Bag}\{\} \tau)^{\top} = (\lambda - . 0)$
*⟨proof⟩* **lemma** [*simp, code-unfold*]: *const Bag*{}
*⟨proof⟩*

Note that the collection types in OCL allow for null to be included; however, there is the null-collection into which inclusion yields invalid.

**2.8.5. Definition: Including**

**definition** *OclIncluding* :: [(('A, 'α::null) *Bag*, ('A, 'α) *val*)] ⇒ ('A, 'α) *Bag*

**where** *OclIncluding* $x y = (\lambda \tau. \mathit{if} (\delta x) \tau = \mathit{true} \tau \land (v y) \tau = \mathit{true} \tau$

then *Abs-Bag*<sub>base</sub> ⊔ ⌜Rep-Bag<sub>base</sub>(x τ)⌝

$$((y \tau) := \top \mathit{Rep-Bag}_{base}(x \tau)^{\top} (y \tau) + 1)$$

else invalid $\tau$ ⊔

**notation** *OclIncluding* $(- \rightarrow \mathit{including}_{Bag}'(-))$

**interpretation** *OclIncluding* : *profile-bin<sub>d-v</sub>* *OclIncluding* $\lambda x y$. *Abs-Bag*<sub>base</sub> ⊔ ⌜Rep-Bag<sub>base</sub>(x τ)⌝
($y := \top \mathit{Rep-Bag}_{base}(x \tau)^{\top} y + 1$) ⊔

*⟨proof⟩*

**syntax**

- *OclFinbag* :: *args* => ('A, 'a::null) *Bag* (*Bag*{(-)})

**translations**

*Bag{x, xs} == CONST *OclIncluding* (Bag{xs}) x

*Bag{x} == CONST *OclIncluding* (Bag{}) x

**2.8.6. Definition: Excluding**

**definition** *OclExcluding* :: [(('A, 'α::null) *Bag*, ('A, 'α) *val*)] ⇒ ('A, 'α) *Bag*

**where** *OclExcluding* $x y = (\lambda \tau. \mathit{if} (\delta x) \tau = \mathit{true} \tau \land (v y) \tau = \mathit{true} \tau$

then *Abs-Bag*<sub>base</sub> ⊔ ⌜Rep-Bag<sub>base</sub>(x τ)⌝

else invalid $\tau$)

**notation** *OclExcluding* $(- \rightarrow \mathit{excluding}_{Bag}'(-))$
interpretation *OclExcluding: profile-bin<sub>d-v</sub> OclExcluding*

$\lambda x \ y. \ \mathit{Abs-Bag}_{\mathit{base}} \ \mathop{\sqcup}\nolimits^{\top} \mathit{Rep-Bag}_{\mathit{base}}(x)^{\top}(y:=0::\mathit{nat})\mathop{\sqcup}\nolimits$

*<proof>*

### 2.8.7. Definition: Includes

definition *OclIncludes* :: [(‘A,‘α::null) *Bag*,(‘A,‘α) val] ⇒ ‘A Boolean

where *OclIncludes* $x y = (\lambda \tau. \ if \ (\delta x) \ \tau = true \ \tau \land \ (v y) \ \tau = true \ \tau$
then $\mathop{\sqcup}\nolimits^{\top} \mathit{Rep-Bag}_{\mathit{base}} (x \ \tau)^{\top} (y \ \tau) > 0 \mathop{\sqcup}\nolimits^{\top}$
else $\perp$)

notation *OclIncludes* $\mathop{\neg\neg}\nolimits^{\rightarrow} \mathit{includes}_{\mathit{Bag}}'(-')$

interpretation *OclIncludes* : *profile-bin<sub>d-v</sub> OclIncludes* $\lambda x \ y. \ \mathop{\sqcup}\nolimits^{\top} \mathit{Rep-Bag}_{\mathit{base}} x^{\top} y > 0 \mathop{\sqcup}\nolimits^{\top}$
*<proof>*

### 2.8.8. Definition: Excludes

definition *OclExcludes* :: [(‘A,‘α::null) *Bag*,(‘A,‘α) val] ⇒ ‘A Boolean

where *OclExcludes* $x y = (\mathit{not}(\mathit{OclIncludes*} x y))$

notation *OclExcludes* $\mathop{\neg\neg}\nolimits^{\rightarrow} \mathit{excludes}_{\mathit{Bag}}'(-')$

The case of the size definition is somewhat special, we admit explicitly in Featherweight OCL the
possibility of infinite bags. For the size definition, this requires an extra condition that assures that the
cardinality of the bag is actually a defined integer.

interpretation *OclExcludes* : *profile-bin<sub>d-v</sub> OclExcludes* $\lambda x \ y. \ \mathop{\sqcup}\nolimits^{\top} \mathit{Rep-Bag}_{\mathit{base}} x^{\top} y \le 0 \mathop{\sqcup}\nolimits^{\top}$
*<proof>*

### 2.8.9. Definition: Size

definition *OclSize* :: ('A, 'α::null) *Bag* ⇒ 'A Integer

where *OclSize* $x = (\lambda \tau. \ if \ (\delta x) \ \tau = true \ \tau \land \ finite \ (\mathit{Rep-Bag-base} \ x \ \tau)$
then $\mathop{\sqcup}\nolimits^{\top} \mathit{int} \ (\mathit{card} \ (\mathit{Rep-Bag-base} \ x \ \tau)) \mathop{\sqcup}\nolimits^{\top}$
else $\perp$)

notation

*OclSize* $\mathop{\neg\neg}\nolimits^{\rightarrow} \mathit{size}_{\mathit{Bag}}'(')$

The following definition follows the requirement of the standard to treat null as neutral element of bags. It is a well-documented exception from the general strictness rule and the rule that the distinguished argument itself should be non-null.

### 2.8.10. Definition: IsEmpty

definition *OclIsEmpty* :: ('A,‘α::null) *Bag* ⇒ ‘A Boolean

where *OclIsEmpty* $x = ((v x \ and \ not \ (\delta x)) \ or \ ((\mathit{OclSize} \ x) \dotfill 0))$

notation *OclIsEmpty* $\mathop{\neg\neg}\nolimits^{\rightarrow} \mathit{isEmpty}_{\mathit{Bag}}'(')$

### 2.8.11. Definition: NotEmpty

definition *OclNotEmpty* :: ('A,‘α::null) *Bag* ⇒ ‘A Boolean

where *OclNotEmpty* $x = \mathit{not}(\mathit{OclIsEmpty*} x)$

notation *OclNotEmpty* $\mathop{\neg\neg}\nolimits^{\rightarrow} \mathit{notEmpty}_{\mathit{Bag}}'(')$

### 2.8.12. Definition: Any

definition *OclANY* :: [(‘A,‘α::null) *Bag*] ⇒ ‘A Boolean

where *OclANY* $x = (\lambda \tau. \ if \ (v x) \ \tau = true \ \tau$
then if (δ x and *OclNotEmpty* x) τ = true τ
then SOME y. y ∈ (Rep-Set-base x τ)

else null τ

else ⊥)

**notation** OclANY (-->any<sub>Bag</sub>'(')

### 2.8.13. Definition: Forall

The definition of OclForall mimics the one of op and: OclForall is not a strict operation.

**definition** OclForall :: [(‘A,‘α::null)Bag, (‘A,‘α)val⇒(‘A)Boolean] ⇒ ‘A Boolean

**where** OclForall S P = (λ τ. if (δ S) τ = true τ
then if (∃ x ∈ Rep-Set-base S τ. P (λ-. x) τ = false τ)
then false τ
else if (∃ x ∈ Rep-Set-base S τ. P (λ-. x) τ = invalid τ)
then invalid τ
else if (∃ x ∈ Rep-Set-base S τ. P (λ-. x) τ = null τ)
then null τ
else true τ
else ⊥)

**syntax**

-OclForallBag :: [(‘A,‘α::null) Bag,id,(‘A)Boolean] ⇒ ‘A Boolean ((-)→forallAll<sub>Bag</sub>'(-|-'))

**translations**

X->forallAll<sub>Bag</sub>(x | P) == CONST UML-Bag.OclForall X (%x. P)

### 2.8.14. Definition: Exists

Like OclForall, OclExists is also not strict.

**definition** OclExists :: [(‘A,‘α::null) Bag, (‘A,‘α)val⇒(‘A)Boolean] ⇒ ‘A Boolean

**where** OclExists S P = not(UML-Bag.OclForall S (λ X. not (P X)))

**syntax**

-OclExistBag :: [(‘A,‘α::null) Bag,id,(‘A)Boolean] ⇒ ‘A Boolean ((-)→exists<sub>Bag</sub>'(-|-'))

**translations**

X->exists<sub>Bag</sub>(x | P) == CONST UML-Bag.OclExists X (%x. P)

### 2.8.15. Definition: Iterate

**definition** OclIterate :: [(‘A,‘α::null) Bag, (‘A,‘β::null)val,

(‘A,‘α)val⇒(‘A,‘β)val⇒(‘A,‘β)val] ⇒ (‘A,‘β)val

**where** OclIterate S A F = (λ τ. if (δ S) τ = true τ ∧ (v A) τ = true τ ∧ finite (Rep-Bag-base S τ)
then Finite-Set-fold (F o (λa τ. a) o fst) A (Rep-Bag-base S τ) τ
else ⊥)

**syntax**

-OclIterateBag :: [(‘A,‘α::null) Bag, idt, idt, ‘α, ‘β] => (‘A,‘γ)val

(- ->iterate<sub>Bag</sub>'(-;-=| -'))

**translations**

X->iterate<sub>Bag</sub>(a; x = A | P) == CONST OclIterate X A (%a. (% x. P))

### 2.8.16. Definition: Select

**definition** OclSelect :: [(‘A,‘α::null)Bag, (‘A,‘α)val⇒(‘A)Boolean] ⇒ (‘A,‘α)Bag

**where** OclSelect S P = (λτ. if (δ S) τ = true τ
then if (∃ x ∈ Rep-Set-base S τ. P(λ -. x) τ = invalid τ)
then invalid τ
else Abs-Bag<sub>base</sub> ⊔λx.

let n = ⊑ Rep-Bag<sub>base</sub> (S τ) ⊕ x in

if n = 0 | P (λ-. x) τ = false τ then
0
else
  $n_{\perp}$
else invalid $\tau$)

**syntax**

-OclSelectBag :: [('A, 'α::null) Bag, id, ('A) Boolean] ⇒ 'A Boolean ((-) → selectBag' (-|-'))

**translations**

$X \rightarrow select_{Bag}(x | P) == CONST OclSelect X (\% x. P)$

## 2.8.17. Definition: Reject

**definition** OclReject :: [('A, 'α::null) Bag, ('A, 'α) val ⇒ ('A) Boolean] ⇒ ('A, 'α::null) Bag

where $OclReject S P = OclSelect S (\text{not o } P)$

**syntax**

-OclRejectBag :: [('A, 'α::null) Bag, id, ('A) Boolean] ⇒ 'A Boolean ((-) → rejectBag' (-|-'))

**translations**

$X \rightarrow reject_{Bag}(x | P) == CONST OclReject X (\% x. P)$

## 2.8.18. Definition: IncludesAll

**definition** OclIncludesAll :: [('A, 'α::null) Bag, ('A, 'α) Bag] ⇒ 'A Boolean

**where** $OclIncludesAll x y = (\lambda \tau. \text{ if } (\delta x) \tau = \text{true} \quad \tau \wedge (\delta y) \tau = \text{true} \quad \tau$
\quad then $\perp \text{ Rep-Bag-base } y \quad \tau \subseteq \text{ Rep-Bag-base } x \quad \tau \perp$
\quad else $\perp$)

**notation** $OclIncludesAll (\dashrightarrow includesAll_{Bag}' (-'))$

**interpretation** $OclIncludesAll : \text{profile-bin}_{d-d} OclIncludesAll \lambda x y. \perp \text{ Rep-Bag-base}' y \subseteq \text{ Rep-Bag-base}' x \perp$
$\langle\text{proof}\rangle$

## 2.8.19. Definition: ExcludesAll

**definition** OclExcludesAll :: [('A, 'α::null) Bag, ('A, 'α) Bag] ⇒ 'A Boolean

**where** $OclExcludesAll x y = (\lambda \tau. \text{ if } (\delta x) \tau = \text{true} \quad \tau \wedge (\delta y) \tau = \text{true} \quad \tau$
\quad then $\perp \text{ Rep-Bag-base } y \quad \tau \cap \text{ Rep-Bag-base } x \quad \tau = \emptyset \perp$
\quad else $\perp$)

**notation** $OclExcludesAll (\dashrightarrow excludesAll_{Bag}' (-'))$

**interpretation** $OclExcludesAll : \text{profile-bin}_{d-d} OclExcludesAll \lambda x y. \perp \text{ Rep-Bag-base}' y \cap \text{ Rep-Bag-base}' x =$
$\{\perp\}$
$\langle\text{proof}\rangle$

## 2.8.20. Definition: Union

**definition** OclUnion :: [('A, 'α::null) Bag, ('A, 'α) Bag] ⇒ ('A, 'α) Bag

**where** $OclUnion x y = (\lambda \tau. \text{ if } (\delta x) \tau = \text{true} \quad \tau \wedge (\delta y) \tau = \text{true} \quad \tau$
\quad then $\text{Abs-Bag}_{\text{base}} \perp \lambda X. \text{ Rep-Bag}_{\text{base}} (x \quad \tau)^{\top} X +$
\quad \qquad $\text{ Rep-Bag}_{\text{base}} (y \quad \tau)^{\top} X_{\perp}$
\quad else invalid $\tau)$

**notation** $OclUnion (\dashrightarrow union_{Bag}' (-'))$

**interpretation** $OclUnion :$
$\text{profile-bin}_{d-d} \text{ OclUnion } \lambda x y. \text{ Abs-Bag}_{\text{base}} \perp \lambda X. \text{ Rep-Bag}_{\text{base}} x^\top X +$
$\qquad \text{ Rep-Bag}_{\text{base}} y^\top X_{\perp}$

$\langle\text{proof}\rangle$

## 2.8.21. Definition: Intersection

**definition** OclIntersection :: [('A, 'α::null) Bag, ('A, 'α) Bag] ⇒ ('A, 'α) Bag
**where**
$$ \mathit{OclIntersection} x y = (\lambda \tau. \mathit{if} (\delta x) \tau = \mathit{true} \tau \land (\delta y) \tau = \mathit{true} \tau \mathit{then} \mathit{Abs-Bag}_{\mathit{base}_{\perp}} \lambda X. \mathit{min} (\mathit{\uparrow Rep-Bag}_{\mathit{base}} (x \tau)^{\top} X) (\mathit{\uparrow Rep-Bag}_{\mathit{base}} (y \tau)^{\top} X)_{\perp} \mathit{else} \perp ) $$

**notation**
$$ \mathit{OclIntersection}(\mathit{-->}\mathit{intersection}_{\mathit{Bag}'}(-') ) $$

**interpretation**
$$ \mathit{OclIntersection} : \mathit{profile-bin}_{d-d} \mathit{OclIntersection} \lambda x y. \mathit{Abs-Bag}_{\mathit{base}_{\perp}} \lambda X. \mathit{min} (\mathit{\uparrow Rep-Bag}_{\mathit{base}} x^{\top} X) (\mathit{\uparrow Rep-Bag}_{\mathit{base}} y^{\top} X)_{\perp} $$
$$ \langle \mathit{proof} \rangle $$

## 2.8.22. Definition: Count

**definition**
$$ \mathit{OclCount} :: [(\mathfrak{A},'\alpha::\mathit{null}) \mathit{Bag}, (\mathfrak{A}','\alpha) \mathit{val}] \Rightarrow (\mathfrak{A}) \mathit{Integer} $$

**where**
$$ \mathit{OclCount} x y = (\lambda \tau. \mathit{if} (\delta x) \tau = \mathit{true} \tau \land (\delta y) \tau = \mathit{true} \tau \mathit{then} \mathit{\perp} \mathit{int}(\mathit{\uparrow Rep-Bag}_{\mathit{base}} (x \tau)^{\top} (y \tau))_{\perp} \mathit{else} \mathit{invalid} \tau) $$

**notation**
$$ \mathit{OclCount}(\mathit{-->}\mathit{count}_{\mathit{Bag}'}(-') ) $$

**interpretation**
$$ \mathit{OclCount} : \mathit{profile-bin}_{d-d} \mathit{OclCount} \lambda x y. \mathit{\perp} \mathit{int}(\mathit{\uparrow Rep-Bag}_{\mathit{base}} x^{\top} y)_{\perp} $$
$$ \langle \mathit{proof} \rangle $$

## 2.8.23. Definition (future operators)

**consts**
$$ \mathit{OclSum} ::= (\mathfrak{A},'\alpha::\mathit{null}) \mathit{Bag} \Rightarrow \mathfrak{A} \mathit{Integer} $$

**notation**
$$ \mathit{OclSum}(\mathit{-->}\mathit{sum}_{\mathit{Bag}'}(-') ) $$

## 2.8.24. Test Statements

**instantiation**
$$ \mathit{Bag}_{\mathit{base}} ::= (\mathit{equal})\mathit{equal} $$

**begin**

**definition**
$$ \mathit{HOL equal} k l \leftrightarrow (k::(\mathit{a}::\mathit{equal})\mathit{Bag}_{\mathit{base}}) = l $$

**instance**
$$ \langle \mathit{proof} \rangle $$

**end**

**lemma**
$$ \mathit{equal-Bag}_{\mathit{base}}\text{-code [code]}: \mathit{HOL equal} k (l::(\mathit{a}::\{\mathit{equal},\mathit{null}\})\mathit{Bag}_{\mathit{base}}) \leftrightarrow \mathit{Rep-Bag}_{\mathit{base}} k = \mathit{Rep-Bag}_{\mathit{base}} l $$
$$ \langle \mathit{proof} \rangle $$

**Assert**
$$ \tau \models (\mathit{Bag}\{\}) \doteq \mathit{Bag}\{\} $$

**end**

**theory**
$$ \mathit{UML-Set} $$

**imports**
$$ \text{../basic-types/UML-Void} $$

```
../basic-types/UML-Boolean
```

```
../basic-types/UML-Integer
```

```
../basic-types/UML-String
```

```
../basic-types/UML-Real
```
begin

no-notation None (⊥)

## 2.9. Collection Type Set: Operations

### 2.9.1. As a Motivation for the (infinite) Type Construction: Type-Extensions as Sets

Our notion of typed set goes beyond the usual notion of a finite executable set and is powerful enough to capture the extension of a type in UML and OCL. This means we can have in Featherweight OCL Sets containing all possible elements of a type, not only those (finite) ones representable in a state. This holds for base types as well as class types, although the notion for class-types — involving object id's not occuring in a state — requires some care.

In a world with invalid and null, there are two notions extensions possible:

1. the set of all *defined* values of a type *T* (for which we will introduce the constant *T*)

2. the set of all *valid* values of a type *T*, so including *null* (for which we will introduce the constant *Tnull*).

We define the set extensions for the base type *Integer* as follows:

**definition** $Integer :: ('A, Integer_{base}) Set$

**where** $Integer \equiv (\lambda \tau. (\text{Abs-Set}_{\text{base}} \text{ o Some o Some}) ((\text{Some o Some}) \text{ ' (UNIV::int set)}))$

**definition** $Integer_{null} :: ('A, Integer_{base}) Set$

**where** $Integer_{null} \equiv (\lambda \tau. (\text{Abs-Set}_{\text{base}} \text{ o Some o Some}) (\text{Some ' (UNIV::int option set)}))$

**lemma** $Integer-defined : \delta Integer = true$

⟨proof⟩

**lemma** $Integer_{null-defined} : \delta Integer_{null} = true$

⟨proof⟩

This allows the theorems:

$\tau \models \delta x \implies \tau \models (Integer->includes_{Set}(x)) \quad \tau \models \delta x \implies \tau \models Integer \triangleq (Integer->including_{Set}(x))$

$\tau \models \nu x \implies \tau \models (Integer_{null->includes_{Set}}(x)) \quad \tau \models \nu x \implies \tau \models Integer_{null} \triangleq (Integer_{null->including_{Set}}(x))$

which characterize the infiniteness of these sets by a recursive property on these sets.

In the same spirit, we proceed similarly for the remaining base types:

**definition** $Void_{null} :: ('A, Void_{base}) Set$

**where** $Void_{null} \equiv (\lambda \tau. (\text{Abs-Set}_{\text{base}} \text{ o Some o Some}) \{\text{Abs-Void}_{\text{base}} (\text{Some None})\})$

**definition** $Void_{empty} :: ('A, Void_{base}) Set$

**where** $Void_{empty} \equiv (\lambda \tau. (\text{Abs-Set}_{\text{base}} \text{ o Some o Some}) \{\})$

**lemma** $Void_{null-defined} : \delta Void_{null} = true$

⟨proof⟩

**lemma** $Void_{empty-defined} : \delta Void_{empty} = true$

⟨proof⟩

**lemma** assumes $\tau \models \delta (V :: ('A, Void_{base}) Set)$
**shows** $\tau \models V \triangleq \text{Void}_{\text{null}} \lor \tau \models V \triangleq \text{Void}_{\text{empty}}$

*Proof*

**definition** Boolean :: ('A,Boolean$_{base}$) Set

**where** Boolean $\equiv (\lambda \tau. (\text{Abs-Set}_{\text{base}} \text{ o Some o Some}) ((\text{Some o Some}) \text{ ' (UNIV::bool set)}))$

**definition** Boolean$_{null}$ :: ('A,Boolean$_{base}$) Set

**where** Boolean$_{null}$ $\equiv (\lambda \tau. (\text{Abs-Set}_{\text{base}} \text{ o Some o Some}) (\text{Some ' (UNIV::bool option set)}))$

**lemma** Boolean-defined : $\delta$ Boolean = true
*Proof*

**lemma** Boolean$_{null}$-defined : $\delta$ Boolean$_{null}$ = true
*Proof*

**definition** String :: ('A,String$_{base}$) Set

**where** String $\equiv (\lambda \tau. (\text{Abs-Set}_{\text{base}} \text{ o Some o Some}) ((\text{Some o Some}) \text{ ' (UNIV::string set)}))$

**definition** String$_{null}$ :: ('A,String$_{base}$) Set

**where** String$_{null}$ $\equiv (\lambda \tau. (\text{Abs-Set}_{\text{base}} \text{ o Some o Some}) (\text{Some ' (UNIV::string option set)}))$

**lemma** String-defined : $\delta$ String = true
*Proof*

**lemma** String$_{null}$-defined : $\delta$ String$_{null}$ = true
*Proof*

**definition** Real :: ('A,Real$_{base}$) Set

**where** Real $\equiv (\lambda \tau. (\text{Abs-Set}_{\text{base}} \text{ o Some o Some}) ((\text{Some o Some}) \text{ ' (UNIV::real set)}))$

**definition** Real$_{null}$ :: ('A,Real$_{base}$) Set

**where** Real$_{null}$ $\equiv (\lambda \tau. (\text{Abs-Set}_{\text{base}} \text{ o Some o Some}) (\text{Some ' (UNIV::real option set)}))$

**lemma** Real-defined : $\delta$ Real = true
*Proof*

**lemma** Real$_{null}$-defined : $\delta$ Real$_{null}$ = true
*Proof*

## 2.9.2. Basic Properties of the Set Type

Every element in a defined set is valid.

**lemma** Set-inv-lemma: $\tau \models (\delta X) \implies \forall x \in \mathbb{T} \text{Rep-Set}_{\text{base}} (X \tau)^{\mathbb{T}}$. $x \neq \text{bot}$
*Proof*

**lemma** Set-inv-lemma':

assumes $x\text{-def} : \tau \models \delta X$

and $e\text{-mem} : e \in \mathbb{T} \text{Rep-Set}_{\text{base}} (X \tau)^{\mathbb{T}}$

shows $\tau \models v (\lambda-. e)$

*Proof*

**lemma** abs-rep-simp':

assumes $S\text{-all-def} : \tau \models \delta S$

shows $\text{Abs-Set}_{\text{base}} \mathbb{T} \text{Rep-Set}_{\text{base}} (S \tau)^{\mathbb{T}} = S \tau$
*Proof*

**lemma** S-lift':
assumes S-all-def : (τ :: 'A st) |- δ S

shows ∃S'. (λa (::: 'A st). a) 'Rep-Setbase (S τ)⊤ = (λa (::: 'A st). ⌢a] ) 'S'
<proof>

lemma invalid-set-OclNot-defined [simp,code-unfold]:δ(invalid::('A,'α::null) Set) = false <proof>

lemma null-set-OclNot-defined [simp,code-unfold]:δ(null::('A,'α::null) Set) = false
<proof>

lemma invalid-set-valid [simp,code-unfold]:v(invalid::('A,'α::null) Set) = false
<proof>

lemma null-set-valid [simp,code-unfold]:v(null::('A,'α::null) Set) = true
<proof>

... which means that we can have a type ('A, ('A, ('A) Integer) Set) Set corresponding exactly to Set/Set Integer) in OCL notation. Note that the parameter 'A still refers to the object universe; making the OCL semantics entirely parametric in the object universe makes it possible to study (and prove) its properties independently from a concrete class diagram.

2.9.3. Definition: Strict Equality

After the part of foundational operations on sets, we detail here equality on sets. Strong equality is
inherited from the OCL core, but we have to consider the case of the strict equality. We decide to
overload strict equality in the same way we do for other value's in OCL:

def s (overloaded) StrictRefEqS et :

$$
\begin{align*}
(x::('\mathfrak{A}, ('\mathfrak{A}, ('\mathfrak{A}) \text{Integer}) \text{Set}) \text{Set} :
  & y \equiv \lambda \tau. \text{if } (v x) \tau = \text{true } \tau \land (v y) \tau = \text{true } \tau \\
  & \text{then } (x \triangleq y)\tau \\
  & \text{else invalid } \tau
\end{align*}
$$

One might object here that for the case of objects, this is an empty definition. The answer is no,
we will restrain later on states and objects such that any object has its oid stored inside the object (so
the ref, under which an object can be referenced in the store will represented in the object itself). For
such well-formed stores that satisfy this invariant (the WFF-invariant), the referential equality and the
strong equality—and therefore the strict equality on sets in the sense above—coincides.

Property proof in terms of profile-bin$_{StrongEq-v-v}$

interpretation StrictRefEqSet : profile-bin$_{StrongEq-v-v}$ λ x y. (x::('A,'α::null)Set) = y
<proof>

2.9.4. Constants: mtSet

definition mtSet::('A,'α::null) Set (Set{})

where Set{} ≡ (λ τ. Abs-Set<sub>base</sub> ⌢ {}::'α set<sub>⊥</sub> )

lemma mtSet-defined[simp,code-unfold]:δ(set{}) = true
<proof>

lemma mtSet-valid[simp,code-unfold]:v(set{}) = true
<proof>

lemma mtSet-rep-set: $\top \mathrm{Rep-Set}_{\mathrm{base}} (\mathrm{Set}\{\}) \top = \{\}$
<proof>

lemma [simp,code-unfold]: const Set{}
<proof>

Note that the collection types in OCL allow for null to be included; however, there is the null-collection
into which inclusion yields invalid.
### 2.9.5. Definition: Including

**definition** *OclIncluding* :: [(('A', 'α::null) Set, ('A', 'α') val] ⇒ ('A', 'α') Set

**where** *OclIncluding* x y = (λ τ. if (δ x) τ = true τ ∧ (υ y) τ = true τ
then Abs-Set<sub>base</sub> ⊔<sup>⊤</sup>Rep-Set<sub>base</sub> (x τ)<sup>Π</sup> ∪ {y τ} ⊔
else invalid τ)

**notation** *OclIncluding* (->*includingSet*`'(-)'*)

**interpretation** *OclIncluding* : profile-bin<sub>d-v</sub> *OclIncluding* λx y. Abs-Set<sub>base</sub><sub>⊥</sub><sup>⊤</sup>Rep-Set<sub>base</sub> x<sup>Π</sup> ∪ {y}⊥
<proof>

**syntax**

`-OclFinset :: args => ('A, 'a::null) Set (Set{(-)})`

**translations**

`Set{x, xs} == CONST OclIncluding (Set{xs}) x`

`Set{x} == CONST OclIncluding (Set{}) x`

### 2.9.6. Definition: Excluding

**definition** *OclExcluding* :: [(('A', 'α::null) Set, ('A', 'α') val] ⇒ ('A', 'α') Set

**where** *OclExcluding* x y = (λ τ. if (δ x) τ = true τ ∧ (υ y) τ = true τ
then Abs-Set<sub>base</sub> ⊔<sup>⊤</sup>Rep-Set<sub>base</sub> (x τ)<sup>Π</sup> - {y τ} ⊔
else ⊥)

**notation** *OclExcluding* (->*excludingSet*`'(-)'*)

**lemma** *OclExcluding-inv*: (x:: Set('b::{null})) ≠ ⊥ = ⇒ x ≠ null = ⇒ y ≠ ⊥ = ⇒
  ⊔<sup>⊤</sup>Rep-Set<sub>base</sub> x<sup>Π</sup> - {y}⊥ ∈ {X. X = bot ∨ X = null ∨ (∀x∈<sup>Π</sup>X<sup>Π</sup>. x ≠ bot)}
<proof>

**interpretation** *OclExcluding* : profile-bin<sub>d-v</sub> *OclExcluding* λx y. Abs-Set<sub>base</sub><sub>⊥</sub><sup>⊤</sup>Rep-Set<sub>base</sub> x<sup>Π</sup> - {y}⊥
<proof>

### 2.9.7. Definition: Includes

**definition** *OclIncludes* :: [(('A', 'α::null) Set, ('A', 'α') val] ⇒ 'A Boolean

**where** *OclIncludes* x y = (λ τ. if (δ x) τ = true τ ∧ (υ y) τ = true τ
then ⊔<sup>⊤</sup>(y τ) ∈ <sup>⊤</sup>Rep-Set<sub>base</sub> (x τ)<sup>Π</sup> ⊔
else ⊥)

**notation** *OclIncludes* (->*includesSet*`'(-)'*)

**interpretation** *OclIncludes* : profile-bin<sub>d-v</sub> *OclIncludes* λx y. ⊔<sup>⊤</sup>y ∈ <sup>⊤</sup>Rep-Set<sub>base</sub> x<sup>Π</sup> ⊔
<proof>

### 2.9.8. Definition: Excludes

**definition** *OclExcludes* :: [(('A', 'α::null) Set, ('A', 'α') val] ⇒ 'A Boolean

**where** *OclExcludes* x y = (not(*OclIncludes* x y))

**notation** *OclExcludes* (->*excludesSet*`'(-)'*)

The case of the size definition is somewhat special, we admit explicitly in Featherweight OCL the
possibility of infinite sets. For the size definition, this requires an extra condition that assures that the
cardinality of the set is actually a defined integer.

**interpretation** *OclExcludes* : profile-bin<sub>d-v</sub> *OclExcludes* λx y. ⊔<sup>⊤</sup>y ∉ <sup>⊤</sup>Rep-Set<sub>base</sub> x<sup>Π</sup> ⊔
<proof>
### 2.9.9. Definition: Size

**definition** `OclSize` :: (`'A', 'α::null`) Set ⇒ `'A` Integer

**where** `OclSize x` = (`λ τ. if (δ x) τ = true τ ∧ finite(⊤Rep-Set<sub>base</sub> (x τ)<sup>Π</sup>)`
then `⊥` int `card (⊤Rep-Set<sub>base</sub> (x τ)<sup>Π</sup>)` `⊥`
else `⊥`)

**notation**

`OclSize (->size<sub>Set</sub>'('))`

The following definition follows the requirement of the standard to treat null as neutral element of sets. It is a well-documented exception from the general strictness rule and the rule that the distinguished argument self should be non-null.

### 2.9.10. Definition: IsEmpty

**definition** `OclIsEmpty` :: (`'A', 'α::null`) Set ⇒ `'A` Boolean

**where** `OclIsEmpty x` = `((v x and not (δ x)) or ((OclSize x) = 0))`

**notation** `OclIsEmpty'(')`

### 2.9.11. Definition: NotEmpty

**definition** `OclNotEmpty` :: (`'A', 'α::null`) Set ⇒ `'A` Boolean

**where** `OclNotEmpty x` = `not(OclIsEmpty x)`

**notation** `OclNotEmpty'(')`

### 2.9.12. Definition: Any

**definition** `OclANY` :: `[(`'A', 'α::null`) Set] ⇒ (`'A', 'α`) val

**where** `OclANY x` = (`λ τ. if (v x) τ = true τ`
then if (`δ x` and `OclNotEmpty x`) τ = true τ
then `SOME y. y ∈ ⊤Rep-Set<sub>base</sub> (x τ)<sup>Π</sup>`
else null τ
else `⊥`)

**notation** `OclANY'(')`

### 2.9.13. Definition: Forall

The definition of `OclForall` mimics the one of `op` and: `OclForall` is not a strict operation.

**definition** `OclForall` :: `[(`'A', 'α::null`) Set, (`'A', 'α`) val] ⇒ (`'A`) Boolean

**where** `OclForall S P` = (`λ τ. if (`δ S`) τ = true τ`
then if (`∃ x ∈ ⊤Rep-Set<sub>base</sub> (S τ)<sup>Π</sup>`. P(`λ -. x`) τ = false τ)
then false τ
else if (`∃ x ∈ ⊤Rep-Set<sub>base</sub> (S τ)<sup>Π</sup>`. P(`λ -. x`) τ = invalid τ)
then invalid τ
else if (`∃ x ∈ ⊤Rep-Set<sub>base</sub> (S τ)<sup>Π</sup>`. P(`λ -. x`) τ = null τ)
then null τ
else true τ
else `⊥`)

**syntax**

`-OclForallSet :: [(`'A', 'α::null`) Set, id, (`'A`) Boolean] ⇒ ('A` Boolean `((->forall<sub>Set</sub>'(`-|`))`)

**translations**

`X->forall<sub>Set</sub>(x | P) == CONST UML-Set.OclForall X (%x. P)`

### 2.9.14. Definition: Exists

Like `OclForall`, `OclExists` is also not strict.

**definition** `OclExists` :: `[(`'A', 'α::null`) Set, (`'A', 'α`) val] ⇒ (`'A`) Boolean
where $\mathit{OclExists} S P = \mathit{not}(\mathit{UML-Set.OclForall} S (\lambda X. \mathit{not}(P X)))$

### syntax

- $\mathit{OclExistSet} :: [(\mathfrak{A},'\alpha::\mathit{null}) \mathit{Set}, id, ('\mathfrak{A})\mathit{Boolean}] \Rightarrow ('\mathfrak{A})\mathit{Boolean} ((-) \rightarrow \mathit{exists}_{\mathit{Set}}'(-|-'))$

### translations

$X \rightarrow \mathit{exists}_{\mathit{Set}}(x | P) == \mathit{CONST UML-Set.OclExists} X (\%x. P)$

## 2.9.15. Definition: Iterate

definition $\mathit{OclIterate} :: [(\mathfrak{A},'\alpha::\mathit{null}) \mathit{Set}, ('\mathfrak{A}','\beta::\mathit{null})\mathit{val},$

$$ ('\mathfrak{A}', '\alpha)\mathit{val} \Rightarrow ('\mathfrak{A}', '\beta)\mathit{val} \Rightarrow ('\mathfrak{A}', '\beta)\mathit{val} \Rightarrow ('\mathfrak{A}', '\beta)\mathit{val} $$

where $\mathit{OclIterate} S A F = (\lambda \tau. \mathit{if} (\delta S) \tau = \mathit{true} \tau \wedge (v A) \tau = \mathit{true} \tau \wedge \mathit{finite}^{\top} \mathit{Rep-Set}_{\mathit{base}} (S \tau)^{\top} \\ \mathit{then} (\mathit{Finite-Set.fold} (F) (A) ((\lambda a. \tau. a) \mathit{ Rep-Set}_{\mathit{base}} (S \tau)^{\top})) \tau \\ \mathit{else} \perp)$

### syntax

- $\mathit{OclIterateSet} :: [(\mathfrak{A},'\alpha::\mathit{null}) \mathit{Set}, id, idt, '\alpha, '\beta] \Rightarrow ('\mathfrak{A}','\gamma)\mathit{val}$

$$ (\mathit{--}) \rightarrow \mathit{iterate}_{\mathit{Set}}'(-;=-|-|-') $$

### translations

$X \rightarrow \mathit{iterate}_{\mathit{Set}}(a; x = A | P) == \mathit{CONST OclIterate} X A (\%a. (\% x. P))$

## 2.9.16. Definition: Select

definition $\mathit{OclSelect} :: [(\mathfrak{A},'\alpha::\mathit{null})\mathit{Set}, ('\mathfrak{A}','\alpha)\mathit{val} \Rightarrow ('\mathfrak{A})\mathit{Boolean}] \Rightarrow ('\mathfrak{A}','\alpha)\mathit{Set}$

where $\mathit{OclSelect} S P = (\lambda \tau. \mathit{if} (\delta S) \tau = \mathit{true} \tau$

$$ \mathit{then} \ if \ (\exists x \in^{\top} \mathit{Rep-Set}_{\mathit{base}} (S \tau)^{\top}. P(\lambda-.x) \tau = \mathit{invalid} \tau) $$

$\mathit{then} \ invalid \ \tau$

$$ \mathit{else} \ \mathit{Abs-Set}_{\mathit{base}} \llcorner \{x \in^{\top} \mathit{Rep-Set}_{\mathit{base}} (S \tau)^{\top}. P (\lambda-.x) \tau \neq \mathit{false} \tau\}_{\llcorner} $$

$\mathit{else} \ invalid \ \tau$

### syntax

- $\mathit{OclSelectSet} :: [(\mathfrak{A},'\alpha::\mathit{null}) \mathit{Set}, id, ('\mathfrak{A})\mathit{Boolean}] \Rightarrow ('\mathfrak{A})\mathit{Boolean} ((-) \rightarrow \mathit{select}_{\mathit{Set}}'(-|-'))$

### translations

$X \rightarrow \mathit{select}_{\mathit{Set}}(x | P) == \mathit{CONST OclSelect} X (\% x. P)$

## 2.9.17. Definition: Reject

definition $\mathit{OclReject} :: [(\mathfrak{A},'\alpha::\mathit{null})\mathit{Set}, ('\mathfrak{A}','\alpha)\mathit{val} \Rightarrow ('\mathfrak{A})\mathit{Boolean}] \Rightarrow ('\mathfrak{A}','\alpha::\mathit{null})\mathit{Set}$

where $\mathit{OclReject} S P = \mathit{OclSelect} S (\mathit{not} \ o \ P)$

### syntax

- $\mathit{OclRejectSet} :: [(\mathfrak{A},'\alpha::\mathit{null}) \mathit{Set}, id, ('\mathfrak{A})\mathit{Boolean}] \Rightarrow ('\mathfrak{A})\mathit{Boolean} ((-) \rightarrow \mathit{reject}_{\mathit{Set}}'(-|-'))$

### translations

$X \rightarrow \mathit{reject}_{\mathit{Set}}(x | P) == \mathit{CONST OclReject} X (\% x. P)$

## 2.9.18. Definition: IncludesAll

definition $\mathit{OclIncludesAll} :: [(\mathfrak{A},'\alpha::\mathit{null}) \mathit{Set}, ('\mathfrak{A}','\alpha) \mathit{Set}] \Rightarrow ('\mathfrak{A})\mathit{Boolean}$

where $\mathit{OclIncludesAll} x y = (\lambda \tau. \mathit{if} (\delta x) \tau = \mathit{true} \ \tau \wedge (\delta y) \tau = \mathit{true} \ \tau$

$$ \mathit{then} \ \llcorner^{\top} \mathit{Rep-Set}_{\mathit{base}} (y \ \tau)^{\top} \subseteq \llcorner^{\top} \mathit{Rep-Set}_{\mathit{base}} (x \ \tau)^{\top} \llcorner $$

$\mathit{else} \ \perp$)

notation $\mathit{OclIncludesAll} (\mathit{-->} \mathit{includesAll}_{\mathit{Set}}'(-'))$

interpretation $\mathit{OclIncludesAll} : \mathit{profile-bin}_d \rightarrow \mathit{OclIncludesAll} \ \lambda x \ y. \llcorner^{\top} \mathit{Rep-Set}_{\mathit{base}} \ y^{\top} \subseteq \llcorner^{\top} \mathit{Rep-Set}_{\mathit{base}} \ x^{\top} \llcorner \langle \mathit{proof} \rangle$

## 2.9.19. Definition: ExcludesAll

definition $\mathit{OclExcludesAll} :: [(\mathfrak{A},'\alpha::\mathit{null}) \mathit{Set}, ('\mathfrak{A}','\alpha) \mathit{Set}] \Rightarrow ('\mathfrak{A})\mathit{Boolean}$

where $\mathit{OclExcludesAll} x y = (\lambda \tau. \mathit{if} (\delta x) \tau = \mathit{true} \ \tau \wedge (\delta y) \tau = \mathit{true} \ \tau$

$$ \mathit{then} \ \llcorner^{\top} \mathit{Rep-Set}_{\mathit{base}} (y \ \tau)^{\top} \cap \llcorner^{\top} \mathit{Rep-Set}_{\mathit{base}} (x \ \tau)^{\top} = \{\} \llcorner $$
else $\perp$ )

notation OclExcludesAll ( $\rightarrow$ excludesAll$_{Set}$( $\rightarrow$ (-') ) )

interpretation OclExcludesAll : profile-bin$_{d}$-$_{d}$ OclExcludesAll $\lambda x y. \llcorner$ $^{\top}$Rep-Set$_{base}$ $y^{\top}$ $\cap$ $^{\top}$Rep-Set$_{base}$ $x^{\top}$ =
${}^{|}$
<proof>

2.9.20. Definition: Union

definition OclUnion :: [('A, 'a::null) Set, ('A, 'a) Set] $\Rightarrow$ ('A, 'a) Set

where
OclUnion $x y = (\lambda \tau. \text{ if } (\delta x) \tau = \text{ true } \tau \land (\delta y) \tau = \text{ true } \tau$
\quad then $\text{Abs-Set}_{\text{base}\llcorner}^{\top} \text{Rep-Set}_{\text{base}} (y \tau)^{\top} \cup \top \text{Rep-Set}_{\text{base}} (x \tau)^{\top} \urcorner$
\quad else $\perp$ )

notation OclUnion ( $\rightarrow$ union$_{Set}$ '(-') )

lemma OclUnion-inv: (x:: Set('b::{null})) \neq \perp \Rightarrow x \neq null \Rightarrow y \neq \perp \Rightarrow y \neq null \Rightarrow \llcorner
\top \text{Rep-Set}_{\text{base}} y^{\top} \cup \top \text{Rep-Set}_{\text{base}} x^{\top} \urcorner \in \{X. X = \text{bot} \lor X = \text{null} \lor (\forall x \in \top X^{\top}. x \neq \text{bot})\}
\text{<proof>}

interpretation OclUnion : profile-bin$_{d}$-$_{d}$ OclUnion $\lambda x y. \text{Abs-Set}_{\text{base}\llcorner}^{\top} \text{Rep-Set}_{\text{base}} y^{\top} \cup \top \text{Rep-Set}_{\text{base}} x^{\top} \urcorner$
<proof>

2.9.21. Definition: Intersection

definition OclIntersection :: [('A, 'a::null) Set, ('A, 'a) Set] $\Rightarrow$ ('A, 'a) Set

where
OclIntersection $x y = (\lambda \tau. \text{ if } (\delta x) \tau = \text{ true } \tau \land (\delta y) \tau = \text{ true } \tau$
\quad then $\text{Abs-Set}_{\text{base}\llcorner}^{\top} \text{Rep-Set}_{\text{base}} (y \tau)^{\top}$
\quad $\cap \top \text{Rep-Set}_{\text{base}} (x \tau)^{\top} \urcorner$
\quad else $\perp$ )

notation OclIntersection( $\rightarrow$ intersection$_{Set}$ '(-') )

lemma OclIntersection-inv: (x:: Set('b::{null})) \neq \perp \Rightarrow x \neq null \Rightarrow y \neq \perp \Rightarrow y \neq null \Rightarrow \llcorner
\top \text{Rep-Set}_{\text{base}} y^{\top} \cap \top \text{Rep-Set}_{\text{base}} x^{\top} \urcorner \in \{X. X = \text{bot} \lor X = \text{null} \lor (\forall x \in \top X^{\top}. x \neq \text{bot})\}
\text{<proof>}

interpretation OclIntersection : profile-bin$_{d}$-$_{d}$ OclIntersection $\lambda x y. \text{Abs-Set}_{\text{base}\llcorner}^{\top} \text{Rep-Set}_{\text{base}} y^{\top} \cap$
$^{\top}$Rep-Set$_{base}$ $x^{\top}$]
<proof>

2.9.22. Definition (future operators)

megs

OclCount :: [('A, 'a::null) Set, ('A, 'a) Set] $\Rightarrow$ 'A Integer

OclSum :: ('A, 'a::null) Set $\Rightarrow$ 'A Integer

notation OclCount ( $\rightarrow$ count$_{Set}$ '(-') )

notation OclSum ( $\rightarrow$ sum$_{Set}$ '(-') )

2.9.23. Logical Properties

OclIncluding

lemma OclIncluding-valid-args-valid:
($\tau$ $\models$ $v(X \rightarrow \text{including}_{\text{Set}}(x))$) = (($\tau$ $\models$ ($\delta X$)) $\land$ ($\tau$ $\models$(v $x$)))
<proof>

lemma OclIncluding-valid-args-valid''[simp,code-unfold]:
v(X->including$_{Set}$(x)) = ((δ X) and (v x))
`(proof)`

etc. etc.

OclExcluding

**lemma OclExcluding-valid-args-valid:**
(τ ⊨ υ(X->excluding$_{Set}$(x))) = ((τ ⊨(δ X)) ∧ (τ ⊨(υ x)))
(proof)

$$
\begin{equation*}
\begin{array}{l}
(\tau \models \nu(X \rightarrow \text{excluding}_{\text{Set}}(x))) = ((\tau \models (\delta X)) \land (\tau \models (\upsilon x))) \\
\qquad \langle \text{proof} \rangle
\end{array}
\end{equation*}
$$

**lemma OclExcluding-valid-args-valid''[simp,code-unfold]:**

$$
\begin{align*}
\nu(X \rightarrow \text{excluding}_{\text{Set}}(x)) &= ((\delta X) \text{ and } (\upsilon x)) \\
\langle \text{proof} \rangle
\end{align*}
$$

OclIncludes

**lemma OclIncludes-valid-args-valid:**

$$
\begin{align*}
(\tau \models \upsilon(X \rightarrow \mathit{includes}_{\mathit{Set}}(x))) &= ((\tau \models (\delta X)) \land (\tau \models (\upsilon x))) \\
\langle \mathit{proof} \rangle
\end{align*}
$$

lemma OclIncludes-valid-args-valid''[simp, code-unfold]:

$$
\begin{array}{l}
\nu(X \rightarrow \mathit{includes}_{\mathit{Set}}(x)) = ((\delta X) \text{ and } (\upsilon x)) \\
\langle \mathit{proof} \rangle
\end{array}
$$

OclExcludes

lemma OclExcludes-valid-args-valid:

$$
\begin{align*}
(\tau \models \upsilon(X \rightarrow \mathit{excludes}_{\mathit{Set}}(x))) &= ((\tau \models (\delta X)) \land (\tau \models (\upsilon x))) \\
\langle \mathit{proof} \rangle
\end{align*}
$$

lemma OclExcludes-valid-args-valid''[simp, code-unfold]:

$$
\begin{array}{l}
\nu(X \rightarrow \mathit{excludes}_{\mathit{Set}}(x)) = ((\delta X) \text{ and } (\upsilon x)) \\
\langle \mathit{proof} \rangle
\end{array}
$$

OclSize

lemma OclSize-defined-args-valid: τ ⊧ δ (X->size$_{Set}$( )) = ⇒ τ ⊧ δ X

`(proof)`

lemma OclSize-infinite:

assumes non-finite: τ ⊧ not(δ(S->size$_{Set}$()))

shows (τ ⊧ not(δ(S))) ∨ ¬ finite ᴠRep-Set$_{base}$ (S τ) ᴠ
(proof)

lemma τ ⊧ δ X = ⇒ ¬ finite ᴠRep-Set$_{base}$ (X τ) ᴠ = ⇒ τ ⊧ δ (X->size$_{Set}$( ))

<proof>

lemma size-defined:

assumes X-finite: ᐎτ. finite ᐕRep-Set$_{base}$ (X τ) ᐕ

shows δ (X->size$_{Set}$( )) = δ X

<proof>

lemma size-defined':

assumes X-finite: finite ᴠRep-Set$_{base}$ (X τ) ᴠ

shows (τ ⊧ δ (X->size$_{Set}$())) = (τ ⊧ δ X)

<proof>

OclIsEmpty

lemma OclIsEmpty-defined-args-valid:τ ⊧ δ (X->$_{Set}$( )) = ⇒ τ ⊧ υ X

`(proof)`
**lemma** $\tau \models \delta (\mathit{null} \rightarrow \mathit{isEmptySet})$
$\langle\mathit{proof}\rangle$

**lemma** OclIsEmpty-infinite: $\tau \models \delta X \implies \neg \text{finite } \text{Rep-Set}_{\text{base}} (X \tau)^{\top} \implies \neg \tau \models \delta (X \rightarrow \text{emptySet})$
$\langle\mathit{proof}\rangle$

OclNotEmpty

**lemma** OclNotEmpty-defined-args-valid: $\tau \models \delta (X \rightarrow \text{notEmptySet}) \implies \tau \models \nu X$
$\langle\mathit{proof}\rangle$

**lemma** $\tau \models \delta (\mathit{null} \rightarrow \mathit{notEmptySet})$
$\langle\mathit{proof}\rangle$

**lemma** OclNotEmpty-infinite: $\tau \models \delta X \implies \neg \text{finite } \text{Rep-Set}_{\text{base}} (X \tau)^{\top} \implies \neg \tau \models \delta (X \rightarrow \text{notEmptySet})$
$\langle\mathit{proof}\rangle$

**lemma** OclNotEmpty-has-elt : $\tau \models \delta X \implies$
$\tau \models X \rightarrow \text{notEmptySet} \implies$
$\exists e. e \in \text{Rep-Set}_{\text{base}} (X \tau)^{\top}$
$\langle\mathit{proof}\rangle$

OclANY

**lemma** OclANY-defined-args-valid: $\tau \models \delta (X \rightarrow \text{anySet}) \implies \tau \models \delta X$
$\langle\mathit{proof}\rangle$

**lemma** $\tau \models \delta X \implies \tau \models X \rightarrow \text{emptySet} \implies \neg \tau \models \delta (X \rightarrow \text{anySet})$
$\langle\mathit{proof}\rangle$

**lemma** OclANY-valid-args-valid:
$(\tau \models \nu (X \rightarrow \text{anySet})) = (\tau \models \nu X)$
$\langle\mathit{proof}\rangle$

**lemma** OclANY-valid-args-valid''[simp,code-unfold]:
$\nu(X \rightarrow \text{anySet}) = (\nu X)$
$\langle\mathit{proof}\rangle$

## 2.9.24. Execution Laws with Invalid or Null or Infinite Set as Argument

OclIncluding

OclExcluding

OclIncludes

OclExcludes

OclSize

**lemma** OclSize-invalid[simp,code-unfold]: $(\text{invalid} \rightarrow \text{sizeSet}) = \text{invalid}$
$\langle\mathit{proof}\rangle$

**lemma** OclSize-null[simp,code-unfold]: $(\text{null} \rightarrow \text{sizeSet}) = \text{invalid}$
$\langle\mathit{proof}\rangle$

OclIsEmpty

**lemma** OclIsEmpty-invalid[simp,code-unfold]: $(\text{invalid} \rightarrow \text{emptySet}) = \text{invalid}$
$\langle\mathit{proof}\rangle$

**lemma** OclIsEmpty-null[simp,code-unfold]: $(\text{null} \rightarrow \text{emptySet}) = \text{true}$
〈proof〉

OclNotEmpty

lemma OclNotEmpty-invalid[simp, code-unfold]: (invalid->notEmptySet()) = invalid
<proof>

lemma OclNotEmpty-null[simp, code-unfold]: (null->notEmptySet()) = false
<proof>

OclANY

lemma OclANY-valid[simp, code-unfold]: (invalid->anySet()) = invalid
<proof>

lemma OclANY-null[simp, code-unfold]: (null->anySet()) = null
<proof>

OclForall

lemma OclForall-valid[simp, code-unfold]: invalid->forallSet(a | P a) = invalid
<proof>

lemma OclForall-null[simp, code-unfold]: null->forallSet(a | P a) = invalid
<proof>

OclExists

lemma OclExists-valid[simp, code-unfold]: invalid->existsSet(a | P a) = invalid
<proof>

lemma OclExists-null[simp, code-unfold]: null->existsSet(a | P a) = invalid
<proof>

OclIterate

lemma OclIterate-valid[simp, code-unfold]: invalid->iterateSet(a; x = A | P a x) = invalid
<proof>

lemma OclIterate-null[simp, code-unfold]: null->iterateSet(a; x = A | P a x) = invalid
<proof>

lemma OclIterate-valid-args[simp, code-unfold]: S->iterateSet(a; x = invalid | P a x) = invalid
<proof>

An open question is this ...

lemma S->iterateSet(a; x = null | P a x) = invalid
<proof>

lemma OclIterate-infinite:

assumes non-finite: τ ⊧ not(δ(S->sizeSet()))

shows (OclIterate S A F) τ = invalid τ
<proof>

OclSelect

lemma OclSelect-valid[simp, code-unfold]: invalid->selectSet(a | P a) = invalid
<proof>

lemma OclSelect-null[simp, code-unfold]: null->selectSet(a | P a) = invalid
<proof>
### OclReject

**lemma** OclReject-invalid[simp,code-unfold]: invalid->reject$_{Set}$(a | P a) = invalid
<proof>

**lemma** OclReject-null[simp,code-unfold]: null->reject$_{Set}$(a | P a) = invalid
<proof>

### Context Passing

**lemma** cp-OclIncludes1:

(X->includes$_{Set}$(x)) τ = (X->includes$_{Set}$(λ-. x τ)) τ
<proof>

**lemma** cp-OclSize: X->size$_{Set}$( ) τ = ((λ-. X τ)->size$_{Set}$( ) τ
<proof>

**lemma** cp-OclIsEmpty: X->empty$_{Set}$( ) τ = ((λ-. X τ)->empty$_{Set}$( ) τ
<proof>

**lemma** cp-OclNotEmpty: X->notEmpty$_{Set}$( ) τ = ((λ-. X τ)->notEmpty$_{Set}$( ) τ
<proof>

**lemma** cp-OclANY: X->any$_{Set}$( ) τ = ((λ-. X τ)->any$_{Set}$( ) τ
<proof>

**lemma** cp-OclForall:

(S->forall$_{Set}$(x | P x)) τ = ((λ-. S τ)->forall$_{Set}$(x | P (λ-. x τ))) τ
<proof>

**lemma** cp-OclForall1 [simp, intro!]:

cp S = cp (λX. ((S X)->forall$_{Set}$(x | P x)))
<proof>

**lemma**

cp (λX St x. P (λτ. x) X St) = cp S = cp (λX. (S X)->forall$_{Set}$(x|P x X))
<proof>

**lemma**

cp S =
(\X. cp(P x)) =
cp(λX. ((S X)->forall$_{Set}$(x | P x X)))
<proof>

**lemma** cp-OclExists:

(S->exists$_{Set}$(x | P x)) τ = ((λ-. S τ)->exists$_{Set}$(x | P (λ-. x τ))) τ
<proof>

**lemma** cp-OclExists1 [simp, intro!]:

cp S = cp (λX. ((S X)->exists$_{Set}$(x | P x)))
<proof>

**lemma** cp-OclIterate:

(X->iterate$_{Set}$(a; x = A | P a)) τ =
((λ -. X τ) -> iterateSet(a; x = A | P a x)) τ
<proof>

lemma cp-OclSelect: (X->selectSet(a | P a)) τ =
((λ -. X τ) -> selectSet(a | P a)) τ
<proof>

lemma cp-OclReject: (X->rejectSet(a | P a)) τ = ((λ -. X τ)->rejectSet(a | P a)) τ
<proof>

lemmas cp-intro''$_{Set}$ [intro!, simp, code-unfold] =
cp-OclSize [THEN allU[THEN allU[THEN cpI1], of OclSize]]
cp-OclIsEmpty [THEN allU[THEN allU[THEN cpI1], of OclIsEmpty]]
cp-OclNotEmpty [THEN allU[THEN allU[THEN cpI1], of OclNotEmpty]]
cp-OclANY [THEN allU[THEN allU[THEN cpI1], of OclANY]]

Const

lemma const-OclIncluding[simp, code-unfold] :
assumes const-x : const x
and const-S : const S
shows const (S->including$_{Set}$(x))
<proof>

2.9.25. General Algebraic Execution Rules

Execution Rules on Including

lemma OclIncluding-finite-rep-set :
assumes X-def : τ |= δ X
and x-val : τ |= υ x
shows finite ⌢Rep-Set$_{base}$ (X->including$_{Set}$(x) τ) ⌢ = finite ⌢Rep-Set$_{base}$ (X τ) ⌢
<proof>

lemma OclIncluding-rep-set :
assumes S-def : τ |= δ S
shows ⌢Rep-Set$_{base}$ (S->including$_{Set}$(λ-. ⌢x$_{↓}$) τ) ⌢ = insert ⌢x$_{↓}$ ⌢Rep-Set$_{base}$ (S τ) ⌢
<proof>

lemma OclIncluding-notempty-rep-set :
assumes X-def : τ |= δ X
and a-val : τ |= υ a
shows ⌢Rep-Set$_{base}$ (X->including$_{Set}$(a) τ) ⌢ ≠ {}
<proof>

lemma OclIncluding-includes0 :
assumes τ |= X->includes$_{Set}$(x)
shows X->including$_{Set}$(x) τ = X τ
<proof>

lemma OclIncluding-includes :
assumes τ |= X->includes$_{Set}$(x)
shows τ |= X->including$_{Set}$(x) ≜ X
<proof>

lemma OclIncluding-commute0 :
assumes S-def : τ |= δ S
and i-val : τ |= υ i
and $j\text{-val} : \tau \models v j$

shows $\tau \models ((S :: ('A, 'a::null) Set)\rightarrow\text{excluding}_{Set}(i)\rightarrow\text{excluding}_{Set}(j)) \triangleq (S\rightarrow\text{excluding}_{Set}(j)\rightarrow\text{excluding}_{Set}(i)))$

<proof>

**lemma OclIncluding-commute[simp,code-unfold]:**

((S :: ('A, 'a::null) Set) -> excludingSet(i) -> excludingSet(j) = (S -> excludingSet(j) -> excludingSet(i)))
<proof>

### Execution Rules on Excluding

**lemma OclExcluding-finite-rep-set:**

assumes $X\text{-def} : \tau \models \delta X$

and $x\text{-val} : \tau \models v x$

shows finite $\sqsuperscript{\top}\text{Rep-Set}_{\text{base}}$ ($X \rightarrow \text{excluding}_{Set}(x) \tau^{\top} = \text{finite } \sqsuperscript{\top}\text{Rep-Set}_{\text{base}}$ ($X \tau^{\top}$)
<proof>

**lemma OclExcluding-rep-set:**

assumes $S\text{-def} : \tau \models \delta S$

shows $\sqsuperscript{\top}\text{Rep-Set}_{\text{base}}$ ($S \rightarrow \text{excluding}_{Set}(\lambda. \Box x_{\Box}) \tau^{\top} = \sqsuperscript{\top}\text{Rep-Set}_{\text{base}}$ ($S \tau^{\top} - \{\Box x_{\Box}\}$)
<proof>

**lemma OclExcluding-excludes0:**

assumes $\tau \models X \rightarrow \text{excludes}_{Set}(x)$

shows $X \rightarrow \text{excluding}_{Set}(x) \tau = X \tau$
<proof>

**lemma OclExcluding-excludes:**

assumes $\tau \models X \rightarrow \text{excludes}_{Set}(x)$

shows $\tau \models X \rightarrow \text{excluding}_{Set}(x) \triangleq X$
<proof>

**lemma OclExcluding-charn0[simp]:**

assumes $\text{val} \text{-} x : \tau \models (v x)$

shows $\tau \models ((\text{Set}\{\} \rightarrow \text{excluding}_{Set}(x)) \triangleq \text{Set}\{\})$
<proof>

**lemma OclExcluding-commute0:**

assumes $S\text{-def} : \tau \models \delta S$

and $i\text{-val} : \tau \models i$

and $j\text{-val} : \tau \models j$

shows $\tau \models ((S :: ('A, 'a::null) Set)\rightarrow\text{excluding}_{Set}(i)\rightarrow\text{excluding}_{Set}(j) \triangleq (S\rightarrow\text{excluding}_{Set}(j)\rightarrow\text{excluding}_{Set}(i)))$

<proof>

**lemma OclExcluding-commute[simp,code-unfold]:**

((S :: ('A, 'a::null) Set) -> excludingSet(i) -> excludingSet(j) = (S -> excludingSet(j) -> excludingSet(i)))
<proof>

**lemma OclExcluding-charn0-exec[simp,code-unfold]:**

($\text{Set}\{\} \rightarrow \text{excluding}_{Set}(x) = (\text{if } (v x) \text{ then } \text{Set}\{\} \text{ else invalid } \text{endif})$
<proof>

**lemma OclExcluding-charn1:**

assumes $\text{def} \text{-} X : \tau \models (\delta X)$
and $\mathit{val-x}:\tau \models (\upsilon x)$
and $\mathit{val-y}:\tau \models (\upsilon y)$
and $\mathit{neq} :\tau \models \mathit{not}(x \triangleq y)$
shows $\tau \models ((X \rightarrow \mathit{including}_{\mathit{Set}}(x)) \rightarrow \mathit{excluding}_{\mathit{Set}}(y)) \triangleq ((X \rightarrow \mathit{excluding}_{\mathit{Set}}(y)) \rightarrow \mathit{including}_{\mathit{Set}}(x))$
$\langle\mathit{proof}\rangle$

**lemma OclExcluding-charn2:**
assumes $\mathit{def-X}:\tau \models (\delta X)$
and $\mathit{val-x}:\tau \models (\upsilon x)$
shows $\tau \models (((X \rightarrow \mathit{including}_{\mathit{Set}}(x)) \rightarrow \mathit{excluding}_{\mathit{Set}}(x)) \triangleq (X \rightarrow \mathit{excluding}_{\mathit{Set}}(x)))$
$\langle\mathit{proof}\rangle$

**theorem OclExcluding-charn3:** $((X \rightarrow \mathit{including}_{\mathit{Set}}(x)) \rightarrow \mathit{excluding}_{\mathit{Set}}(x)) = (X \rightarrow \mathit{excluding}_{\mathit{Set}}(x))$
$\langle\mathit{proof}\rangle$

One would like a generic theorem of the form:

**lemma OclExcluding_charn_exec:**
"(X->including\_set(x::('A,a::null)val)->excluding\_set(y)) =
( if δ X then if x = y
 then X->excluding\_set(y)
 else X->excluding\_set(y)->including\_set(x)
 else invalid endif)"

Unfortunately, this does not hold in general, since referential equality is an overloaded concept and has to be defined for each type individually. Consequently, it is only valid for concrete type instances for Boolean, Integer, and Sets thereof...

The computational law *OclExcluding-charn-exec* becomes generic since it uses strict equality which in itself is generic. It is possible to prove the following generic theorem and instantiate it later (using properties that link the polymorphic logical strong equality with the concrete instance of strict quality).

**lemma OclExcluding-charn-exec:**
assumes strict1: (invalid = y) = invalid
and strict2: (x = invalid) = invalid
and StrictRefEq-valid-args-valid: $\bigwedge (x::('A,a::null)val) y \tau$.
($\tau \models \delta (x = y) = ((\tau \models (\upsilon x)) \land (\tau \models \upsilon y))$)
and cp-StrictRefEq: $\bigwedge (X::('A,a::null)val) Y \tau$. ($X = Y \Rightarrow \tau = ((\lambda-. X \tau) = (\lambda-. Y \tau)) \land \tau = \upsilon x \Rightarrow \tau = \upsilon y \Rightarrow (\tau = ((x = y) \triangleq (x \triangleq y)))$)
and StrictRefEq-vs-StrongEq: $\bigwedge (x::('A,a::null)val) y \tau$.
$\tau \models (x = y) \triangleq (x \triangleq y)$)
shows $(X \rightarrow \mathit{including}_{\mathit{Set}}(x::('A,a::null)val) \rightarrow \mathit{excluding}_{\mathit{Set}}(y)) =$
( if δ X then if x = y
 then X \rightarrow \mathit{excluding}_{\mathit{Set}}(y)
 else X \rightarrow \mathit{excluding}_{\mathit{Set}}(y) \rightarrow \mathit{including}_{\mathit{Set}}(x)
 else invalid endif)
$\langle\mathit{proof}\rangle$

**schematic-lemma OclExcluding-charn-exec\_Integer[simp,code-unfold]:** ?X
$\langle\mathit{proof}\rangle$
**schematic-lemma** *OclExcluding-charn-exec*<sub>*Boolean*</sub>[*simp*,*code-unfold*]: ?X
*⟨proof⟩*

**schematic-lemma** *OclExcluding-charn-exec*<sub>*Set*</sub>[*simp*,*code-unfold*]: ?X
*⟨proof⟩*

## Execution Rules on Includes

**lemma** *OclIncludes-charn0* [*simp*]:

assumes val-x:τ |= (v x)

**shows**
$$ \tau \models \text{not}(\text{Set}\{\dots\} \rightarrow \text{includes}_{\text{Set}}(x)) $$
*⟨proof⟩*

**lemma** *OclIncludes-charn0'* [*simp*,*code-unfold*]:

Set{}->includes<sub>Set</sub>(x) = (if v x then false else invalid end if)
*⟨proof⟩*

**lemma** *OclIncludes-charn1*:

assumes def-X:τ |= (δ X)

assumes val-x:τ |= (v x)

**shows**
$$ \tau \models (X \rightarrow \text{including}_{\text{Set}}(x) \rightarrow \text{includes}_{\text{Set}}(x)) $$
*⟨proof⟩*

**lemma** *OclIncludes-charn2*:

assumes def-X:τ |= (δ X)

and val-x:τ |= (v x)

and val-y:τ |= (v y)

and neq :τ |= not(x ≜ y)

**shows**
$$ \tau \models (X \rightarrow \text{including}_{\text{Set}}(x) \rightarrow \text{includes}_{\text{Set}}(y)) \triangleq (X \rightarrow \text{includes}_{\text{Set}}(y)) $$
*⟨proof⟩*

Here is again a generic theorem similar as above.

**lemma** *OclIncludes-execute-generic*:

assumes strict1: (invalid ≜ y) = invalid

and strict2: (x ≜ invalid) = invalid

and cp-StrictRefEq: ⋀ (X::('A, 'a::null)val) Y τ. (X ≜ Y) τ = ((λ-. X τ) ≜ (λ-. Y τ)) τ

and StrictRefEq-vs-StrongEq: ⋀ (x::('A, 'a::null)val) y τ.

$$ \tau \models v x \implies \tau \models v y \implies (\tau \models ((x \doteq y) \triangleq (x \triangleq y))) $$

**shows**

$$ (X \rightarrow \text{including}_{\text{Set}}(x::('A, 'a::null)val) \rightarrow \text{includes}_{\text{Set}}(y)) = $$

(if δ X then if x ≜ y then true else X->includes<sub>Set</sub>(y) else invalid end if)
*⟨proof⟩*

**schematic-lemma** *OclIncludes-execute*<sub>*Integer*</sub>[*simp*,*code-unfold*]: ?X
*⟨proof⟩*

**schematic-lemma** *OclIncludes-execute*<sub>*Boolean*</sub>[*simp*,*code-unfold*]: ?X
*⟨proof⟩*

**schematic-lemma** *OclIncludes-execute*<sub>*Set*</sub>[*simp*,*code-unfold*]: ?X
〈proof〉

**lemma OclIncludes-including-generic:**

assumes OclIncludes-execute-generic [simp] : $\bigwedge X \ x \ y.$
$(X \rightarrow \text{including}_{Set}(x::(\mathfrak{A},'a::null)\text{val}) \rightarrow \text{includes}_{Set}(y)) =$
(if $\delta X$ then if $x \doteq y$ then true else $X \rightarrow \text{includes}_{Set}(y)$ elif else invalid end if)

and StrictRefEq-strict'' : $\bigwedge x \ y$. $\delta ((x::(\mathfrak{A},'a::null)\text{val}) \doteq y) = (v(x) \text{ and } v(y))$

and a-val : $\tau \models v \ a$

and x-val : $\tau \models v \ x$

and S-incl : $\tau \models (S) \rightarrow \text{includes}_{Set}((x::(\mathfrak{A},'a::null)\text{val}))$

shows $\tau \models S \rightarrow \text{including}_{Set}((a::(\mathfrak{A},'a::null)\text{val}) \rightarrow \text{includes}_{Set}(x))$

$\langle\text{proof}\rangle$

lemmas OclIncludes-includingInteger =
OclIncludes-including-generic[OF OclIncludes-executeInteger StrictRefEqInteger.def-homo]

## Execution Rules on Excludes

lemma OclExcludes-charn1:

assumes def-X:τ |= (δ X)

assumes val-x:τ |= (v x)

shows
$\tau \models (X \rightarrow \text{excluding}_{Set}(x) \rightarrow \text{excludes}_{Set}(x))$
$\langle\text{proof}\rangle$

## Execution Rules on Size

lemma [simp, code-unfold]: Set{} -> sizeSet() = 0
$\langle\text{proof}\rangle$

lemma OclSize-including-exec[simp, code-unfold]:
((X -> includingSet(x)) -> sizeSet()) = (if δ X and v x then
X -> sizeSet() +_int if X -> includesSet(x) then 0 else 1 end if
else
invalid
end if)
$\langle\text{proof}\rangle$

## Execution Rules on IsEmpty

lemma [simp, code-unfold]: Set{} -> emptySet() = true
$\langle\text{proof}\rangle$

lemma OclIsEmpty-including [simp]:

assumes X-def: τ |= δ X

and X-finite: finite $\sqsupset\sqcap$ Rep-Set$_{base}$ (X $\tau$)$^\square$

and a-val : τ |= v a

shows $X \rightarrow \text{including}_{Set}(a) \rightarrow \text{emptySet()} \tau = \text{false} \tau$
$\langle\text{proof}\rangle$

## Execution Rules on NotEmpty

lemma [simp, code-unfold]: Set{} -> notEmptySet() = false
$\langle\text{proof}\rangle$

lemma OclNotEmpty-including [simp, code-unfold]:

assumes X-def: τ |= δ X

and X-finite: finite $\sqsupset\sqcap$ Rep-Set$_{base}$ (X $\tau$)$^\square$

and a-val : τ |= v a
shows $X->including_{Set}(a)->notEmpty_{Set}() \quad \tau = true \quad \tau$
<proof>

### Execution Rules on Any

lemma [simp, code-unfold]: Set{}->any_{Set()} = null
<proof>

lemma OclANY-singleton-exec[simp, code-unfold]:
(Set{}->including_{Set}(a)) -> any_{Set()} = a
<proof>

### Execution Rules on Forall

lemma OclForall-mtSet-exec[simp, code-unfold] : ((Set{})->forall_{Set}(z | P(z))) = true
<proof>

The following rule is a main theorem of our approach: From a denotational definition that assures consistency, but may be — as in the case of the OclForall X P — dauntingly complex, we derive operational rules that can serve as a gold-standard for operational execution, since they may be evaluated in whatever situation and according to whatever strategy. In the case of OclForall X P, the operational rule gives immediately a way to evaluation in any finite (in terms of conventional OCL: denotable) set, although the rule also holds for the infinite case:

$$ \mathit{Integer}_{null} -> \mathit{forallAll}_{Set}(x | \mathit{Integer}_{null} -> \mathit{forallAll}_{Set}(y | x + \mathit{int} \ y \triangleq y + \mathit{int} \ x)) $$

or even:

$$ \mathit{Integer} -> \mathit{forallAll}_{Set}(x | \mathit{Integer} -> \mathit{forallAll}_{Set}(y | x + \mathit{int} \ y \doteq y + \mathit{int} \ x)) $$

are valid OCL statements in any context $\tau$.

theorem OclForall-including-exec[simp, code-unfold] :

assumes cp0 : cp P

shows
((S->including_{Set}(x)) ->forall_{Set}(z | P(z))) = (if $\delta$ S and $\nu$ x
then P x and (S->forall_{Set}(z | P(z)))
else invalid
endif)

<proof>

### Execution Rules on Exists

lemma OclExists-mtSet-exec[simp, code-unfold] :
((Set{})->exists_{Set}(z | P(z))) = false
<proof>

lemma OclExists-including-exec[simp, code-unfold] :

assumes cp : cp P

shows ((S->including_{Set}(x)) ->exists_{Set}(z | P(z))) = (if $\delta$ S and $\nu$ x
then P x or (S->exists_{Set}(z | P(z))))
else invalid
endif)

<proof>

### Execution Rules on Iterate

lemma OclIterate-empty[simp, code-unfold]: ((Set{})->iterate_{Set}(a; x = A | P a x)) = A
<proof>

In particular, this does hold for $A = \text{null}$.

lemma OclIterate-including:

assumes $S$-finite: $\tau \models \delta(S->size_{Set()})$
and F-valid-arg: (v A) τ = (v (F a A)) τ

and F-commute: comp-fun-commute F

and F-cp: ⋀ x y τ. F x y τ = F (λ - . x τ) y τ

shows ((S->includingSet(a))-->iterateSet(a; x = A | F a x)) τ =
((S->excludingSet(a))-->iterateSet(a; x = F a A | F a x)) τ
(proof)

Execution Rules on Select

lemma OclSelect-mtSet-exec[simp, code-unfold]: OclSelect mtSet P = mtSet
(proof)

definition OclSelect-body :: - ⇒ - ⇒ - ⇒ ('A, 'a option option) Set
≡ (λP x acc. if P x = false then acc else acc->includingSet(x) endif)

theorem OclSelect-including-exec[simp, code-unfold]:

assumes P-cp : cp P

shows OclSelect (X->includingSet(y)) P = OclSelect-body P y (OclSelect (X->excludingSet(y)) P)

(is - = ?select)

<proof>

Execution Rules on Reject

lemma OclReject-mtSet-exec[simp, code-unfold]: OclReject mtSet P = mtSet
(proof)

lemma OclReject-including-exec[simp, code-unfold]:

assumes P-cp : cp P

shows OclReject (X->includingSet(y)) P = OclSelect-body (not o P) y (OclReject (X->excludingSet(y)) P)

<proof>

Execution Rules Combining Previous Operators

OclIncluding

lemma OclIncluding-idem0 :

assumes τ ::= δ S

and τ ::= v i

shows τ ::= (S->includingSet(i)->includingSet(i) ⇝ (S->includingSet(i)))

<proof>

theorem OclIncluding-idem[simp, code-unfold]: ((S :: ('A, 'a::null)Set)->includingSet(i)->includingSet(i) = (S->includingSet(i)))
(proof)

<proof>

OclExcluding

lemma OclExcluding-idem0 :

assumes τ ::= δ S

and τ ::= v i

shows τ ::= (S->excludingSet(i)->excludingSet(i) ⇝ (S->excludingSet(i)))

<proof>

theorem OclExcluding-idem[simp, code-unfold]: ((S->excludingSet(i)->excludingSet(i)) = (S->excludingSet(i)))
(proof)

<proof>

OclIncludes
**lemma OclIncludes-any[simp,code-unfold]:**

$$
\begin{align*}
X \rightarrow \text{includes}_{\text{Set}}(X \rightarrow \text{any}_{\text{Set}}()) &= (\text{if } \delta X \text{ then} \\
&\quad \text{if } \delta (X \rightarrow \text{size}_{\text{Set}}()) \text{ then not } (X \rightarrow \text{isEmpty}_{\text{Set}}()) \\
&\quad \text{else } X \rightarrow \text{includes}_{\text{Set}}(\text{null}) \text{endif} \\
&\quad \text{else invalidendif})
\end{align*}
$$

`(proof)`

OclSize

lemma [simp, code-unfold]: δ (Set{}} -> sizeSet()) = true

`(proof)`

lemma [simp, code-unfold]: δ ((X -> includingSet(x)) -> sizeSet()) = (δ(X -> sizeSet()) and v(x))

`(proof)`

lemma [simp, code-unfold]: δ ((X -> excludingSet(x)) -> sizeSet()) = (δ(X -> sizeSet()) and v(x))

`(proof)`

lemma [simp]:

assumes X-finite: ⋀τ. finite ⌜Rep-Set<sub>base</sub> (X τ)⌝

shows δ ((X -> including<sub>Set</sub>(x)) -> size<sub>Set</sub>() ) = (δ(X) and v(x))

`(proof)`

OclForall

lemma OclForall-rep-set-false:

assumes τ ::= δ X

shows (OclForall X P τ = false τ) = (∃x ∈ ⌜Rep-Set<sub>base</sub> (X τ)⌝. P (λτ. x) τ = false τ)

`(proof)`

lemma OclForall-rep-set-true:

assumes τ ::= δ X

shows (τ ::= OclForall X P) = (∀x ∈ ⌜Rep-Set<sub>base</sub> (X τ)⌝. τ ::= P (λτ. x))

`(proof)`

lemma OclForall-includes :

assumes x-def : τ ::= δ x

and y-def : τ ::= δ y

shows (τ ::= OclForall x (OclIncludes y)) = (⌝Rep-Set<sub>base</sub> (x τ)⌝ ⊆ ⌝Rep-Set<sub>base</sub> (y τ)⌝)

`(proof)`

lemma OclForall-not-includes :

assumes x-def : τ ::= δ x

and y-def : τ ::= δ y

shows (OclForall x (OclIncludes y) τ = false τ) = (¬ ⌜Rep-Set<sub>base</sub> (x τ)⌝ ⊆ ⌜Rep-Set<sub>base</sub> (y τ)⌝)

`(proof)`

lemma OclForall-iterate:

assumes S-finite: finite ⌜Rep-Set<sub>base</sub> (S τ)⌝

shows S->forAll<sub>Set</sub>(x | P x) τ = (S->iterate<sub>Set</sub>(x; acc = true | acc and P x)) τ

`(proof)`

lemma OclForall-cong:

assumes ⋀x. x ∈ ⌜Rep-Set<sub>base</sub> (X τ)⌝ = τ ::= P (λτ. x) = τ ::= Q (λτ. x)

assumes P: τ ::= OclForall X P

shows τ ::= OclForall X Q

`(proof)`
**lemma OclForall-cong':**

assumes $A. x. x \in \Gamma \text{Rep-Set}_{\text{base}} (X \tau)^\Gamma \Rightarrow \tau \models P (\lambda\tau. x) \Rightarrow \tau \models Q (\lambda\tau. x) \Rightarrow \tau \models R (\lambda\tau. x)$

assumes $P: \tau \models A \text{OclForall} X P$

assumes $Q: \tau \models A \text{OclForall} X Q$

shows $\tau \models A \text{OclForall} X R$

(*proof*)

Strict Equality

**lemma StrictRefEqSet-defined** :

assumes $x-def: \tau \models \delta x$

assumes $y-def: \tau \models \delta y$

shows $((x::(\mathfrak{A}, \alpha::\text{null})\text{Set}) \doteq y) \tau = (x->\text{forall}\_\text{Set}(z| y->\text{includes}\_\text{Set}(z))) \text{ and } (y->\text{forall}\_\text{Set}(z| x->\text{includes}\_\text{Set}(z))) \tau$

(*proof*)

**lemma StrictRefEqSet-exec[simp,code-unfold]** :

$((x::(\mathfrak{A}, \alpha::\text{null})\text{Set}) \doteq y) = (\text{if } \delta x \text{ then } (\text{if } \delta y \text{ then } ((x->\text{forall}\_\text{Set}(z| y->\text{includes}\_\text{Set}(z))) \text{ and } (y->\text{forall}\_\text{Set}(z| x->\text{includes}\_\text{Set}(z))))))$

else if $v y$
then false (* $x'->\text{includes} = \text{null}$ *)
else invalid
endif

endif

else if $v x$ (* null = ???

then if $v y$ then not($\delta y$) else invalid
else invalid
endif

endif

else invalid
endif

endif

endif)

(*proof*)

**lemma StrictRefEqSet-L-subst1** : $\text{cp } P \implies \tau \models v x \implies \tau \models v y \implies \tau \models v P x \implies \tau \models v P y \implies \tau \models (x::(\mathfrak{A}, \alpha::\text{null})\text{Set}) \doteq y \implies \tau \models (P x :: (\mathfrak{A}, \alpha::\text{null})\text{Set}) \doteq P y$

(*proof*)

**lemma OclIncluding-cong'** :

shows $\tau \models \delta s \implies \tau \models \delta t \implies \tau \models v x \implies \tau \models ((s::(\mathfrak{A}, \alpha::\text{null})\text{Set}) \doteq t) \implies \tau \models (s->\text{including}_{\text{Set}}(x) \doteq (t->\text{including}_{\text{Set}}(x)))$

(*proof*)

**lemma OclIncluding-cong** : $\bigwedge (s::(\mathfrak{A}, \alpha::\text{null})\text{Set}) t x y \tau. \tau \models \delta t \implies \tau \models v y \implies \tau \models s \doteq t \implies x = y \implies \tau \models s->\text{including}_{\text{Set}}(x) \doteq (t->\text{including}_{\text{Set}}(y))$

(*proof*)

**lemma const-StrictRefEqSet-empty** : $\text{const } X \implies \text{const } (X \doteq \text{Set}\{\})$

(*proof*)

**lemma const-StrictRefEqSet-including** :

$\text{const } a \implies \text{const } S \implies \text{const } X \implies \text{const } (X \doteq S->\text{including}_{\text{Set}}(a))$

(*proof*)

## 2.9.26. Test Statements

Assert $(\tau \models (\text{Set}\{\lambda-. \text{↓}x_{↓}\} \doteq \text{Set}\{\lambda-. \text{↓}x_{↓}\}))$

Assert $(\tau \models (\text{Set}\{\lambda-. \text{↓}x_{↓}\} \doteq \text{Set}\{\lambda-. \text{↓}x_{↓}\}))$
such well-formed stores that satisfy this invariant (the WFF-invariant), the referential equality and the
strong equality—and therefore the strict equality on sequences in the sense above—coincides.

Property proof in terms of `profile-bin<StrongEq>v-v`

**interpretation** StrictRefEq<Seq : profile-bin<StrongEq>v-v> $\lambda x y$. ($x::('A, 'a::null) Sequence$) $\doteq$ $y$
<proof>

## 2.10.3. Constants: mtSequence

**definition** `mtSequence` :: ('A, 'a::null) Sequence (Sequence{})

**where** `Sequence{}` $\equiv$ ($\lambda \tau$. `Abs-Sequence<base> []`::'a list[]`)

**lemma** `mtSequence-defined[simp,code-unfold]:` $\delta(Sequence{})$ = true
<proof>

**lemma** `mtSequence-valid[simp,code-unfold]:` $v(Sequence{})$ = true
<proof>

**lemma** `mtSequence-rep-set:` $\top Rep-Sequence<base> (Sequence{}) \tau^\top$ = []
<proof> **lemma** [simp,code-unfold]: const Sequence{}
<proof>

Note that the collection types in OCL allow for null to be included; however, there is the null-collection
into which inclusion yields invalid.

## 2.10.4. Definition: Prepend

**definition** `OclPrepend` :: [(('A, 'a::null) Sequence, ('A, 'a) val] $\Rightarrow$ ('A, 'a) Sequence

**where** `OclPrepend x y` = ($\lambda \tau$. if ($\delta x$) $\tau$ = true $\tau$ $\wedge$ ($v y$) $\tau$ = true $\tau$
then `Abs-Sequence<base> []` ($y \tau$) $\#\top$ `Rep-Sequence<base> ($x \tau$)$^\top$ []
else invalid $\tau$)

**notation** `OclPrepend` $\text{(->}\text{->}\text{prepend}_{Seq}'(-')\text{)}$

**interpretation** `OclPrepend:profile-bin<delta> OclPrepend $\lambda x y$. `Abs-Sequence<base> []$y$` $\#\top$ `Rep-Sequence<base> $x^\top$ []$
<proof>

**syntax**

`-OclFinsequence` :: `args` $\Rightarrow$ (`'A', 'a::null)` Sequence (Sequence{(-)})

**translations**

`Sequence{x, xs}` == `CONST OclPrepend (Sequence{xs}) x`

`Sequence{x}` == `CONST OclPrepend (Sequence{}) x`

## 2.10.5. Definition: Including

**definition** `OclIncluding` :: [(('A, 'a::null) Sequence, ('A, 'a) val] $\Rightarrow$ ('A, 'a) Sequence

**where** `OclIncluding x y` = ($\lambda \tau$. if ($\delta x$) $\tau$ = true $\tau$ $\wedge$ ($v y$) $\tau$ = true $\tau$
then `Abs-Sequence<base> []` $\top$ `Rep-Sequence<base> ($x \tau$)$^\top$ @ [$y \tau$] []
else invalid $\tau$)

**notation** `OclIncluding` $\text{(->}\text{->}\text{including}_{Seq}'(-')\text{)}$

**interpretation** `OclIncluding` :

`profile-bin<delta> OclIncluding $\lambda x y$. `Abs-Sequence<base> []$\top$ `Rep-Sequence<base> $x^\top$ @ [$y$] []
<proof>

**lemma** [simp,code-unfold] : (Sequence{}$\rightarrow$`including<Seq>(a)}) = (Sequence{}$\rightarrow$`prepend<Seq>(a))
<proof>
**lemma** [simp, code-unfold] : ((S->prependSeq(a))->includingSeq(b)) = ((S->includingSeq(b))->prependSeq(a))

*<proof>*

## 2.10.6. Definition: Excluding

**definition** *OclExcluding* :: [(‘*A*,‘*α*::null) Sequence, (‘*A*,‘*α* ) val] ⇒ (‘*A*,‘*α* ) Sequence

**where**
OclExcluding x y = (λ τ. if (δ x) τ = true τ ∧ (v y) τ = true τ
then Abs-Sequence<sub>base</sub> ⊥ filter (λx. x = y τ)
<sup>Π</sup>Rep-Sequence<sub>base</sub> (x τ)<sup>Π</sup> ⊥
else invalid τ )

notation OclExcluding (->excludingSeq' (-'))

interpretation OclExcluding:profile-bin<sub>d-v</sub> OclExcluding
λx y. Abs-Sequence<sub>base</sub> ⊥ filter (λx. x = y) <sup>Π</sup>Rep-Sequence<sub>base</sub> (x)<sup>Π</sup> ⊥
<proof>

## 2.10.7. Definition: Append

Identical to OclIncluding.

**definition** *OclAppend* :: [(‘*A*,‘*α*::null) Sequence, (‘*A*,‘*α* ) val] ⇒ (‘*A*,‘*α* ) Sequence

**where** OclAppend = OclIncluding

notation OclAppend (->appendSeq' (-'))

interpretation OclAppend :
profile-bin<sub>d-v</sub> OclAppend λx y. Abs-Sequence<sub>base</sub> <sup>Π</sup>Rep-Sequence<sub>base</sub> x<sup>Π</sup> @ [y]<sub>⊥</sub>
<proof>

## 2.10.8. Definition: Union

**definition** *OclUnion* :: [(‘*A*,‘*α*::null) Sequence, (‘*A*,‘*α* ) Sequence] ⇒ (‘*A*,‘*α* ) Sequence

**where**
OclUnion x y = (λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then Abs-Sequence<sub>base</sub> ⊥ <sup>Π</sup>Rep-Sequence<sub>base</sub> (x τ)<sup>Π</sup> @
<sup>Π</sup>Rep-Sequence<sub>base</sub> (y τ)<sup>Π</sup> ⊥
else invalid τ )

notation OclUnion (->unionSeq' (-'))

interpretation OclUnion :
profile-bin<sub>d-d</sub> OclUnion λx y. Abs-Sequence<sub>base</sub> <sup>Π</sup>Rep-Sequence<sub>base</sub> x<sup>Π</sup> @ <sup>Π</sup>Rep-Sequence<sub>base</sub> y<sup>Π</sup> ⊥
<proof>

## 2.10.9. Definition: At

**definition** *OclAt* :: [(‘*A*,‘*α*::null) Sequence, (‘*A*) Integer] ⇒ (‘*A*,‘*α* ) val

**where**
OclAt x y = (λ τ. if (δ x) τ = true τ ∧ (δ y) τ = true τ
then if 1 ≤ <sup>Π</sup>y τ<sup>Π</sup> ∧ <sup>Π</sup>y τ<sup>Π</sup> ≤ length<sup>Π</sup>Rep-Sequence<sub>base</sub> (x τ)<sup>Π</sup>
then <sup>Π</sup>Rep-Sequence<sub>base</sub> (x τ)<sup>Π</sup> ! (nat <sup>Π</sup>y τ<sup>Π</sup> - 1)
else invalid τ
else invalid τ )

notation OclAt (->atSeq' (-'))

## 2.10.10. Definition: First

**definition** *OclFirst* :: [(‘*A*,‘*α*::null) Sequence] ⇒ (‘*A*,‘*α* ) val

**where**
OclFirst x = (λ τ. if (δ x) τ = true τ then
case <sup>Π</sup>Rep-Sequence<sub>base</sub> (x τ)<sup>Π</sup> of [] ⇒ invalid τ
| x # - ⇒ x

else invalid τ )

notation OclFirst (->firstSeq'(-'))

2.10.11. Definition: Last

definition OclLast :: [( 'A , 'α::null ) Sequence] ⇒ ( 'A , 'α ) val

where
OclLast x = (λ τ. if (δ x) τ = true τ then
if ⊺ Rep-Sequence$_{base}$ (x τ) ⊺ = [] then
invalid τ
else
last ⊺ Rep-Sequence$_{base}$ (x τ) ⊺
else invalid τ )

notation OclLast (-->lastSeq'(-'))

2.10.12. Definition: Iterate

definition OclIterate :: [ ( 'A , 'α::null ) Sequence , ( 'A , 'β::null ) val ,
( 'A , 'α ) val ⇒ ( 'A , 'β ) val ⇒ ( 'A , 'β ) val ] ⇒ ( 'A , 'β ) val

where
OclIterate S A F = (λ τ. if (δ S) τ = true τ ∧ (v A) τ = true τ
then (foldr (F) (map (λa τ. a) ⊺ Rep-Sequence$_{base}$ (S τ) ⊺)) (A) τ
else ⊥)

syntax

-OclIterateSeq :: [ ( 'A , 'α::null ) Sequence , idt , idt , 'α , 'β ] => ( 'A , 'γ ) val
( - -> iterate$_{Seq}$ ' (;-=- | -' ) )

translations

X->iterate$_{Seq}$(a; x = A | P) == CONST OclIterate X A (%a. (% x. P))

2.10.13. Definition: Forall

definition OclForall ::= [ ( 'A , 'α::null ) Sequence , ( 'A , 'α ) val ⇒ ( 'A ) Boolean ] ⇒ 'A Boolean

where OclForall S P = (S->iterateSeq(b; x = true | x and (P b)))

syntax

-OclForallSeq :: [ ( 'A , 'α::null ) Sequence , id , ( 'A ) Boolean ] ⇒ 'A Boolean ((-) -> forAll$_{Seq}$'(-|-'))

translations

X->forAll$_{Seq}$(x | P) == CONST UML-Sequence.OclForall X (%x. P)

2.10.14. Definition: Exists

definition OclExists ::= [ ( 'A , 'α::null ) Sequence , ( 'A , 'α ) val ⇒ ( 'A ) Boolean ] ⇒ 'A Boolean

where OclExists S P = (S->iterate$_{Seq}$(b; x = false | x or (P b)))

syntax

-OclExistSeq :: [ ( 'A , 'α::null ) Sequence , id , ( 'A ) Boolean ] ⇒ 'A Boolean ((-) -> exists$_{Seq}$ '(-|-'))

translations

X->exists$_{Seq}$(x | P) == CONST OclExists X (%x. P)

2.10.15. Definition: Collect

definition OclCollect :: [ ( 'A , 'α::null ) Sequence , ( 'A , 'α ) val ⇒ ( 'A , 'β ) val ] ⇒ ( 'A , 'β::null ) Sequence

where OclCollect S P = (S->iterate$_{Seq}$(b; x = Sequence{} | x->prepend$_{Seq}$(P b)))

syntax

-OclCollectSeq :: [ ( 'A , 'α::null ) Sequence , id , ( 'A ) Boolean ] ⇒ 'A Boolean ((-) -> collect$_{Seq}$ '(-|-'))

translations

X->collect$_{Seq}$(x | P) == CONST OclCollect X (%x. P)
### 2.10.16. Definition: Select

**definition** `OclSelect` :: [(‘A,’α::null)Sequence, (‘A,’α)val⇒(‘A)Boolean]⇒(‘A,’α::null)Sequence

**where** `OclSelect S P =`
(S->iterate$_{Seq}$ (b; x = Sequence{} | if P b then x->prepend$_{Seq}$ (b) else xendif))

**syntax**

`-OclSelectSeq :: [(‘A,’α::null) Sequence,id,(‘A)Boolean] ⇒ ‘A Boolean ((-)→selectSeq’(-|‘))`

**translations**

`X->selectSeq(x | P) == CONST UML-Sequence.OclSelect X (%x. P)`

### 2.10.17. Definition: Size

**definition** `OclSize` :: [(‘A,’α::null)Sequence]⇒(‘A)Integer ((-)→size$_{Seq}$’('))

**where** `OclSize S = (S->iterate$_{Seq}$ (b; x = 0 | x +int 1 ))`

### 2.10.18. Definition: IsEmpty

**definition** `OclIsEmpty` :: ('A,'α::null) Sequence ⇒ 'A Boolean

**where** `OclIsEmpty x = ((v x and not (δ x)) or ((OclSize x) = 0))`

**notation** `OclIsEmpty` `(-->$_{Seq}$’(’))`

### 2.10.19. Definition: NotEmpty

**definition** `OclNotEmpty` :: ('A,'α::null) Sequence ⇒ 'A Boolean

**where** `OclNotEmpty x = not(OclIsEmpty x)`

**notation** `OclNotEmpty` `(-->notEmpty$_{Seq}$’(’))`

### 2.10.20. Definition: Any

**definition** `OclANY x = (λ τ.`

if x τ = invalid τ then

⊥

else

case drop (drop (Rep-Sequence$_{base}$ (x τ))) of [] ⇒ ⊥
| l ⇒ hd l)

**notation** `OclANY` `(-->any$_{Seq}$’(’))`

### 2.10.21. Definition (future operators)

**const's**

`OclCount` :: [(‘A,’α::null) Sequence, (‘A,’α) Sequence] ⇒ ‘A Integer

`OclSum` :: ('A,'α::null) Sequence ⇒ 'A Integer

**notation** `OclCount` `(-->count$_{Seq}$’(-’))`

**notation** `OclSum` `(-->sum$_{Seq}$’(’))`

### 2.10.22. Logical Properties

### 2.10.23. Execution Laws with Invalid or Null as Argument

`OclIterate`

**lemma** `OclIterate-valid[simp,code-unfold]:invalid->iterate$_{Seq}$(a; x = A | P a x) = invalid`
〈proof〉

**lemma** *OclIterate-null[simp,code-unfold]:* `null->iterateSeq(a; x = A | P a x) = invalid`
*(*proof*)*

**lemma** *OclIterate-invalid-args[simp,code-unfold]:* `S->iterateSeq(a; x = invalid | P a x) = invalid`
*(*proof*)*

## Context Passing

**lemma** *cp-OclIncluding:*

(X->includingSeq(x)) τ = ((λ -. X τ)->includingSeq(λ -. x τ)) τ
*(*proof*)*

**lemma** *cp-OclIterate:*

(X->iterateSeq(a; x = A | P a x)) τ =
((λ -. X τ)->iterateSeq(a; x = A | P a x)) τ
*(*proof*)*

**lemmas** *cp-into''Seq[intro!,simp,code-unfold] =*
*cp-OclIncluding [THEN allI[THEN allI[THEN allI[THEN cpI2]], of OclIncluding]]*

## Const

## 2.10.24. General Algebraic Execution Rules

### Execution Rules on Iterate

**lemma** *OclIterate-empty[simp,code-unfold]:* `Sequence{}->iterateSeq(a; x = A | P a x) = A`
*(*proof*)*

In particular, this does hold for A = null.

**lemma** *OclIterate-including[simp,code-unfold]:*

assumes strict1 : X. P invalid X = invalid

and P-valid-arg : τ. (v A) τ = (v (P a A)) τ

and P-cp : x y τ. P x y τ = P (λ -. x τ) y τ

and P-cp' : x y τ. P x y τ = P x (λ -. y τ) τ

shows (S->includingSeq(a)) -> iterateSeq(b; x = A | P b x) = S->iterateSeq(b; x = P a A | P b x)
*(*proof*)*

**lemma** *OclIterate-prepend[simp,code-unfold]:*

assumes strict1 : X. P invalid X = invalid

and strict2 : X. P X invalid = invalid

and P-cp : x y τ. P x y τ = P (λ -. x τ) y τ

and P-cp' : x y τ. P x y τ = P x (λ -. y τ) τ

shows (S->prependSeq(a)) -> iterateSeq(b; x = A | P b x) = P a (S->iterateSeq(b; x = A | P b x))
*(*proof*)*

## 2.10.25. Test Statements

instantiation Sequence<base> ::= (equal)equal

begin

definition HOL equal k l ←→ (k::(‘a::equal)Sequence<base>) = l

instance *(*proof*)*

end

**lemma** *equal-Sequence<base>-code [code]:*

HOL equal k (l::(‘a::{equal null})Sequence<base>) ←→ Rep-Sequence<base> k = Rep-Sequence<base> l
〈proof〉

Assert τ |= (Sequence{} ⋇ Sequence{})

Assert τ |= (Sequence{1,2} ≜ Sequence{} → prependSeq(2) → prependSeq(1))

Assert τ |= (Sequence{1,invalid,2} ≜ invalid)

Assert τ |= (Sequence{1,2} → prependSeq(null) ≜ Sequence{null,1,2})

Assert τ |= (Sequence{1,2} → includingSeq(null) ≜ Sequence{1,2 null})

end

theory UML-Library

imports

basic-types/UML-Boolean

basic-types/UML-Void

basic-types/UML-Integer

basic-types/UML-Real

basic-types/UML-String

collection-types/UML-Pair

collection-types/UML-Bag

collection-types/UML-Set

collection-types/UML-Sequence

begin

## 2.11. Miscellaneous Stuff

### 2.11.1. Definition: asBoolean

definition OclAsBooleanInt :: ('A) Integer ⇒ ('A) Boolean ((-) → oclAsTypeInt('Boolean'))

where
OclAsBooleanInt X = (λτ. if (δ X) τ = true τ
then ⊥^X τ^ ≠ 0_⊥
else invalid τ)

interpretation OclAsBooleanInt : profile-mono<sub>d</sub> OclAsBooleanInt λx. ⊥^x^ ≠ 0_⊥
<proof>

definition OclAsBooleanReal :: ('A) Real ⇒ ('A) Boolean ((-) → oclAsTypeReal('Boolean'))

where
OclAsBooleanReal X = (λτ. if (δ X) τ = true τ
then ⊥^X τ^ ≠ 0_⊥
else invalid τ)

interpretation OclAsBooleanReal : profile-mono<sub>d</sub> OclAsBooleanReal λx. ⊥^x^ ≠ 0_⊥
<proof>

### 2.11.2. Definition: asInteger

definition OclAsIntegerReal :: ('A) Real ⇒ ('A) Integer ((-) → oclAsTypeReal('Integer'))

where
OclAsIntegerReal X = (λτ. if (δ X) τ = true τ
then ⊥floor^X τ^⊥
else invalid $\tau$)

**interpretation** $\mathit{OclAsInteger}_{\mathit{Real}} : \mathit{profile\text{-}mono}_d \mathit{OclAsInteger}_{\mathit{Real}} \lambda x. \llcorner \mathit{floor} \ \overline{\mathit{x}} \ \overline{\lceil} \ \lceil \mathit{proof} \ \rceil$

### 2.11.3. Definition: asReal

**definition** $\mathit{OclAsReal}_{\mathit{Int}} :: (\mathfrak{A}) \mathit{Integer} \Rightarrow (\mathfrak{A}) \mathit{Real} ((-) \to \mathit{oclAsType}_{\mathit{Int}}'(\mathit{Real}))$

**where** $\mathit{OclAsReal}_{\mathit{Int}} X = (\lambda\tau. \text{ if } (\delta X) \tau = \text{ true } \tau$
then $\llcorner \mathit{real\text{-}of\text{-}int} \ \overline{\mathit{x}} \ \overline{\lceil} \ \lceil \mathit{tau} \ \rceil \llcorner$
else invalid $\tau$)

**interpretation** $\mathit{OclAsReal}_{\mathit{Int}} : \mathit{profile\text{-}mono}_d \mathit{OclAsReal}_{\mathit{Int}} \lambda x. \llcorner \mathit{real\text{-}of\text{-}int} \ \overline{\mathit{x}} \ \overline{\lceil} \ \lceil \mathit{proof} \ \rceil$

**lemma** $\mathit{Integer\text{-}subtype\text{-}of\text{-}Real}$:

assumes $\tau \models \delta X$

shows $\tau \models X \rightarrow \mathit{oclAsType}_{\mathit{Int}}(\mathit{Real}) \rightarrow \mathit{oclAsType}_{\mathit{Real}}(\mathit{Integer}) \triangleq X$
$\langle \mathit{proof} \rangle$

### 2.11.4. Definition: asPair

**definition** $\mathit{OclAsPair}_{\mathit{Seq}} :: [(\mathfrak{A},'\alpha::\mathit{null})\mathit{Sequence}] \Rightarrow (\mathfrak{A},'\alpha::\mathit{null},'\alpha::\mathit{null}) \mathit{Pair} ((-) \to \mathit{asPair}_{\mathit{Seq}}'('))$

**where** $\mathit{OclAsPair}_{\mathit{Seq}} S = (\text{if } S \to \mathit{size}_{\mathit{Seq}}() \doteq 2$
then $\mathit{Pair}\{S \to \mathit{at}_{\mathit{Seq}}(0), S \to \mathit{at}_{\mathit{Seq}}(1)\}$
else invalid
endif)

**definition** $\mathit{OclAsPair}_{\mathit{Set}} :: [(\mathfrak{A},'\alpha::\mathit{null})\mathit{Set}] \Rightarrow (\mathfrak{A},'\alpha::\mathit{null},'\alpha::\mathit{null}) \mathit{Pair} ((-) \to \mathit{asPair}_{\mathit{Set}}'('))$

**where** $\mathit{OclAsPair}_{\mathit{Set}} S = (\text{if } S \to \mathit{size}_{\mathit{Set}}() \doteq 2$
then let $v = S \to \mathit{any}_{\mathit{Set}}()$ in
$\mathit{Pair}\{v, S \to \mathit{excluding}_{\mathit{Set}}(v) \to \mathit{any}_{\mathit{Set}}()\}$
else invalid
endif)

**definition** $\mathit{OclAsPair}_{\mathit{Bag}} :: [(\mathfrak{A},'\alpha::\mathit{null})\mathit{Bag}] \Rightarrow (\mathfrak{A},'\alpha::\mathit{null},'\alpha::\mathit{null}) \mathit{Pair} ((-) \to \mathit{asPair}_{\mathit{Bag}}'('))$

**where** $\mathit{OclAsPair}_{\mathit{Bag}} S = (\text{if } S \to \mathit{size}_{\mathit{Bag}}() \doteq 2$
then let $v = S \to \mathit{any}_{\mathit{Bag}}()$ in
$\mathit{Pair}\{v, S \to \mathit{excluding}_{\mathit{Bag}}(v) \to \mathit{any}_{\mathit{Bag}}()\}$
else invalid
endif)

### 2.11.5. Definition: asSet

**definition** $\mathit{OclAsSet}_{\mathit{Seq}} :: [(\mathfrak{A},'\alpha::\mathit{null})\mathit{Sequence}] \Rightarrow (\mathfrak{A},'\alpha)\mathit{Set} ((-) \to \mathit{asSet}_{\mathit{Seq}}'('))$

**where** $\mathit{OclAsSet}_{\mathit{Seq}} S = (S \to \mathit{iterate}_{\mathit{Seq}}(b; x = \mathit{Set}{} | x \to \mathit{including}_{\mathit{Set}}(b)))$

**definition** $\mathit{OclAsSet}_{\mathit{Pair}} :: [(\mathfrak{A},'\alpha::\mathit{null},'\alpha::\mathit{null}) \mathit{Pair}] \Rightarrow (\mathfrak{A},'\alpha)\mathit{Set} ((-) \to \mathit{asSet}_{\mathit{Pair}}'('))$

**where** $\mathit{OclAsSet}_{\mathit{Pair}} S = \mathit{Set}\{S \mathit{First}(\mathit{S}), S \mathit{Second}(\mathit{S})\}$

**definition** $\mathit{OclAsSet}_{\mathit{Bag}} :: (\mathfrak{A},'\alpha::\mathit{null}) \mathit{Bag} \Rightarrow (\mathfrak{A},'\alpha)\mathit{Set} ((-) \to \mathit{asSet}_{\mathit{Bag}}'('))$

**where** $\mathit{OclAsSet}_{\mathit{Bag}} S = (\lambda \tau. \text{ if } (\delta S) \tau = \text{ true } \tau$
then $\mathit{Abs\text{-}Set}_{\mathit{base}} \ \mathit{Rep\text{-}Set\text{-}base} S \ \tau \llcorner$
else if $(v S) \tau = \text{ true } \tau$ then null $\tau$
else invalid $\tau$)
### 2.11.6. Definition: asSequence

**definition** $\mathit{OclAsSeqSet} :: [(\mathfrak{A},'\alpha::null)\mathit{Set}] \Rightarrow (\mathfrak{A},'\alpha)\mathit{Sequence} ((-) \to \mathit{asSequenceSet}'('))$

**where** $\mathit{OclAsSeqSet} S = (S \to \mathit{iterateSet}(b; x = \mathit{Sequence}\{\} | x \to \mathit{includingSeq}(b)))$

**definition** $\mathit{OclAsSeqBag} :: [(\mathfrak{A},'\alpha::null)\mathit{Bag}] \Rightarrow (\mathfrak{A},'\alpha)\mathit{Sequence} ((-) \to \mathit{asSequenceBag}'('))$

**where** $\mathit{OclAsSeqBag} S = (S \to \mathit{iterateBag}(b; x = \mathit{Sequence}\{\} | x \to \mathit{includingSeq}(b)))$

**definition** $\mathit{OclAsSeqPair} :: [(\mathfrak{A},'\alpha::null,'\alpha::null)\mathit{Pair}] \Rightarrow (\mathfrak{A},'\alpha)\mathit{Sequence} ((-) \to \mathit{asSequencePair}'('))$

**where** $\mathit{OclAsSeqPair} S = \mathit{Sequence}\{S .\mathit{First}(\mathit{S}), S .\mathit{Second}(\mathit{S})\}$

### 2.11.7. Definition: asBag

**definition** $\mathit{OclAsBagSeq} :: [(\mathfrak{A},'\alpha::null)\mathit{Sequence}] \Rightarrow (\mathfrak{A},'\alpha)\mathit{Bag} ((-) \to \mathit{asBagSeq}'('))$

**where** $\mathit{OclAsBagSeq} S = (\lambda\tau. \mathit{Abs-BagBase} \perp \lambda s. \mathit{if list-ex} (\mathit{op} = s) \top \mathit{Rep-SequenceBase} (S \tau) \top \mathit{then} 1 \mathit{else} 0_{\perp})$

**definition** $\mathit{OclAsBagSet} :: [(\mathfrak{A},'\alpha::null)\mathit{Set}] \Rightarrow (\mathfrak{A},'\alpha)\mathit{Bag} ((-) \to \mathit{asBagSet}'('))$

**where** $\mathit{OclAsBagSet} S = (\lambda\tau. \mathit{Abs-BagBase} \perp \lambda s. \mathit{if } s \in \top \mathit{Rep-SetBase} (S \tau) \top \mathit{then} 1 \mathit{else} 0_{\perp})$

**lemma** assumes $\tau \models \delta (S \to \mathit{sizeSet}())$

shows $\mathit{OclAsBagSet} S = (S \to \mathit{iterateSet}(b; x = \mathit{Bag}\{\} | x \to \mathit{includingBag}(b)))$

⟨proof⟩

**definition** $\mathit{OclAsBagPair} :: [(\mathfrak{A},'\alpha::null,'\alpha::null)\mathit{Pair}] \Rightarrow (\mathfrak{A},'\alpha)\mathit{Bag} ((-) \to \mathit{asBagPair}'('))$

**where** $\mathit{OclAsBagPair} S = \mathit{Bag}\{S .\mathit{First}(\mathit{S}), S .\mathit{Second}(\mathit{S})\}$

### 2.11.8. Collection Types

**lemmas** $\mathit{cp-intro}''$ [introduction, simplification, code-unfolding] =

$\mathit{cp-intro}'$

$\mathit{cp-intro}''_{\mathit{Set}}$

$\mathit{cp-intro}''_{\mathit{Seq}}$

### 2.11.9. Test Statements

**lemma** syntax-test: $\mathit{Set}\{\mathbf{2},\mathbf{1}\} = (\mathit{Set}\{\} \to \mathit{includingSet}(\mathbf{1}) \to \mathit{includingSet}(\mathbf{2}))$

⟨proof⟩

Here is an example of a nested collection.

**lemma** semantic-test2: $\mathit{H}:(\mathit{Set}\{\mathbf{2}\} \doteq \mathit{null}) = (\mathit{false}::(\mathfrak{A})\mathit{Boolean})$

**assumes** $\mathit{H}:(\mathit{Set}\{\mathbf{2}\} \doteq \mathit{null}) = (\mathit{false}::(\mathfrak{A})\mathit{Boolean})$

**shows** $(\tau::(\mathfrak{A})\mathit{st}) \models (\mathit{Set}\{\mathit{Set}\{\mathbf{2}\},\mathit{null}\} \to \mathit{includesSet}(\mathit{null}))$

⟨proof⟩

**lemma** short-cut'[simplification, code-unfolding]: $(\mathbf{8} \doteq \mathbf{6}) = \mathit{false}$

⟨proof⟩

**lemma** short-cut''[simplification, code-unfolding]: $(\mathbf{2} \doteq \mathbf{1}) = \mathit{false}$

⟨proof⟩

**lemma** short-cut'''[simplification, code-unfolding]: $(\mathbf{1} \doteq \mathbf{2}) = \mathit{false}$

⟨proof⟩

**Assert** $\tau \models (\mathbf{0} <_{\mathit{int}} \mathbf{2}) \text{ and } (\mathbf{0} <_{\mathit{int}} \mathbf{1})$

Elementary computations on Sets.
declare OclSelect-body-def [simp]

Assert ¬ (τ |= v(invalid::('A,'α::null) Set))

Assert τ |= v(null::('A,'α::null) Set)

Assert ¬ (τ |= δ(null::('A,'α::null) Set))

Assert τ |= v(Set{})

Assert τ |= v(set{2},null)

Assert τ |= δ(set{2},null)

Assert τ |= (Set{2,1} -> includes$_{Set}$(1))

Assert ¬ (τ |= (Set{2} -> includes$_{Set}$(1)))

Assert ¬ (τ |= (Set{2,1} -> includes$_{Set}$(null)))

Assert τ |= (Set{2 null} -> includes$_{Set}$(null))

Assert τ |= (Set{null,2} -> includes$_{Set}$(null))

Assert τ |= ((Set{}) -> forAll$_{Set}$(z | 0 <$_{int}$ z))

Assert τ |= ((Set{2,1}) -> forAll$_{Set}$(z | 0 <$_{int}$ z))

Assert ¬ (τ |= ((Set{2,1}) -> exists$_{Set}$(z | z <$_{int}$ 0 )))

Assert ¬ (τ |= (δ(set{2 null}) -> forAll$_{Set}$(z | 0 <$_{int}$ z)))

Assert ¬ (τ |= ((Set{2, null}) -> forAll$_{Set}$(z | 0 <$_{int}$ z)))

Assert τ |= ((Set{2, null}) -> exists$_{Set}$(z | 0 <$_{int}$ z))

Assert ¬ (τ |= (Set{null::'a Boolean} = Set{}))

Assert ¬ (τ |= (Set{null::'a Integer} = Set{}))

Assert ¬ (τ |= (Set{true} = Set{false}))

Assert ¬ (τ |= (Set{true, true} = Set{false}))

Assert ¬ (τ |= (Set{2} = Set{1}))

Assert τ |= (Set{2 null, 2} = Set{null, 2})

Assert τ |= (Set{1, null, 2} <> Set{null, 2})

Assert τ |= (Set{Set{2, null}} = Set{Set{null, 2}})

Assert τ |= (Set{Set{2, null}} <> Set{Set{null, 2}, null})

Assert τ |= (Set{null} -> select$_{Set}$(x | not x) = Set{null})

Assert τ |= (Set{null} -> reject$_{Set}$(x | not x) = Set{null})

lemma const (Set{Set{2, null}, invalid}) (proof)

Elementary computations on Sequences.

Assert ¬ (τ |= v(invalid::('A,'α::null) Sequence))

Assert τ |= v(null::('A,'α::null) Sequence)

Assert ¬ (τ |= δ(null::('A,'α::null) Sequence))

Assert τ |= v(Sequence{})

lemma const (Sequence{Sequence{2, null}, invalid}) (proof) (ML) (ML) end
<figure><img src="image_11.png" /></figure>
# 3. Formalization III: UML/OCL constructs: State Operations and Objects

**theory** UML-State

**imports** UML-Library

**begin**

**no-notation** None (⊥)

## 3.1. Introduction: States over Typed Object Universes

In the following, we will refine the concepts of a user-defined data-model (implied by a class-diagram) as well as the notion of state used in the previous section to much more detail. Surprisingly, even without a concrete notion of an objects and a universe of object representation, the generic infrastructure of state-related operations is fairly rich.

### 3.1.1. Fundamental Properties on Objects: Core Referential Equality

**Definition**

Generic referential equality - to be used for instantiations with concrete object types ...

**definition** StrictRefEqObject :: ('A,'a::{object, null}) val ⇒ ('A,'a) val ⇒ ('A) Boolean

**where** StrictRefEqObject x y

$$ \equiv \lambda \tau. \text{ if } (\upsilon x) \tau = \text{true } \tau \land (\upsilon y) \tau = \text{true } \tau $$

then if $x \tau = \text{null} \lor y \tau = \text{null}$

then $\perp_x \tau = \text{null} \land y \tau = \text{null}_\perp$

else $\perp(\text{oid-of } x \tau) = (\text{oid-of } y \tau)_\perp$

else invalid $\tau$

**Strictness and context passing**

**lemma** StrictRefEqObject-strict1 [simp, code-unfold] :

$$ (\text{StrictRefEqObject } x \text{ invalid}) = \text{invalid} $$

⟨proof⟩

**lemma** StrictRefEqObject-strict2 [simp, code-unfold] :

$$ (\text{StrictRefEqObject } \text{invalid } x) = \text{invalid} $$

⟨proof⟩

**lemma** cp-StrictRefEqObject:

$$ (\text{StrictRefEqObject } x \ y \ \tau) = (\text{StrictRefEqObject } (\lambda-. \ x \ \tau) (\lambda-. \ y \ \tau)) \ \tau $$

⟨proof⟩ **lemmas** cp0-StrictRefEqObject = cp-StrictRefEqObject[THEN allI[THEN allI[THEN allI[THEN cpI2]], of StrictRefEqObject]]

**lemmas** cp-intro''[intro!, simp, code-unfold] =

cp-intro''

cp-StrictRefEqObject[THEN allI[THEN allI[THEN allI[THEN cpI2]], of StrictRefEqObject]]
### 3.1.2. Logic and Algebraic Layer on Object

#### Validity and Definedness Properties

We derive the usual laws on definedness for (generic) object equality:

**lemma StrictRefEqObject-defargs:**

$$ \tau \models (\text{StrictRefEq}_{\text{Object}} x (y::('\mathfrak{A}','a::\{\text{null,object}\})\text{val})) \implies (\tau \models (v x) \land (\tau \models (v y))) \\ \langle\text{proof}\rangle $$

**lemma defined-StrictRefEqObject-I:**

assumes $val-x : \tau \models v x$

assumes $val-x : \tau \models v y$

shows $\tau \models \delta (\text{StrictRefEq}_{\text{Object}} x y)$

$\langle\text{proof}\rangle$

**lemma StrictRefEqObject-def-homo :**

$$ \delta(\text{StrictRefEq}_{\text{Object}} x (y::('\mathfrak{A}','a::\{\text{null,object}\})\text{val})) = ((v x) \text{ and } (v y)) $$

$\langle\text{proof}\rangle$

#### Symmetry

**lemma StrictRefEqObject-sym :**

assumes $x-val : \tau \models v x$

shows $\tau \models \text{StrictRefEq}_{\text{Object}} x x$

$\langle\text{proof}\rangle$

#### Behavior vs StrongEq

It remains to clarify the role of the state invariant $inv_\sigma(\sigma)$ mentioned above that states the condition that there is a “one-to-one” correspondence between object representations and oid’s: $\forall oid \in \text{dom } \sigma$. $oid = \text{OidOf } \lceil\sigma(oid)\rceil$. This condition is also mentioned in [32, Annex A] and goes back to Richters [33]; however, we state this condition as an invariant on states rather than a global axiom. It can, therefore, not be taken for granted that an oid makes sense both in pre- and post-states of OCL expressions.

We capture this invariant in the predicate WFF :

**definition WFF** :: ('\mathfrak{A}::\text{object})\text{st} \Rightarrow \text{bool}

**where** WFF $\tau = ((\forall x \in \text{ran}(\text{heap}(fst} \tau)). \lceil\text{heap}(fst} \tau \rceil (\text{oid-of } x) \rceil = x) \land (\forall x \in \text{ran}(\text{heap}(snd} \tau)). \lceil\text{heap}(snd} \tau \rceil (\text{oid-of } x) \rceil = x))$

It turns out that WFF is a key-concept for linking strict referential equality to logical equality: in well-formed states (i.e. those states where the self (oid-of) field contains the pointer to which the object is associated to in the state), referential equality coincides with logical equality.

We turn now to the generic definition of referential equality on objects: Equality on objects in a state is reduced to equality on the references to these objects. As in HOL-OCL [6, 8], we will store the reference of an object inside the object in a (ghost) field. By establishing certain invariants (“consistent state”), it can be assured that there is a “one-to-one-correspondence” of objects to their references—and therefore the definition below behaves as we expect.

Generic Referential Equality enjoys the usual properties: (quasi) reflexivity, symmetry, transitivity, substitutivity for defined values. For type-technical reasons, for each concrete object type, the equality $\doteq$ is defined by generic referential equality.

**theorem StrictRefEqObject-vs-StrongEq:**

assumes WFF : WFF $\tau$

and valid-x: $\tau \models (v x)$

and valid-y: $\tau \models (v y)$

and x-present-pre: $x \tau \in \text{ran} (\text{heap}(fst} \tau))$

and y-present-pre: $y \tau \in \text{ran} (\text{heap}(fst} \tau))$
and $x$-present-post:$x \tau \in \text{ran}(\text{heap}(\text{snd } \tau))$

and $y$-present-post:$y \tau \in \text{ran}(\text{heap}(\text{snd } \tau))$

shows $(\tau \models (\text{StrictRefEq}_{\text{Object}} x y)) = (\tau \models (x \triangleq y))$
\textit{\<proof\>}

theorem $\text{StrictRefEq}_{\text{Object}}$-vs-$\text{StrongEq}'$:

assumes WFF: WFF $\tau$

and valid-$x$: $\tau \models (v (x :: ('A::object, 'a::{null, object}) val))$

and valid-$y$: $\tau \models (v y)$

and oid-preserve: $\bigwedge x. x \in \text{ran}(\text{heap}(\text{fst } \tau)) \lor x \in \text{ran}(\text{heap}(\text{snd } \tau)) \implies$
$H x \neq \perp \implies \text{oid-of}(H x) = \text{oid-of} x$

and $xy$-together: $x \tau \in H, \text{ran}(\text{heap}(\text{fst } \tau)) \land y \tau \in H, \text{ran}(\text{heap}(\text{fst } \tau)) \lor$
$x \tau \in H, \text{ran}(\text{heap}(\text{snd } \tau)) \land y \tau \in H, \text{ran}(\text{heap}(\text{snd } \tau))$

shows $(\tau \models (\text{StrictRefEq}_{\text{Object}} x y)) = (\tau \models (x \triangleq y))$
\textit{\<proof\>}

So, if two object descriptions live in the same state (both pre or post), the referential equality on
objects implies in a WFF state the logical equality.

## 3.2. Operations on Object

### 3.2.1. Initial States (for testing and code generation)

definition $\tau_0 :: ('A)st$

where $\tau_0 \equiv ((|\text{heap}=\text{Map.empty, assocs} = \text{Map.empty}|), (|\text{heap}=\text{Map.empty, assocs} = \text{Map.empty}|))$

### 3.2.2. OclAllInstances

To denote OCL types occurring 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 a sufficient “characterization.”

definition $\text{OclAllInstances-generic} :: (('A::object) st \Rightarrow 'A state) \Rightarrow ('A::object \to '\alpha) \Rightarrow$ 
('A, '$\alpha$ option option) Set

where $\text{OclAllInstances-generic} \text{fst-snd } H = (\lambda\tau. \text{Abs-Set}_{\text{base}} \sqsubseteq \text{Some '}} ((H '\text{ran} (\text{heap (fst-snd } \tau))) - \{ \text{None} \}) \sqsupseteq)$

lemma $\text{OclAllInstances-generic-defined}: \tau \models \delta (\text{OclAllInstances-generic pre-post } H)$
\textit{\<proof\>}

lemma $\text{OclAllInstances-generic-init-empty}$:

assumes $[\mathit{simp}]: \bigwedge x. \mathit{pre-post}(x, x) = x$

shows $\tau_0 \models \text{OclAllInstances-generic pre-post } H \triangleq \text{Set}\{\}$
\textit{\<proof\>}

lemma represented-generic-objects-nonnull:

assumes A: $\tau \models ((\text{OclAllInstances-generic pre-post } (H::('A::object \to '\alpha))) \rightarrow \text{includes}_{\text{Set}}(x))$

shows $\tau \models \text{not}(x \triangleq \text{null})$

\<proof\>

lemma represented-generic-objects-defined:

assumes A: $\tau \models ((\text{OclAllInstances-generic pre-post } (H::('A::object \to '\alpha))) \rightarrow \text{includes}_{\text{Set}}(x))$

shows $\tau \models \delta (\text{OclAllInstances-generic pre-post } H) \land \tau \models \delta x$
〈proof〉

One way to establish the actual presence of an object representation in a state is:

**definition** is-represented-in-state fst-snd x H τ = (x τ ∈ (Some o H) ' ran (heap (fst-snd τ)))

**lemma** represented-generic-objects-in-state:

assumes A: τ |= (OclAllInstances-generic pre-post H) → >includes$_{Set}$(x)

shows is-represented-in-state pre-post x H τ

〈proof〉

**lemma** state-update-vs-allInstances-generic-empty:

assumes [simp]: ⋀a. pre-post (mk a) = a

shows (mk (|heap=empty, assocs=A|)) |= OclAllInstances-generic pre-post Type ≜ Set{}

〈proof〉

Here comes a couple of operational rules that allow to infer the value of oclAllInstances from the context τ. These rules are a special-case in the sense that they are the only rules that relate statements with different τ's. For that reason, new concepts like "constant contexts P" are necessary (for which we do not elaborate an own theory for reasons of space limitations; in examples, we will prove resulting constraints straight forward by hand).

**lemma** state-update-vs-allInstances-generic-including':

assumes [simp]: ⋀a. pre-post (mk a) = a

assumes ⋀x. σ' oid = Some x = ⇒ x = Object

and Type Object ≠ None

shows (OclAllInstances-generic pre-post Type)

$$
 mk (|heap=\sigma'(oid \to Object), \text{assocs}=A|)
$$

=

((OclAllInstances-generic pre-post Type) → >including$_{Set}$(λ - . ⊥ drop (Type Object) ⊥)))

$$
 mk (|heap=\sigma', \text{assocs}=A|)
$$

〈proof〉

**lemma** state-update-vs-allInstances-generic-including:

assumes [simp]: ⋀a. pre-post (mk a) = a

assumes ⋀x. σ' oid = Some x = ⇒ x = Object

and Type Object ≠ None

shows (OclAllInstances-generic pre-post Type)

$$
 mk (|heap=\sigma'(oid \to Object), \text{assocs}=A|)
$$

=

((λ-. (OclAllInstances-generic pre-post Type)
 (mk (|heap=σ', assocs=A|))) → including$_{Set}$(λ - . ⊥ drop (Type Object) ⊥)))

$$
 mk (|heap=\sigma'(oid \to Object), \text{assocs}=A|)
$$

〈proof〉

**lemma** state-update-vs-allInstances-generic-noincluding':

assumes [simp]: ⋀a. pre-post (mk a) = a

assumes ⋀x. σ' oid = Some x = ⇒ x = Object

and Type Object = None

shows (OclAllInstances-generic pre-post Type)

$$
 mk (|heap=\sigma'(oid \to Object), \text{assocs}=A|)
$$

=

(OclAllInstances-generic pre-post Type)

$$
 mk (|heap=\sigma', \text{assocs}=A|)
$$

〈proof〉
**theorem state-update-vs-allInstances-generic-ntc:**

**assumes** [simp]: $\bigwedge a. \text{ pre-post } (mk a) = a$

**assumes** oid-def: $oid \notin \text{dom } \sigma'$

**and** non-type-conform: Type Object = None

**and** cp-ctx: $cp P$

**and** const-ctx: $\bigwedge X. \text{ const } X \implies \text{ const } (P X)$

**shows** $(mk (|heap=\sigma'(oid \to Object),assocs=A|) \models P (\text{OclAllInstances-generic pre-post Type})) = (mk (|heap=\sigma', assocs=A|) \models P (\text{OclAllInstances-generic pre-post Type}))$

(is $(?\tau \models P ?\varphi) = (?\tau' \models P ?\varphi))$

(*proof*)

**theorem state-update-vs-allInstances-generic-tc:**

**assumes** [simp]: $\bigwedge a. \text{ pre-post } (mk a) = a$

**assumes** oid-def: $oid \notin \text{dom } \sigma'$

**and** type-conform: Type Object $\neq$ None

**and** cp-ctx: $cp P$

**and** const-ctx: $\bigwedge X. \text{ const } X \implies \text{ const } (P X)$

**shows** $(mk (|heap=\sigma'(oid \to Object),assocs=A|) \models P (\text{OclAllInstances-generic pre-post Type})) = (mk (|heap=\sigma', assocs=A|) \models P ((\text{OclAllInstances-generic pre-post Type}) \rightarrow \text{including}_{\text{Set}}(\lambda . - \lfloor \text{Type Object} \rfloor)))$

(is $(?\tau \models P ?\varphi) = (?\tau' \models P ?\varphi'))$

(*proof*)

**declare** OclAllInstances-generic-def [simp]

## OclAllInstances (@post)

**definition** OclAllInstances-at-post :: ('A :: object $\to$ '$\alpha$') $\Rightarrow$ ('A, '$\alpha$ option option) Set
(- .allInstances' ('))

**where** OclAllInstances-at-post = OclAllInstances-generic snd

**lemma** OclAllInstances-at-post-defined: $\tau \models \delta (H . \text{allInstances()})$

(*proof*)

**lemma** $\tau_0 \models H . \text{allInstances()} \triangleq \text{Set}\{\}$

(*proof*)

**lemma represented-at-post-objects-nonnull:**

**assumes** A: $\tau \models (((H::('A::object $\to$ '$\alpha$)).\text{allInstances()} \rightarrow \text{includes}_{\text{Set}}(x))$

**shows** $\tau \models \text{not}(x \triangleq \text{null})$

(*proof*)

**lemma represented-at-post-objects-defined:**

**assumes** A: $\tau \models (((H::('A::object $\to$ '$\alpha$)).\text{allInstances()} \rightarrow \text{includes}_{\text{Set}}(x))$

**shows** $\tau \models \delta (H . \text{allInstances()} \land \tau \models \delta x)$

(*proof*)

One way to establish the actual presence of an object representation in a state is:

**lemma**

**assumes** A: $\tau \models H . \text{allInstances()} \rightarrow \text{includes}_{\text{Set}}(x)$

**shows** is-represented-in-state snd $x H \tau$

(*proof*)

**lemma state-update-vs-allInstances-at-post-empty:**

**shows** $(\sigma, (|heap=\text{empty}, assocs=A|) \models \text{Type} . \text{allInstances()} \doteq \text{Set}\{\}$
〈proof〉

Here comes a couple of operational rules that allow to infer the value of oclAllInstances from the context $\tau$. These rules are a special-case in the sense that they are the only rules that relate statements with different $\tau$'s. For that reason, new concepts like "constant contexts P" are necessary (for which we do not elaborate an own theory for reasons of space limitations; in examples, we will prove resulting constraints straight forward by hand).

**lemma state-update-vs-allInstances-at-post-including':**

assumes $\bigwedge x. \sigma' oid = \text{Some } x \implies x = \text{Object}$
and Type Object $\neq$ None

shows (Type .allInstances())
($\sigma$, ($\lfloor heap=\sigma'(oid \to Object), assocs=A \rfloor$))
$=$
((Type .allInstances()) $\to$ including$_{Set}$ ($\lambda . \lfloor \text{drop (Type Object)} \rfloor$))
($\sigma$, ($\lfloor heap=\sigma', assocs=A \rfloor$))

<proof>

**lemma state-update-vs-allInstances-at-post-including:**

assumes $\bigwedge x. \sigma' oid = \text{Some } x \implies x = \text{Object}$
and Type Object $\neq$ None

shows (Type .allInstances())
($\sigma$, ($\lfloor heap=\sigma'(oid \to Object), assocs=A \rfloor$))
$=$
((\$\lambda\$. (Type .allInstances()))
($\sigma$, ($\lfloor heap=\sigma', assocs=A \rfloor$)) $\to$ including$_{Set}$ ($\lambda . \lfloor \text{drop (Type Object)} \rfloor$))
($\sigma$, ($\lfloor heap=\sigma', assocs=A \rfloor$))

<proof>

**lemma state-update-vs-allInstances-at-post-noincluding':**

assumes $\bigwedge x. \sigma' oid = \text{Some } x \implies x = \text{Object}$
and Type Object = None

shows (Type .allInstances())
($\sigma$, ($\lfloor heap=\sigma'(oid \to Object), assocs=A \rfloor$))
$=$
(Type .allInstances())
($\sigma$, ($\lfloor heap=\sigma', assocs=A \rfloor$))

<proof>

**theorem state-update-vs-allInstances-at-post-ntc:**

assumes oid-def: oid $\notin$ dom $\sigma'$
and non-type-conform: Type Object = None

and cp-ctx: cp P

and const-ctx: $\bigwedge X. \text{const } X \implies \text{const } (P X)$
shows (($\sigma$, ($\lfloor heap=\sigma'(oid \to Object), assocs=A \rfloor$)) $\models$ (P(Type .allInstances())) =
(($\sigma$, ($\lfloor heap=\sigma', assocs=A \rfloor$)) $\models$ (P(Type .allInstances()))))

<proof>

**theorem state-update-vs-allInstances-at-post-tc:**

assumes oid-def: oid $\notin$ dom $\sigma'$
and type-conform: Type Object $\neq$ None

and cp-ctx: cp P

and const-ctx: $\bigwedge X. \text{const } X \implies \text{const } (P X)$
shows (($\sigma$, ($\lfloor heap=\sigma'(oid \to Object), assocs=A \rfloor$)) $\models$ (P(Type .allInstances())) =
(($\sigma$, ($\lfloor heap=\sigma', assocs=A \rfloor$)) $\models$ (P((Type .allInstances()))))
->includingSet(λ - .(Type Object)_)))

<proof>

## OclAllInstances (@pre)

**definition** OclAllInstances-at-pre :: ('A :: object → 'α) ⇒ ('A, 'α option option) Set
(- .allInstances@pre'())

**where** OclAllInstances-at-pre = OclAllInstances-generic fst

**lemma** OclAllInstances-at-pre-defined: τ |= δ (H .allInstances@pre())

<proof>

**lemma** τ₀ |= H .allInstances@pre() ≜ Set{}

<proof>

**lemma** represented-at-pre-objects- nonnull:

**assumes** A: τ |= (((H::('A::object → 'α)).allInstances@pre()) -> includesSet(x))

**shows** τ |= not(x ≜ null)

<proof>

**lemma** represented-at-pre-objects-defined:

**assumes** A: τ |= (((H::('A::object → 'α)).allInstances@pre()) -> includesSet(x))

**shows** τ |= δ (H .allInstances@pre()) ∧ τ |= δ x

<proof>

One way to establish the actual presence of an object representation in a state is:

**lemma**

**assumes** A: τ |= H .allInstances@pre() -> includesSet(x)

**shows** is-represented-in-state fst x H τ

<proof>

**lemma** state-update-vs-allInstances-at-pre-empty:

**shows** (|heap=empty, assocs=A|), σ |= Type .allInstances@pre() ≜ Set{}

<proof>

Here comes a couple of operational rules that allow to infer the value of oclAllInstances@pre from the context τ. These rules are a special-case in the sense that they are the only rules that relate statements with different τ's. For that reason, new concepts like "constant contexts P" are necessary (for which we do not elaborate an own theory for reasons of space limitations; in examples, we will prove resulting constraints straight forward by hand).

**lemma** state-update-vs-allInstances-at-pre-including':

**assumes** A x. σ' oid = Some x =⇒ x = Object

and Type Object ≠ None

**shows** (Type .allInstances@pre())

|(heap=σ'(oid→Object), assocs=A|), σ|

=

|((Type .allInstances@pre()) -> includingSet(λ - .(Type Object)_)))

|(heap=σ', assocs=A|), σ|

<proof>

**lemma** state-update-vs-allInstances-at-pre-including:

**assumes** A x. σ' oid = Some x =⇒ x = Object

and Type Object ≠ None

**shows** (Type .allInstances@pre())
((heap=σ'(oid→Object), assocs=A], σ)
= ((λ-. (Type .allInstances@pre()) ((heap=σ', assocs=A], σ)))->including$_{Set}$(λ -. ⊥ drop (Type Object) ⊥)) ((heap=σ'(oid→Object), assocs=A], σ)
<proof>

lemma state-update-vs-allInstances-at-pre-noincluding':

assumes A x. σ' oid = Some x =⇒ x = Object
and Type Object = None

shows (Type .allInstances@pre())
((heap=σ'(oid→Object), assocs=A], σ)
=
(Type .allInstances@pre())
((heap=σ', assocs=A], σ)
<proof>

theorem state-update-vs-allInstances-at-pre-ntc:

assumes oid-def: oid ∉ dom σ'

and non-type-conform: Type Object = None

and cp-ctx: cp P

and const-ctx: ⋀ X. const X =⇒ const (P X)

shows (((heap=σ'(oid→Object),assocs=A], σ) |- (P(Type .allInstances@pre())) = ((|heap=σ', assocs=A|], σ) |- (P(Type .allInstances@pre())))
<proof>

theorem state-update-vs-allInstances-at-pre-tc:

assumes oid-def: oid ∉ dom σ'

and type-conform: Type Object ≠ None

and cp-ctx: cp P

and const-ctx: ⋀ X. const X =⇒ const (P X)

shows (((heap=σ'(oid→Object),assocs=A], σ) |- (P(Type .allInstances@pre())) = ((|heap=σ', assocs=A|], σ) |- (P((Type .allInstances@pre()) ->including$_{Set}$(λ -. ⊥ (Type Object) ⊥)))))
<proof>

@post or @pre

theorem StrictRefEq$_{Object}$-vs-StrongEq'':

assumes WFF: WFF τ

and valid-x: τ |- (v (x :: ('A::object,'α::object option option) val))

and valid-y: τ |- (v y)

and oid-preserve: ⋀ x. x ∈ ran (heap(fst τ)) ∨ x ∈ ran (heap(snd τ)) =⇒
oid-of (H x) = oid-of x

and xy-together: τ |- ((H .allInstances() -> includes$_{Set}$(x) and H .allInstances() -> includes$_{Set}$(y)) or
(H .allInstances@pre() -> includes$_{Set}$(x) and H .allInstances@pre() -> includes$_{Set}$(y)))

shows (τ |- (StrictRefEq$_{Object}$ x y)) = (τ |- (x ≜ y))
<proof>

3.2.3. OcllsNew, OcllsDeleted, OcllsMaintained, OcllsAbsent

definition OcllsNew:: ('A, 'α::{null,object})val ⇒ ('A)Boolean ((-).ocllsNew'('))

where X .ocllsNew() ≡ (λτ . if (δ X) τ = true τ

then ⊥oid-of (X τ) ∉ dom (heap (fst τ)) ∧
oid-of (X τ) ∈ dom (heap (snd τ)) ⊥
else invalid τ)

The following predicates — which are not part of the OCL standard descriptions — complete the goal of oclIsNew by describing where an object belongs.

**definition** *OclIsDeleted*:: ('A, 'α::{null,object})val ⇒ ('A)Boolean ((-).oclIsDeleted'('))

where
X .oclIsDeleted() ≡ (λτ . if (δ X) τ = true τ
then ⊥oid-of (X τ) ∈ domABL heap(fst τ)) ∧
oid-of (X τ) ∉ domABL heap(snd τ))⊥
else invalid τ)

definition *OclIsMaintained*:: ('A, 'α::{null,object})val ⇒ ('A)Boolean((-).oclIsMaintained'('))

where
X .oclIsMaintained() ≡ (λτ . if (δ X) τ = true τ
then ⊥oid-of (X τ) ∈ domABL heap(fst τ)) ∧
oid-of (X τ) ∈ domABL heap(snd τ))⊥
else invalid τ)

definition *OclIsAbsent*:: ('A, 'α::{null,object})val ⇒ ('A)Boolean ((-).oclIsAbsent'('))

where
X .oclIsAbsent() ≡ (λτ . if (δ X) τ = true τ
then ⊥oid-of (X τ) /∈ domABL heap(fst τ)) ∧
oid-of (X τ) /∈ domABL heap(snd τ))⊥
else invalid τ)

**lemma** state-split : τ ⊨ δ X ⇒
τ ⊨ (X .oclIsNew()) ∨ τ ⊨ (X .oclIsDeleted()) ∨
τ ⊨ (X .oclIsMaintained()) ∨ τ ⊨ (X .oclIsAbsent())
<proof>

**lemma** notNew-vs-others : τ ⊨ δ X ⇐
(¬ τ ⊨ (X .oclIsNew())) = (τ ⊨ (X .oclIsDeleted()) ∨
τ ⊨ (X .oclIsMaintained()) ∨ τ ⊨ (X .oclIsAbsent()))
<proof>

3.2.4. OcllsModifiedOnly

**Definition**

The following predicate—which is not part of the OCL standard—provides a simple, but powerful means to describe framing conditions. For any formal approach, be it animation of OCL contracts, test-case generation or die-hard theorem proving, the specification of the part of a system transition that *does not change* is of primordial importance. The following operator establishes the equality between old and new objects in the state (provided that they exist in both states), with the exception of those objects.

**definition** *OclIsModifiedOnly* :: ('A::: object, 'α::{null, object})Set ⇒ 'A Boolean
(--> oclIsModifiedOnly'('))

where
X->oclIsModifiedOnly() ≡ (λ(σ,σ').
let X' = (oid-of 'Rep-Set<base>(X(σ,σ'))<sup>n</sup>);
S = ((dom (heap σ) ∩ dom (heap σ')) - X');
in if (δ X) (σ,σ') = true (σ,σ') ∧ (∀x∈<sup>n</sup>Rep-Set<base>(X(σ,σ'))<sup>n</sup>. x ≠ null)
then ⊥∀x ∈ S. (heap σ) x = (heap σ') x<sub>⊥</sub>
else invalid (σ,σ')
)

Execution with Invalid or Null or Null Element as Argument

lemma invalid->oclIsModifiedOnly() = invalid
<proof>

lemma null->oclIsModifiedOnly() = invalid
<proof>
**lemma**

assumes $X-\text{null} : \tau \models X \rightarrow \text{includes}_{\text{Set}}(\text{null})$

shows $\tau \models X \rightarrow \text{oclIsModifiedOnly()} \triangleq \text{invalid}$

(*proof*)

### Context Passing

lemma `cp-OclIsModifiedOnly`: $X \rightarrow \text{oclIsModifiedOnly}() \tau = (\lambda-. X \tau) \rightarrow \text{oclIsModifiedOnly}() \tau$

(*proof*)

## 3.2.5. OclSelf

The following predicate—which is not part of the OCL standard—explicitly retrieves in the pre or post state the original OCL expression given as argument.

**definition** [simp]: OclSelf $x H$ `fst-snd` = ($\lambda\tau$. if ($\delta x$) $\tau$ = true $\tau$ then if oid-of ($x \tau$) $\in$ dom，《heap（fst $\tau$）》) $\land$ oid-of ($x \tau$) $\in$ dom，《heap（$\text{snd} \tau$）》 then $H^\Gamma$，《heap（fst-snd $\tau$）》（oid-of ($x \tau$)）$\Gamma$ else invalid $\tau$ else invalid $\tau$)

**definition** `OclSelf-at-pre` :: ('A::object, 'a::{null, object}) val $\Rightarrow$
('A $\Rightarrow$ '$\alpha$') $\Rightarrow$
('A::object, '$\alpha$'::{null, object}) val ((-) @ `pre` (-))

where $x$ `@pre H = OclSelf x H $fst$

**definition** `OclSelf-at-post` :: ('A::object, 'a::{null, object}) val $\Rightarrow$
('A $\Rightarrow$ '$\alpha$') $\Rightarrow$
('A::object, '$\alpha$'::{null, object}) val ((-) @ `post` (-))

where $x$ `@post H = OclSelf x H $snd$

## 3.2.6. Framing Theorem

**lemma** all-oid-diff:

assumes `def-x`: $\tau \models \delta x$

assumes `def-X`: $\tau \models \delta X$

assumes `def-X'`: $\bigwedge x. x \in \Gamma \text{Rep-Set}_{\text{base}} (X \tau)^\Gamma \implies x \neq \text{null}$

defines $P \equiv (\lambda a. \text{not } (\text{StrictRefEq}_{\text{Object}} a))$

shows $(\tau \models X \rightarrow \text{forallAll}_{\text{Set}}(a|P a)) = (\text{oid-of}(x \tau) \notin \text{oid-of}^\Gamma \text{Rep-Set}_{\text{base}}(X \tau)^\Gamma)$

(*proof*)

**theorem** framing:

assumes `modifiesclause`: $\tau \models (X \rightarrow \text{excluding}_{\text{Set}}(x)) \rightarrow \text{oclIsModifiedOnly()}$

and `oid-is-typerepr`: $\tau \models X \rightarrow \text{forallAll}_{\text{Set}}(a | \text{not } (\text{StrictRefEq}_{\text{Object}} a))$

shows $\tau \models (x \text{ @pre } P \triangleq (x \text{ @post } P))$

(*proof*)

As corollary, the framing property can be expressed with only the strong equality as comparison operator.

**theorem** framing':

assumes `wff`: WFF $\tau$

assumes `modifiesclause`: $\tau \models (X \rightarrow \text{excluding}_{\text{Set}}(x)) \rightarrow \text{oclIsModifiedOnly()}$

and `oid-is-typerepr`: $\tau \models X \rightarrow \text{forallAll}_{\text{Set}}(a | \text{not } (x \triangleq a))$

and `oid-preserve`: $\bigwedge x. x \in \text{ran} (\text{heap}（\text{fst } \tau）) \lor x \in \text{ran} (\text{heap}（\text{snd } \tau）) \implies \text{oid-of} (H x) = \text{oid-of} x$

and `xy-together`:
$\tau \models X \rightarrow \text{forallAll}_{Set}(y \mid (H \cdot \text{allInstances}(\cdot) \rightarrow \text{includes}_{Set}(x) \text{ and } H \cdot \text{allInstances}(\cdot) \rightarrow \text{includes}_{Set}(y)) \text{ or} (H \cdot \text{allInstances}(\cdot) \rightarrow \text{includes}_{Set}(x) \text{ and } H \cdot \text{allInstances}(\cdot) \rightarrow \text{includes}_{Set}(y)))$

**shows** $\tau \models (x \text{ @pre } P \triangleq (x \text{ @post } P))$

*proof*

### 3.2.7. Miscellaneous

**lemma pre-post-new:** $\tau \models (x . \text{oclIsNew}()) \impl \neg (\tau \models \nu(x \text{ @pre } H1)) \wedge \neg (\tau \models \nu(x \text{ @post } H2))$

*proof*

**lemma pre-post-old:** $\tau \models (x . \text{oclIsDeleted()}) \impl \neg (\tau \models \nu(x \text{ @pre } H1)) \wedge \neg (\tau \models \nu(x \text{ @post } H2))$

*proof*

**lemma pre-post-absent:** $\tau \models (x . \text{oclIsAbsent()}) \impl \neg (\tau \models \nu(x \text{ @pre } H1)) \wedge \neg (\tau \models \nu(x \text{ @post } H2))$

*proof*

**lemma pre-post-maintained:** $(\tau \models \nu(x \text{ @pre } H1) \lor \tau \models \nu(x \text{ @post } H2)) \impl \tau \models (x . \text{oclIsMaintained()})$

*proof*

**lemma pre-post-maintained':**
$\tau \models (x . \text{oclIsMaintained()}) \impl (\tau \models \nu(x \text{ @pre } (\text{Some } o \ H1)) \land \tau \models \nu(x \text{ @post } (\text{Some } o \ H2)))$

*proof*

**lemma framing-same-state:** $(\sigma, \sigma) \models (x \text{ @pre } H \triangleq (x \text{ @post } H))$

*proof*

## 3.3. Accessors on Object

### 3.3.1. Definition

**definition** `select-object mt incl smash deref l = smash (foldl incl mt (map deref l))`
`(* smash returns null with mt in input (in this case, object contains null pointer) *)`

The continuation $f$ is usually instantiated with a smashing function which is either the identity $id$ or, for 0..1 cardinalities of associations, the UML-Sequence.OclANY-selector which also handles the null-cases appropriately. A standard use-case for this combinator is for example:

**term** `(select-object mtSet UML-Set.OclIncluding UML-Set.OclANY f l oid )::('A, 'a::null) val`

**definition** `select-objectSet = select-object mtSet UML-Set.OclIncluding id`

**definition** `select-object-any0Set f s-set = UML-Set.OclANY (select-objectSet f s-set)`

**definition** `select-object-anySet f s-set =`
`(let s = select-objectSet f s-set in
  if s->sizeSet() $\triangleq$ 1 then
    s->anySet()
  else
    $\bot$
  endif)`

**definition** `select-objectSeq = select-object mtSequence UML-Sequence.OclIncluding id`

**definition** `select-object-anySeq f s-set = UML-Sequence.OclANY (select-objectSeq f s-set)`

**definition** `select-objectPair f1 f2 = (\lambda(a,b). OclPair (f1 a) (f2 b))`

### 3.3.2. Validity and Definedness Properties

**lemma select-fold-execSeq:**

**assumes** `list-all (\lambda f. (\tau \models \nu f)) l`

**shows** `$\sqsuperscript{\text{Rep-Sequencebase}}(\text{foldl UML-Sequence.OclIncluding Sequence}\{\}\ l \tau)^\top = \text{List.map } (\lambda f. f \tau) l$
**lemma select-fold-exec<sub>Set</sub>:**

assumes list-all (λf. (τ |= v f)) l

shows ⊤Rep-Set<sub>base</sub> (foldl UML-Set.OclIncluding Set{} l τ)⊤ = set (List.map (λf. f τ) l)
<proof>

**lemma fold-val-elem<sub>Seq</sub>:**

assumes τ |= v (foldl UML-Sequence.OclIncluding Sequence{} (List.map (f p) s-set))

shows list-all (λx. (τ |= v (f p x))) s-set
<proof>

**lemma fold-val-elem<sub>Set</sub>:**

assumes τ |= v (foldl UML-Set.OclIncluding Set{} (List.map (f p) s-set))

shows list-all (λx. (τ |= v (f p x))) s-set
<proof>

**lemma select-object-any-defined<sub>Seq</sub>:**

assumes def-sel: τ |= δ (select-object-any<sub>Seq</sub> f s-set)

shows s-set ≠ []
<proof>

**lemma**

assumes def-sel: τ |= δ (select-object-any<sub>0</sub> Set f s-set)

shows s-set ≠ []
<proof>

**lemma select-object-any-defined<sub>Set</sub>:**

assumes def-sel: τ |= δ (select-object-any<sub>Set</sub> f s-set)

shows s-set ≠ []
<proof>

**lemma select-object-any-exec<sub>0</sub>Seq:**

assumes def-sel: τ |= δ (select-object-any<sub>Seq</sub> f s-set)

shows τ |= (select-object-any<sub>Seq</sub> f s-set ≜ f (hd s-set))
<proof>

**lemma select-object-any-exec<sub>Set</sub>:**

assumes def-sel: τ |= δ (select-object-any<sub>Set</sub> f s-set)

shows ∃ e. List member s-set e ∧ (τ |= (select-object-any<sub>Set</sub> f s-set ≜ f e))
<proof>

**lemma**

assumes def-sel: τ |= δ (select-object-any<sub>0</sub> Set f s-set)

shows ∃ e. List member s-set e ∧ (τ |= (select-object-any<sub>0</sub> Set f s-set ≜ f e))
<proof>

**lemma select-object-any-exec<sub>Set</sub>:**

assumes def-sel: τ |= δ (select-object-any<sub>Set</sub> f s-set)

shows ∃ e. List member s-set e ∧ (τ |= (select-object-any<sub>Set</sub> f s-set ≜ f e))
<proof>

end

theory UML-Contracts

imports UML-State
### begin

Modeling of an operation contract for an operation with 2 arguments, (so depending on three parameters if one takes "self" into account).

locale contract-scheme =

fixes f-v

fixes f-lam

fixes f :: ('A, 'α0::null) val ⇒
'b ⇒
('A, 'res::null) val

fixes PRE

fixes POST

assumes def-scheme': f self x ≡ (λ τ. SOME res. let res = λ -. res in
  if (τ |= (δ self)) ∧ f-v x τ
  then (τ |= PRE self x) ∧
        (τ |= POST self x res)
  else τ |= res ≜ invalid)

assumes all-post': ∀ σ σ' σ''. ((σ,σ') |= PRE self x) = ((σ,σ'') |= PRE self x)

assumes cp<sub>PRE</sub>: PRE (self) x τ = PRE (λ -. self τ) (f-lam x τ) τ

assumes cp<sub>POST</sub>: POST (self) x (res) τ = POST (λ -. self τ) (f-lam x τ) (λ -. res τ) τ

assumes f-v-val: ⋀a1. f-v (f-lam a1 τ) τ = f-v a1 τ

### begin

lemma strict0 [simp]: f invalid X = invalid
<proof>

lemma nullstrict0 [simp]: f null X = invalid
<proof>

lemma cp0 : f self a1 τ = f (λ -. self τ) (f-lam a1 τ) τ
<proof>

### theorem unfold':

assumes context-ok: cp E

and args-def-or-valid: (τ |= δ self) ∧ f-v a1 τ

and pre-satisfied: τ |= PRE self a1

and post-satisfiable: ∃ res. (τ |= POST self a1 (λ -. res))

and sat-for-sols-post: (∩res. τ |= POST self a1 (λ -. res)) =⇒ τ |= E (λ -. res))

shows
τ |= E(f self a1)

<proof>

### lemma unfold2':

assumes context-ok: cp E

and args-def-or-valid: (τ |= δ self) ∧ (f-v a1 τ)

and pre-satisfied: τ |= PRE self a1

and postsplit-satisfied: τ |= POST' self a1

and post-decomposable : ⋀ res. (POST self a1 res) =
((POST' self a1) and (res ≜ (BODY self a1)))

shows (τ |= E(f self a1)) = (τ |= E(BODY self a1))

<proof>

### end

locale contract0 =

fixes f :: ('A, 'α0::null) val ⇒
('A, 'res::null) val
fixes *PRE*

fixes *POST*

assumes def-scheme: $f \ self \equiv (\lambda \tau. \ SOME \ res. \ let \ res = \lambda -. \ res \ in$
\quad if $\langle \tau \models (\delta \ self) \rangle$
\quad then $\langle \tau \models \ PRE \ self \rangle \wedge$
\quad \quad $\langle \tau \models \ POST \ self \ res \rangle$
\quad else $\tau \models \ res \triangleq \ invalid \rangle$

assumes all-post: $\forall \sigma \sigma' \sigma''$. $((\sigma,\sigma') \models \text{PRE self}) = ((\sigma,\sigma'') \models \text{PRE self})$

assumes $cp_{PRE}: \text{PRE}(\text{self}) \quad \tau = \text{PRE}(\lambda -. \text{self} \quad \tau) \quad \tau$

assumes $cp_{POST}: \text{POST}(\text{self}) (\text{res}) \quad \tau = \text{POST}(\lambda -. \text{self} \quad \tau) (\lambda -. \text{res} \quad \tau) \quad \tau$

sublocale contract0 < contract-scheme $\lambda-. \text{ True} \ \lambda x -. \ x \ \lambda x -. \ f \ x \ \lambda x -. \ PRE \ x \ \lambda x -. \ POST \ x$
$\langle \text{proof} \rangle$

context contract0

begin

lemma cp-pre: cp self' = cp (\lambda X. PRE (self' X))
$\langle \text{proof} \rangle$

lemma cp-post: cp self' = cp res' = cp (\lambda X. POST (self' X) (res' X))
$\langle \text{proof} \rangle$

lemma cp [simp]: cp self' = cp res' = cp (\lambda X. f (self' X))
$\langle \text{proof} \rangle$

lemmas unfold = unfold'[simplified]

lemma unfold2 :

assumes cp E
and (τ |= δ self)
and τ |= PRE self
and τ |= POST' self
and $\bigwedge$ res. (POST self res) = ((POST' self) and (res ≜ (BODY self)))

shows (τ |= E(f self)) = (τ |= E(BODY self))
$\langle \text{proof} \rangle$

end

locale contract1 =

fixes f :: ('A, 'α0::null) val ⇒
('A, 'α1::null) val ⇒
('A, 'res::null) val

fixes PRE

fixes *POST*

assumes def-scheme: f self a1 ≡
(λ τ. SOME res. let res = λ -. res in
  if (τ |= (δ self)) ∧ (τ |= v a1)
  then (τ |= PRE self a1) ∧
  (τ |= POST self a1 res)
  else τ |= res ≜ invalid)

assumes all-post: ∀ σ σ' σ''. ((σ,σ') |= PRE self a1) = ((σ,σ'') |= PRE self a1)

assumes $cp_{PRE}: \text{PRE}(\text{self}) (\text{a1}) \quad \tau = \text{PRE}(\lambda -. \text{self} \quad \tau) (\lambda -. \text{a1} \quad \tau) \quad \tau$
assumes `cpPOST:POST(self)(a1)(res) τ = POST(λ -. self τ)(λ -. a1 τ) (λ -. res τ) τ`

sublocale `contract1 < contract-scheme λa1 τ. (τ |= v a1) λa1 τ. (λ -. a1 τ)`
*<proof>*

context `contract1`

begin

lemma `strict1[simp]: f self invalid = invalid`
*<proof>*

lemma `defined-mono`: `τ |= v(f Y Z) ⇒ (τ |= δ Y) ∧ (τ |= v Z)`
*<proof>*

lemma `cp-pre`: `cp self' ⇒ cp a1' ⇒ cp (λX. PRE (self' X) (a1' X))`
*<proof>*

lemma `cp-post`: `cp self' ⇒ cp a1' ⇒ cp res'`
⇒ `cp (λX. POST (self' X) (a1' X) (res' X))`
*<proof>*

lemma `cp [simp]: cp self' ⇒ cp a1' ⇒ cp res' ⇒ cp (λX. f (self' X) (a1' X))`
*<proof>*

lemmas `unfold = unfold'`

lemmas `unfold2 = unfold2'`

end

locale `contract2 =`

fixes `f :: ('A, 'α0::null) val ⇒ ('A, 'α1::null) val ⇒ ('A, 'α2::null) val ⇒ ('A, 'res::null) val`

fixes `PRE`

fixes `POST`

assumes `def-scheme: f self a1 a2 ≡`
(λ τ. SOME res. let res = λ -. res in
  if (τ |= (δ self)) ∧ (τ |= v a1) ∧ (τ |= v a2)
  then (τ |= PRE self a1 a2) ∧
        (τ |= POST self a1 a2 res)
  else τ |= res ≜ invalid)

assumes `all-post`: `∀ σ σ' σ''. ((σ,σ') |= PRE self a1 a2) = ((σ,σ'') |= PRE self a1 a2)`

assumes `cpPRE`: `PRE(self)(a1)(a2) τ = PRE(λ -. self τ)(λ -. a1 τ)(λ -. a2 τ) τ`

assumes `cpPOST: ∀ res. POST(self)(a1)(a2)(res) τ = POST(λ -. self τ)(λ -. a1 τ)(λ -. a2 τ)(λ -. res τ) τ`

sublocale `contract2 < contract-scheme λ(a1,a2) τ. (τ |= v a1) ∧ (τ |= v a2)`
λ(a1,a2) τ. (λ -. a1 τ, λ -. a2 τ)
(λx (a,b). f x a b)
(λx (a,b). PRE x a b)
(λx (a,b). POST x a b)

*<proof>*

context `contract2`

begin

lemma `strict0'[simp] : f invalid X Y = invalid`
〈proof〉

lemma nullstrict0'[simp]: f null X Y = invalid
(proof)

lemma strict1[simp]: f self invalid Y = invalid
(proof)

lemma strict2[simp]: f self X invalid = invalid
(proof)

lemma defined-mono : τ ⊨ v ( f X Y Z ) ⇒ ( τ ⊨ δ X ) ∧ ( τ ⊨ v Y ) ∧ ( τ ⊨ v Z )
( proof )

lemma cp-pre: cp self' ⇒ cp a1' ⇒ cp a2' ⇒ cp (λX. PRE (self' X) (a1' X) (a2' X))
( proof )

lemma cp-post: cp self' = cp a1' = cp a2' = cp res'
= cp (λX. POST (self' X) (a1' X) (a2' X) (res' X))
( proof )

lemma cp0' : f self a1 a2 τ = f (λ -. self τ) (λ -. a1 τ) (λ -. a2 τ) τ
( proof )

lemma cp [simp]: cp self' = cp a1' = cp a2' = cp res'
= cp (λX. f (self' X) (a1' X) (a2' X))
( proof )

theorem unfold :

assumes cp E
and (τ ⊨ δ self) ∧ (τ ⊨ v a1) ∧ (τ ⊨ v a2)
and τ ⊨ PRE self a1 a2
and ∃ res. (τ ⊨ POST self a1 a2 (λ -. res))
and (∧ res. τ ⊨ POST self a1 a2 (λ -. res)) = τ ⊨ E (λ -. res))
shows τ ⊨ E(f self a1 a2)
( proof )

lemma unfold2 :

assumes cp E
and (τ ⊨ δ self) ∧ (τ ⊨ v a1) ∧ (τ ⊨ v a2)
and τ ⊨ PRE self a1 a2
and τ ⊨ POST self a1 a2
and ∧ res. (POST self a1 a2 res) = ((POST' self a1 a2) and (res ≜ (BODY self a1 a2)))
shows (τ ⊨ E(f self a1 a2)) = (τ ⊨ E(BODY self a1 a2))
( proof )

end

locale contract3 =

fixes f :: ('A, 'α0::null) val ⇒
('A, 'α1::null) val ⇒
('A, 'α2::null) val ⇒
('A, 'α3::null) val ⇒
('A, 'res::null) val

fixes PRE

fixes POST

assumes def-scheme: f self a1 a2 a3 ≡
(λ τ. SOME res. let res = λ -. res in
    if (τ |= (δ self)) ∧ (τ |= v a1) ∧ (τ |= v a2) ∧ (τ |= v a3)
    then (τ |= PRE self a1 a2 a3) ∧
          (τ |= POST self a1 a2 a3 res)
    else τ |= res ≜ invalid)

assumes all-post: ∀ σ σ' σ''. ((σ,σ') |= PRE self a1 a2 a3) = ((σ,σ'') |= PRE self a1 a2 a3)

assumes cp<sub>PRE</sub>: PRE (self) (a1) (a2) (a3) τ = PRE (λ -. self τ) (λ -. a1 τ) (λ -. a2 τ) (λ -. a3 τ) τ

assumes cp<sub>POST</sub>: \\n res. POST (self) (a1) (a2) (a3) (res) τ =
POST (λ -. self τ)(λ -. a1 τ)(λ -. a2 τ)(λ -. a3 τ) (λ -. res τ) τ

**sublocale** contract3 < contract-scheme λ(a1,a2,a3) τ. (τ |= v a1) ∧ (τ |= v a2)∧ (τ |= v a3)
λ(a1,a2,a3) τ. (λ -.a1 τ, λ -.a2 τ, λ -.a3 τ)
(λx (a,b,c). f x a b c)
(λx (a,b,c). PRE x a b c)
(λx (a,b,c). POST x a b c)

<proof>

context contract3

begin

lemma strict0'[simp] : f invalid X Y Z = invalid
<proof>

lemma nullstrict0'[simp]: f null X Y Z = invalid
<proof>

lemma strict1[simp]: f self invalid Y Z = invalid
<proof>

lemma strict2[simp]: f self X invalid Z = invalid
<proof>

lemma defined-mono : τ |=v(f W X Y Z) = ⇒ (τ |=δ W) ∧ (τ |=v X) ∧ (τ |=v Y) ∧ (τ |=v Z)
<proof>

lemma cp-pre: cp self' = ⇒ cp a1' = ⇒ cp a2' = ⇒ cp a3'
= ⇒ cp (λX. PRE (self' X) (a1' X) (a2' X) (a3' X) )
<proof>

lemma cp-post: cp self' = ⇒ cp a1' = ⇒ cp a2' = ⇒ cp a3' = ⇒ cp res'
= ⇒ cp (λX. POST (self' X) (a1' X) (a2' X) (a3' X) (res' X))
<proof>

lemma cp0' : f self a1 a2 a3 τ = f (λ -. self τ) (λ -. a1 τ) (λ -. a2 τ) (λ -. a3 τ) τ
<proof>

lemma cp [simp]: cp self' = ⇒ cp a1' = ⇒ cp a2' = ⇒ cp a3' = ⇒ cp res'
= ⇒ cp (λX. f (self' X) (a1' X) (a2' X) (a3' X))
<proof>

theorem unfold :

assumes cp E
and (τ |= δ self) ∧ (τ |= v a1) ∧ (τ |= v a2) ∧ (τ |= v a3)
and τ |= PRE self a1 a2 a3
and ∃ res. (τ |= POST self a1 a2 a3 (λ -. res))
and ($\wedge_{\text{res.}} \tau \models \text{POST self } a1 a2 a3 (\lambda \cdot . \text{ res}) \implies \tau \models E (\lambda \cdot . \text{ res})$)

shows $\tau \models E(f \text{ self } a1 a2 a3)$

(*proof*)

lemma unfold2 :

assumes $\mathrm{cp} E$

and $(\tau \models \delta \ \mathrm{self}) \wedge (\tau \models \upsilon \ a1) \wedge (\tau \models \upsilon \ a2) \wedge (\tau \models \upsilon \ a3)$

and $\tau \models \mathrm{PRE} \ \mathrm{self} \ a1 a2 a3$

and $\tau \models \mathrm{POST}^* \ \mathrm{self} \ a1 a2 a3$

and $\wedge_{\text{res.}} (\text{POST self } a1 a2 a3 \text{ res}) = ((\text{POST}^* \text{ self } a1 a2 a3) \text{ and } (\text{res} \triangleq (\text{BODY self } a1 a2 a3)))$

shows $(\tau \models E(f \text{ self } a1 a2 a3)) = (\tau \models E(\text{BODY self } a1 a2 a3))$

(*proof*)

end

end

theory UML-Tools

imports UML-Logic

begin

lemmas `substs1 = StrongEq-L-subst2-rev`

foundation15 [THEN iffD2, THEN StrongEq-L-subst2-rev]

foundation7' [THEN iffD2, THEN foundation15 [THEN iffD2, THEN StrongEq-L-subst2-rev]]

foundation14 [THEN iffD2, THEN StrongEq-L-subst2-rev]

foundation13 [THEN iffD2, THEN StrongEq-L-subst2-rev]

lemmas `substs2 = StrongEq-L-subst3-rev`

foundation15 [THEN iffD2, THEN StrongEq-L-subst3-rev]

foundation7' [THEN iffD2, THEN foundation15 [THEN iffD2, THEN StrongEq-L-subst3-rev]]

foundation14 [THEN iffD2, THEN StrongEq-L-subst3-rev]

foundation13 [THEN iffD2, THEN StrongEq-L-subst3-rev]

lemmas `substs4 = StrongEq-L-subst4-rev`

foundation15 [THEN iffD2, THEN StrongEq-L-subst4-rev]

foundation7' [THEN iffD2, THEN foundation15 [THEN iffD2, THEN StrongEq-L-subst4-rev]]

foundation14 [THEN iffD2, THEN StrongEq-L-subst4-rev]

foundation13 [THEN iffD2, THEN StrongEq-L-subst4-rev]

lemmas `substs = substs1 substs2 substs4 [THEN iffD2] substs4`

thm `substs`

(*ML*)

lemma `test1 : τ ⊧ A ⇒ τ ⊧ (A and B ≜ B)`

(*proof*)

lemma `test2 : τ ⊧ A ⇒ τ ⊧ (A and B ≜ B)`

(*proof*)
**lemma test3 : τ ⊨ A ⇒ τ ⊨ (A and A)**
* proof *

**lemma test4 : τ ⊨ not A ⇒ τ ⊨ (A and B ≜ false)**
* proof *

**lemma test5 : τ ⊨ (A ≜ null) ⇒ τ ⊨ (B ≜ null) ⇒ ¬ (τ ⊨ (A and B))**
* proof *

**lemma test6 : τ ⊨ not A ⇒ ¬ (τ ⊨ (A and B))**
* proof *

**lemma test7 : ¬ (τ ⊨ (v A)) ⇒ τ ⊨ (not B) ⇒ ¬ (τ ⊨ (A and B))**
* proof *

**lemma X: ¬ (τ ⊨ (invalid and B))**
* proof *

**lemma X': ¬ (τ ⊨ (invalid and B))**
* proof *

**lemma Y: ¬ (τ ⊨ (null and B))**
* proof *

**lemma Z: ¬ (τ ⊨ (false and B))**
* proof *

**lemma Z': (τ ⊨ (true and B)) = (τ ⊨ B)**
* proof *

end

theory UML-Main
imports UML-Contracts UML-Tools

begin
end
# 4. Example: The Employee Analysis Model

**theory**

Analysis-UML

**imports**

.../../../src/UML-Main

**begin**

## 4.1. Introduction

For certain concepts like classes and class-types, only a generic definition for its resulting semantics can be given. Generic means, there is a function outside HOL that “compiles” a concrete, closed-world class diagram into a “theory” of this data model, consisting of a bunch of definitions for classes, accessors, method, casts, and tests for actual types, as well as proofs for the fundamental properties of these operations in this concrete data model.

Such generic function or “compiler” can be implemented in Isabelle on the ML level. This has been done, for a semantics following the open-world assumption, for UML 2.0 in [4, 7]. In this paper, we follow another approach for UML 2.4: we define the concepts of the compilation informally, and present a concrete example which is verified in Isabelle/HOL.

### 4.1.1. Outlining the Example

We are presenting here an “analysis-model” of the (slightly modified) example Figure 7.3, page 20 of the OCL standard [32]. Here, analysis model means that associations were really represented as relation on objects on the state—as is intended by the standard—rather by pointers between objects as is done in our “design model” (see Chapter 5). To be precise, this theory contains the formalization of the data-part covered by the UML class model (see Figure 4.1):

This means that the association (attached to the association class `EmployeeRanking`) with the association ends `boss` and `employees` is implemented by the attribute `boss` and the operation `employees` (to be discussed in the OCL part captured by the subsequent theory).

<figure><img src="image_12.png" /><figcaption>Figure 4.1.: A simple UML class model drawn from Figure 7.3, page 20 of [32].</figcaption></figure>
## 4.2. Example Data-Universe and its Infrastructure

Ideally, the following is generated automatically from a UML class model.

Our data universe consists in the concrete class diagram just of node's, and implicitly of the class object. Each class implies the existence of a class type defined for the corresponding object representations as follows:

datatype typePerson = mkPerson oid
    int option

datatype typeOclAny = mkOclAny oid
    (int option) option

Now, we construct a concrete “universe of OclAny types” by injection into a sum type containing the class types. This type of OclAny will be used as instance for all respective type-variables.

datatype A = inPerson typePerson | inOclAny typeOclAny

Having fixed the object universe, we can introduce type synonyms that exactly correspond to OCL types. Again, we exploit that our representation of OCL is a “shallow embedding” with a one-to-one correspondance of OCL-types to types of the meta-language HOL.

type-synonym Boolean = A Boolean

type-synonym Integer = A Integer

type-synonym Void = A Void

type-synonym OclAny = (A, typeOclAny option option) val

type-synonym Person = (A, typePerson option option) val

type-synonym Set-Integer = (A, int option option) Set

type-synonym Set-Person = (A, typePerson option option) Set

Just a little check:

typ Boolean

To reuse key-elements of the library like referential equality, we have to show that the object universe belongs to the type class “oclany,” i. e., each class type has to provide a function *oid-of* yielding the object id (*oid*) of the object.

instantiation typePerson :: object

begin

definition oid-of-typePerson-def: oid-of x = (case x of mkPerson oid - ⇒ oid)

instance ⟨proof⟩

end

instantiation typeOclAny :: object

begin

definition oid-of-typeOclAny-def: oid-of x = (case x of mkOclAny oid - ⇒ oid)

instance ⟨proof⟩

end

instantiation A :: object

begin

definition oid-of-A-def: oid-of x = (case x of
    inPerson person ⇒ oid-of person
  | inOclAny oclany ⇒ oid-of oclany)

instance ⟨proof⟩

end
## 4.3. Instantiation of the Generic Strict Equality

We instantiate the referential equality on `Person` and `OclAny`

```text
defs(overloaded) StrictRefEqObjectPerson : (x::Person) ÷ y ≡ StrictRefEqObject x y
```

```text
defs(overloaded) StrictRefEqObjectOclAny : (x::OclAny) ÷ y ≡ StrictRefEqObject x y
```

lemmas cps23 =
* cp-StrictRefEqObject[of x::Person y::Person τ,
  simplified StrictRefEqObjectPerson[symmetric]]
* cp-intro(9) [of P::Person ⇒ PersonQ::Person ⇒ Person,
  simplified StrictRefEqObjectPerson[symmetric]]
* StrictRefEqObject-def [of x::Person y::Person,
  simplified StrictRefEqObjectPerson[symmetric]]
* StrictRefEqObject-defargs [of - x::Person y::Person,
  simplified StrictRefEqObjectPerson[symmetric]]
* StrictRefEqObject-strict1 [of x::Person,
  simplified StrictRefEqObjectPerson[symmetric]]
* StrictRefEqObject-strict2 [of x::Person,
  simplified StrictRefEqObjectPerson[symmetric]]

For each Class `C`, we will have a casting operation `.oclAsType(C)`, a test on the actual type `.oclIsTypeOf(C)` as well as its relaxed form `.oclIsKindOf(C)` (corresponding exactly to Java's `instanceof`-operator).

Thus, since we have two class-types in our concrete class hierarchy, we have two operations to declare and to provide two overloading definitions for the two static types.

## 4.4. OclAsType

### 4.4.1. Definition

```text
constst OclAsTypeOclAny :: 'α ⇒ OclAny ((-) .oclAsType'(OclAny'))
```

```text
constst OclAsTypePerson :: 'α ⇒ Person ((-) .oclAsType'(Person'))
```

```text
definition OclAsTypeOclAny-α = (
  λu. ⌜case u of inOclAny a ⇒ a
  | inPerson (mkPerson oid a) ⇒ mkOclAny oid ⌜a⌝)
```

lemma OclAsTypeOclAny-α-some: OclAsTypeOclAny-α x ≠ None
(proof)

```text
defs (overloaded) OclAsTypeOclAny-OclAny:
  (X::OclAny) .oclAsType(OclAny) ≡ X
```

```text
defs (overloaded) OclAsTypeOclAny-Person:
  (X::Person) .oclAsType(OclAny) ≡
  (λτ. case X τ of
    ⊥ ⇒ invalid τ
  | ⌜⊥⌝ ⇒ null τ
  | ⌜mkPerson oid a⌝ ⇒ ⌜mkOclAny oid ⌜a⌝⌝)
```

```text
definition OclAsTypePerson-α =
  (λu. case u of inPerson p ⇒ ⌜p⌝
  | inOclAny (mkOclAny oid ⌜a⌝) ⇒ ⌜mkPerson oid a⌝
  | - ⇒ None)
```
### `defs` (overloaded) `OclAsTypePerson`-`OclAny`:

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

$$ (\lambda\tau. \text{case } X \tau \text{ of} \quad \begin{array}{l} \perp \Rightarrow \text{invalid } \tau \\ | \perp \downarrow \Rightarrow \text{null } \tau \\ | \llcorner mk_{OclAny} \text{ oid } \perp \downarrow \Rightarrow \text{invalid } \tau \quad (* \text{ down-cast exception } *) \\ | \llcorner mk_{OclAny} \text{ oid } a_{\downarrow} \perp \Rightarrow \llcorner mk_{Person} \text{ oid } a_{\downarrow} \end{array} $$

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

$$ (X::Person) .oclAsType(Person) \equiv X \text{ lemmas } [simp] = \begin{array}{l} OclAsType_{OclAny}-OclAny \\ OclAsType_{Person}-Person \end{array} $$

### 4.4.2. Context Passing

lemma `cp-OclAsTypeOclAny`-`Person`-`Person`: `cp P` = `cp(\lambda X. (P (X::Person>::Person) .oclAsType(OclAny)) <proof>`

lemma `cp-OclAsTypeOclAny`-`OclAny`-`OclAny`: `cp P` = `cp(\lambda X. (P (X::OclAny>::OclAny) .oclAsType(OclAny)) <proof>`

lemma `cp-OclAsTypePerson`-`Person`-`Person`: `cp P` = `cp(\lambda X. (P (X::Person>::Person) .oclAsType(Person)) <proof>`

lemma `cp-OclAsTypePerson`-`OclAny`-`OclAny`: `cp P` = `cp(\lambda X. (P (X::OclAny>::OclAny) .oclAsType(Person)) <proof>`

lemma `cp-OclAsTypeOclAny`-`Person`-`OclAny`: `cp P` = `cp(\lambda X. (P (X::Person>::OclAny) .oclAsType(OclAny)) <proof>`

lemma `cp-OclAsTypeOclAny`-`OclAny`-`Person`: `cp P` = `cp(\lambda X. (P (X::OclAny>::Person) .oclAsType(OclAny)) <proof>`

lemma `cp-OclAsTypePerson`-`Person`-`OclAny`: `cp P` = `cp(\lambda X. (P (X::Person>::OclAny) .oclAsType(Person)) <proof>`

lemma `cp-OclAsTypePerson`-`OclAny`-`Person`: `cp P` = `cp(\lambda X. (P (X::OclAny>::Person) .oclAsType(Person)) <proof>`

lemmas `[simp]` =
* `cp-OclAsTypeOclAny`-`Person`-`Person`
* `cp-OclAsTypeOclAny`-`OclAny`-`OclAny`
* `cp-OclAsTypePerson`-`Person`-`Person`
* `cp-OclAsTypePerson`-`OclAny`-`OclAny`

* `cp-OclAsTypeOclAny`-`Person`-`OclAny`
* `cp-OclAsTypeOclAny`-`OclAny`-`Person`
* `cp-OclAsTypePerson`-`Person`-`OclAny`
* `cp-OclAsTypePerson`-`OclAny`-`Person`

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

lemma `OclAsTypeOclAny`-`OclAny`-`strict`: `(invalid::OclAny) .oclAsType(OclAny) = invalid <proof>`

lemma `OclAsTypeOclAny`-`OclAny`-`nullstrict`: `(null::OclAny) .oclAsType(OclAny) = null <proof>`

lemma `OclAsTypeOclAny`-`Person`-`strict` `[simp]`: `(invalid::Person) .oclAsType(OclAny) = invalid <proof>`

lemma `OclAsTypeOclAny`-`Person`-`nullstrict` `[simp]`: `(null::Person) .oclAsType(OclAny) = null <proof>`

lemma `OclAsTypePerson`-`OclAny`-`strict` `[simp]`: `(invalid::OclAny) .oclAsType(Person) = invalid <proof>`

lemma `OclAsTypePerson`-`OclAny`-`nullstrict` `[simp]`: `(null::OclAny) .oclAsType(Person) = null <proof>`

lemma `OclAsTypePerson`-`Person`-`strict`: `(invalid::Person) .oclAsType(Person) = invalid <proof>`
lemma OclAsTypePerson -Person-nullstrict : (null::Person) .oclAsType(Person) = null <proof>

4.5. OclIsTypeOf

4.5.1. Definition

const s OclIsTypeOf OclAny :: 'α ⇒ Boolean ((-).oclIsTypeOf'(OclAny'))

const s OclIsTypeOf Person :: 'α ⇒ Boolean ((-).oclIsTypeOf'(Person'))

def s (overloaded) OclIsTypeOf OclAny -OclAny:

(X::OclAny) .oclIsTypeOf(OclAny) ≡

$$
\begin{align*}
(\lambda \tau. \ case X \ \tau \ \text{of}) \\
\qquad \bot \Rightarrow \text{invalid } \tau \\
\qquad \lfloor \bot \rfloor \Rightarrow \text{true } \tau \ (\ast \text{ invalid } \text{?? } \ast) \\
\qquad \lfloor \bot mk_{OclAny} \ \text{id} \ \bot \rfloor \Rightarrow \text{true } \tau \\
\qquad \lfloor \bot mk_{OclAny} \ \text{id} \ \lfloor \bot \rfloor \Rightarrow \text{false } \tau \)
\end{align*}
$$

lemma OclIsTypeOf OclAny -OclAny' :

(X::OclAny) .oclIsTypeOf(OclAny) =

$$
\begin{align*}
(\lambda \tau. \ \text{if } \tau \models \upsilon \ X \ \text{then} \ (\text{case } X \ \tau \ \text{of}) \\
\phantom{(\lambda \tau. \ \text{if } \tau \models \upsilon \ X \ \text{then} \ (\text{case } } \lfloor \bot \rfloor \Rightarrow \text{true } \tau \ (\ast \text{ invalid } \text{?? } \ast) \\
\phantom{(\lambda \tau. \ \text{if } \tau \models \upsilon \ X \ \text{then} \ (\text{case } } \lfloor \bot mk_{OclAny} \ \text{id} \ \bot \rfloor \Rightarrow \text{true } \tau \\
\phantom{(\lambda \tau. \ \text{if } \tau \models \upsilon \ X \ \text{then} \ (\text{case } } \lfloor \bot mk_{OclAny} \ \text{id} \ \lfloor \bot \rfloor \Rightarrow \text{false } \tau \) \\
\phantom{(\lambda \tau. \ \text{if } \tau \models \upsilon \ X \ \text{then} \ (\text{case } } \text{else invalid } \tau)
\end{align*}
$$

<proof>

interpretation OclIsTypeOf OclAny -OclAny :

profile-mono-schemeV

OclIsTypeOf OclAny :: OclAny ⇒ Boolean

$$
\begin{align*}
\lambda X. (\text{case } X \text{ of}) \\
\phantom{\lambda X. (\text{case } X \text{ of})} \lfloor \text{None}_\llbracket \rfloor \Rightarrow \lfloor \text{True}_\llbracket \rfloor \quad (\ast \text{ invalid } \text{??} \quad \ast) \}
\end{align*}
$$

$$
\lfloor \mu mk_{OclAny} \text{ oid None}_{\llbracket} \Rightarrow \lfloor \text{True}_{\llbracket} \rfloor
$$

$$
\lfloor \mu mk_{OclAny} \text{ oid } \boxed{\phantom{\text{ invalid } \tau}} \Rightarrow \lfloor \text{False}_{\phantom{\text{ invalid } \tau}} \rfloor
$$

<proof>

def s (overloaded) OclIsTypeOf OclAny -Person :

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

$$
\begin{align*}
(\lambda \tau. \ case X \ \tau \ \text{of}) \\
\qquad \bot \Rightarrow \text{invalid } \tau \\
\qquad \lfloor \bot \rfloor \Rightarrow \text{true } \tau \ (\ast \text{ invalid } \text{?? } \ast) \\
\qquad \lfloor \bot - \rfloor \Rightarrow \text{false } \tau)
\end{align*}
$$

def s (overloaded) OclIsTypeOf Person -OclAny :

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

$$
\begin{align*}
(\lambda \tau. \ case X \ \tau \ \text{of}) \\
\qquad \bot \Rightarrow \text{invalid } \tau \\
\qquad \lfloor \bot \rfloor \Rightarrow \text{true } \tau \\
\qquad \lfloor \mu mk_{OclAny} \ \text{id} \ \bot \rfloor \Rightarrow \text{false } \tau \\
\qquad \lfloor \mu mk_{OclAny} \ \text{id} \ \lfloor \bot \rfloor \Rightarrow \text{true } \tau \)
\end{align*}
$$

def s (overloaded) OclIsTypeOf Person -Person :

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

$$
\begin{align*}
(\lambda \tau. \ case X \ \tau \ \text{of}) \\
\qquad \bot \Rightarrow \text{invalid } \tau \\
\qquad |- \Rightarrow \text{true } \tau)
\end{align*}
$$
### 4.5.2. Context Passing

lemma cp-OclIsTypeOfOclAny-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

### 4.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>
### 4.5.4. Up Down Casting

**lemma actualType-larger-staticType:**

**assumes** `isdef: τ |= (δ X)`

**shows** `τ |= (X::Person) .oclIsTypeOf(OclAny) ≜ false`
*< proof *>*

**lemma down-cast-type:**

**assumes** `isOclAny: τ |= (X::OclAny) .oclIsTypeOf(OclAny)`

**and** `non-null: τ |= (δ X)`

**shows** `τ |= (X .oclAsType(Person)) ≜ invalid`
*< proof *>*

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

**assumes** `isOclAny: τ |= (X::OclAny) .oclIsTypeOf(OclAny)`

**and** `non-null: τ |= (δ X)`

**shows** `τ |= not (v (X .oclAsType(Person)))`
*< proof *>*

**lemma up-down-cast:**

**assumes** `isdef: τ |= (δ X)`

**shows** `τ |= ((X::Person) .oclAsType(OclAny) .oclAsType(Person) ≜ X)`
*< proof *>*

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

**shows** `((X::Person) .oclAsType(OclAny) .oclAsType(Person) = X)`
*< proof *>*

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

**assumes** `τ |= v X`

**shows** `τ |= (((X :: Person) .oclAsType(OclAny) .oclAsType(Person)) = X)`
*< proof *>*

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

**assumes** `τ |= v (X :: Person)`

**shows** `τ |= (X .oclIsTypeOf(Person) implies (X .oclAsType(OclAny) .oclAsType(Person)) = X)`
*< proof *>*

## 4.6. OclIsKindOf

### 4.6.1. Definition

**constst** `OclIsKindOf< OclAny > :: 'α ⇒ Boolean ((-).oclIsKindOf'(OclAny))`

**constst** `OclIsKindOf< Person > :: 'α ⇒ Boolean ((-).oclIsKindOf'(Person))`

**def**s (**overloaded**) `OclIsKindOf< OclAny, OclAny >`:

`(X::OclAny) .oclIsKindOf(OclAny) ≡`

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

**def**s (**overloaded**) `OclIsKindOf< OclAny, Person >`:

`(X::Person) .oclIsKindOf(OclAny) ≡`

`(λτ. case X τ of
⊥ ⇒ invalid τ
| - ⇒ true τ)`
### `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 \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}) $$

### 4.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`

### 4.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>

### 4.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>

## 4.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>

### 4.7.1. OclIsTypeOf

lemma OclAny-allInstances-generic-oclIsTypeOfOclAny1:

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-oclIsTypeOfOclAny1:

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

lemma OclAny-allInstances-at-pre-oclIsTypeOfOclAny1:
∃τ. (τ |= (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>

4.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() \rightarrowforAllSet(X|X .ocIsKindOf(Person))) \\ \langle proof \rangle $$

**lemma Person-allInstances-at-pre-ocIsKindOfPerson:**
$$ \tau \models (Person .allInstances@pre() \rightarrowforAllSet(X|X .ocIsKindOf(Person))) \\ \langle proof \rangle $$

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

Should be generated entirely from a class-diagram.

### 4.8.1. Definition (of the association Employee-Boss)

We start with a oid for the association; this oid can be used in presence of association classes to represent the association inside an object, pretty much similar to the Design\_UML, where we stored an oid inside the class as “pointer.”

**definition oidPersonBOSS** :: oid where oidPersonBOSS = 10

From there on, we can already define an empty state which must contain for `oidPersonBOSS` the empty relation (encoded as association list, since there are associations with a Sequence-like structure).

**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 choose2-1** = fst

**definition choose2-2** = snd

**definition List-flatten** = (λl. (foldl ((λacc. (λl. (foldl ((λacc. (λl. (Cons (l) (acc)))) (acc) ((rev (l)))))) (Nil) ((rev (l))))))

**definition deref-assocs2** :: ('A state × 'A state ⇒ 'A state)
⇒ (oid list list ⇒ oid list × oid list)
⇒ oid
⇒ (oid list ⇒ ('A, 'f) val)
⇒ oid
⇒ ('A, 'f::null) val

**where** deref-assocs₂ pre-post to-from assoc-oid f oid =
(λτ. case (assocs (pre-post τ)) assoc-oid of
  ⊑ S ] ⇒ f (List-flatten (map (choose₂-2 ∠ to-from)
  (filter (λ p. List member (choose₂-1 (to-from p)) oid) S)))
  τ
  |- ⇒ invalid τ)

The pre-post-parameter is configured with `fst` or `snd`, the to-from-parameter either with the identity `id` or the following combinator `switch`:

**definition switch₂-1** = (λ[x,y]⇒ (x,y))

**definition switch₂-2** = (λ[x,y]⇒ (y,x))

**definition switch₃-1** = (λ[x,y,z]⇒ (x,y))
definition switch3-2 = (λ[x,y,z]⇒ (x,z))

definition switch3-3 = (λ[x,y,z]⇒ (y,x))

definition switch3-4 = (λ[x,y,z]⇒ (y,z))

definition switch3-5 = (λ[x,y,z]⇒ (z,x))

definition switch3-6 = (λ[x,y,z]⇒ (z,y))

definition deref-oid$_{Person}$ :: (A state × A state ⇒ A state)

⇒ (type$_{Person}$ ⇒ (A, 'c::null)val)

⇒ oid

⇒ (A, 'c::null)val

where deref-oid$_{Person}$ fst-snd f oid = (λτ. case (heap (fst-snd τ)) oid of

in$_{Person}$ obj ] ⇒ f obj τ

| - ⇒ invalid τ)

definition deref-oid$_{OclAny}$ :: (A state × A state ⇒ A state)

⇒ (type$_{OclAny}$ ⇒ (A, 'c::null)val)

⇒ oid

⇒ (A, 'c::null)val

where deref-oid$_{OclAny}$ fst-snd f oid = (λτ. case (heap (fst-snd τ)) oid of

in$_{OclAny}$ obj ] ⇒ f obj τ

| - ⇒ invalid τ)

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

definition select$_{OclAny}$ ANY f = (λ X. case X of

(mk$_{OclAny}$ - ⊥) ⇒ null

| (mk$_{OclAny}$ - [any$_{j}$]) ⇒ f (λx - . x$_{j}$) any)

definition select$_{Person}$ BOSS f = select-object mtSet UML-Set.OclIncluding UML-Set.OclANY (f (λx - . x$_{⊥}$))

definition select$_{Person}$ SALARY f = (λ X. case X of

(mk$_{Person}$ - ⊥) ⇒ null

| (mk$_{Person}$ - [salary$_{j}$]) ⇒ f (λx - . x$_{⊥}$) salary)

definition deref-assocs$_{2}$ BOSS fst-snd f = (λ mk$_{Person}$ oid - ⇒

deref-assocs$_{2}$ fst-snd switch$_{2}$-1 oid$_{Person}$ BOSS f oid)

definition in-pre-state = fst

definition in-post-state = snd

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

definition dot$_{OclAny}$ ANY :: OclAny ⇒ - ((1(-).any) 50)

where (X).any = eval-extract X

(deref-oid$_{OclAny}$ in-post-state

(select$_{OclAny}$ ANY

reconst-basetype))

definition dot$_{Person}$ BOSS :: Person ⇒ Person ((1(-).boss) 50)

where (X).boss = eval-extract X

(deref-oid$_{Person}$ in-post-state

(deref-assocs$_{2}$ BOSS in-post-state

(select$_{Person}$ BOSS
(deref-oid$_{Person}$ in-post-state)))

**definition** `dotPerson SALARY` :: Person ⇒ Integer ((1(-).salary) 50)

where $(X).salary = \text{eval-extract } X$

(deref-oid$_{Person}$ in-post-state

(select$_{Person}$ SALARY

reconst-basetype))

**definition** `dotOclAny ANY-at-pre` :: OclAny ⇒ - ((1(-).any@pre) 50)

where $(X).any@pre = \text{eval-extract } X$

(deref-oid$_{OclAny}$ in-pre-state

(select$_{OclAny}$ ANY

reconst-basetype))

**definition** `dotPerson BOSS-at-pre`:: Person ⇒ Person ((1(-).boss@pre) 50)

where $(X).boss@pre = \text{eval-extract } X$

(deref-oid$_{Person}$ in-pre-state

(deref-assocs$_2$ BOSS in-pre-state

(select$_{Person}$ BOSS

(deref-oid$_{Person}$ in-pre-state))))

**definition** `dotPerson SALARY-at-pre`:: Person ⇒ Integer ((1(-).salary@pre) 50)

where $(X).salary@pre = \text{eval-extract } X$

(deref-oid$_{Person}$ in-pre-state

(select$_{Person}$ SALARY

reconst-basetype))

**lemmas** `dot-accessor` =

`dotOclAny ANY-def`

`dotPerson BOSS-def`

`dotPerson SALARY-def`

`dotOclAny ANY-at-pre-def`

`dotPerson BOSS-at-pre-def`

`dotPerson SALARY-at-pre-def`

### 4.8.2. Context Passing

lemmas `[simp]` = `eval-extract-def`

lemma `cp-dotOclAny ANY` : ((X).any) τ = ((λ-. X τ).any) τ ⟨proof⟩

lemma `cp-dotPerson BOSS` : ((X).boss) τ = ((λ-. X τ).boss) τ ⟨proof⟩

lemma `cp-dotPerson SALARY` : ((X).salary) τ = ((λ-. X τ).salary) τ ⟨proof⟩

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

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

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

lemmas `cp-dotOclAny ANY-I` `[simp, intro]` =

`cp-dotOclAny ANY[THEN allI[THEN allI],`

of λ X -. X λ - τ. τ, THEN cpI1]

lemmas `cp-dotOclAny ANY-at-pre-I` `[simp, intro]` =

`cp-dotOclAny ANY-at-pre[THEN allI[THEN allI],`

of λ X -. X λ - τ. τ, THEN cpI1]

lemmas `cp-dotPerson BOSS-I` `[simp, intro]` =

`cp-dotPerson BOSS[THEN allI[THEN allI],`

of λ X -. X λ - τ. τ, THEN cpI1]
lemmas $\mathit{cp-dot}_{\mathit{Person}}\mathcal{B}OSS$-at-pre-$I$ [simp, intro!]=
$\mathit{cp-dot}_{\mathit{Person}}\mathcal{B}OSS$-at-pre[THEN allI[THEN allI],
of $\lambda X$. $X \lambda$ - $\tau$. $\tau$, THEN $\mathit{cpI1}$]

lemmas $\mathit{cp-dot}_{\mathit{Person}}\mathcal{S}ALARY$-$I$ [simp, intro!]=
$\mathit{cp-dot}_{\mathit{Person}}\mathcal{S}ALARY$[THEN allI[THEN allI],
of $\lambda X$. $X \lambda$ - $\tau$. $\tau$, THEN $\mathit{cpI1}$]

lemmas $\mathit{cp-dot}_{\mathit{Person}}\mathcal{S}ALARY$-at-pre-$I$ [simp, intro!]=
$\mathit{cp-dot}_{\mathit{Person}}\mathcal{S}ALARY$-at-pre[THEN allI[THEN allI],
of $\lambda X$. $X \lambda$ - $\tau$. $\tau$, THEN $\mathit{cpI1}$]

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

lemma $\mathit{dot}_{\mathit{OclAn}y}\mathcal{A}N\mathcal{Y}$-nullstrict [simp]: (null).any = invalid
<proof>

lemma $\mathit{dot}_{\mathit{OclAn}y}\mathcal{A}N\mathcal{Y}$-at-pre-nullstrict [simp] : (null).any@pre = invalid
<proof>

lemma $\mathit{dot}_{\mathit{OclAn}y}\mathcal{A}N\mathcal{Y}$-strict [simp] : (invalid).any = invalid
<proof>

lemma $\mathit{dot}_{\mathit{OclAn}y}\mathcal{A}N\mathcal{Y}$-at-pre-strict [simp] : (invalid).any@pre = invalid
<proof>

lemma $\mathit{dot}_{\mathit{Person}}\mathcal{B}OSS$-nullstrict [simp]: (null).boss = invalid
<proof>

lemma $\mathit{dot}_{\mathit{Person}}\mathcal{B}OSS$-at-pre-nullstrict [simp] : (null).boss@pre = invalid
<proof>

lemma $\mathit{dot}_{\mathit{Person}}\mathcal{B}OSS$-strict [simp] : (invalid).boss = invalid
<proof>

lemma $\mathit{dot}_{\mathit{Person}}\mathcal{B}OSS$-at-pre-strict [simp] : (invalid).boss@pre = invalid
<proof>

lemma $\mathit{dot}_{\mathit{Person}}\mathcal{S}ALARY$-nullstrict [simp]: (null).salary = invalid
<proof>

lemma $\mathit{dot}_{\mathit{Person}}\mathcal{S}ALARY$-at-pre-nullstrict [simp] : (null).salary@pre = invalid
<proof>

lemma $\mathit{dot}_{\mathit{Person}}\mathcal{S}ALARY$-strict [simp] : (invalid).salary = invalid
<proof>

lemma $\mathit{dot}_{\mathit{Person}}\mathcal{S}ALARY$-at-pre-strict [simp] : (invalid).salary@pre = invalid
<proof>

### 4.8.4. Representation in States

lemma $\mathit{dot}_{\mathit{Person}}\mathcal{B}OSS$-def-mono:$\tau$ $\models$ $\delta(X \cdot \mathit{boss})$ $\implies$ $\tau$ $\models$ $\delta(X)$
<proof>

lemma $\mathit{repr-boss}$:

assumes $A : \tau \models \delta(x \cdot \mathit{boss})$

shows is-represented-in-state in-post-state $(x \cdot \mathit{boss})$ Person $\tau$
<proof>

lemma $\mathit{repr-boss}X$:

assumes $A: \tau \models \delta(x \cdot \mathit{boss})$

shows $\tau \models ((\mathit{Person} \cdot \mathit{allInstances}()) \rightarrow \mathit{includes}_{\mathit{Set}}(x \cdot \mathit{boss}))$
<proof>
<figure><img src="image_13.png" /><figcaption>Figure 4.2.: (a) pre-state $\sigma_1$ and (b) post-state $\sigma'_1$.</figcaption></figure>

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

The example we are defining in this section comes from the figure 4.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_

definition person2 ≡ mkPerson oid1 ⌢ 1800_

definition person3 ≡ mkPerson oid2 None

definition person4 ≡ mkPerson oid3 ⌢ 2900_

definition person5 ≡ mkPerson oid4 ⌢ 3500_

definition person6 ≡ mkPerson oid5 ⌢ 2500_

definition person7 ≡ mkOclAny oid6 ⌢ 3200_

definition person8 ≡ mkOclAny oid7 None

definition person9 ≡ mkPerson oid8 ⌢ 0_

$$ \sigma_1 \equiv (\text{heap} = \text{empty}(oid0 \mapsto \text{inPerson}(mkPerson oid0 \lfloor 1000 \rfloor)) $$

$$ (oid1 \mapsto \text{inPerson}(mkPerson oid1 \lfloor 1200 \rfloor)) $$

(*oid2*)

$$ (oid3 \mapsto \text{inPerson}(mkPerson oid3 \lfloor 2600 \rfloor)) $$

$$ (oid4 \mapsto \text{inPerson}(\text{person5})) $$

$$ (oid5 \mapsto \text{inPerson}(mkPerson oid5 \lfloor 2300 \rfloor)) $$

(*oid6*)

(*oid7*)

$$ (oid8 \mapsto \text{inPerson}(\text{person9})) $$

$$ \text{assocs} = \text{empty}(oidPerson BOSS \mapsto [[oid0],[oid1]], [[oid3],[oid4]], [[oid5],[oid3]]) \} $$

definition
$\sigma_1' \equiv (\text{heap} = \text{empty}(\text{oid0} \mapsto \text{inPerson } \text{person1})$
(\text{oid1} \mapsto \text{inPerson } \text{person2})
(\text{oid2} \mapsto \text{inPerson } \text{person3})
(\text{oid3} \mapsto \text{inPerson } \text{person4})
(*\text{oid4}*)
(\text{oid5} \mapsto \text{inPerson } \text{person6})
(\text{oid6} \mapsto \text{inOclAny } \text{person7})
(\text{oid7} \mapsto \text{inOclAny } \text{person8})
(\text{oid8} \mapsto \text{inPerson } \text{person9}),
\text{assocs} = \text{empty}(\text{oidPerson } \text{BOSS} \mapsto [[[\text{oid0}], [\text{oid1}]], [[\text{oid1}], [\text{oid1}]], [[\text{oid5}], [\text{oid6}]], [[\text{oid6}], [\text{oid6}]]]) )

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

lemma basic-τ-wff: WFF($\sigma_1, \sigma_1'$)
<proof>

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

lemma [simp,code-unfold]: dom (heap $\sigma_1$') = {oid0,oid1,oid2,oid3,(*,oid4*)oid5,oid6,oid7,oid8}
<proof> definition $X_{Person1}$ :: Person $\equiv$ $\lambda - .\llap{\llap{\text{person1}}}$

definition $X_{Person2}$ :: Person $\equiv$ $\lambda - .\llap{\llap{\text{person2}}}$

definition $X_{Person3}$ :: Person $\equiv$ $\lambda - .\llap{\llap{\text{person3}}}$

definition $X_{Person4}$ :: Person $\equiv$ $\lambda - .\llap{\llap{\text{person4}}}$

definition $X_{Person5}$ :: Person $\equiv$ $\lambda - .\llap{\llap{\text{person5}}}$

definition $X_{Person6}$ :: Person $\equiv$ $\lambda - .\llap{\llap{\text{person6}}}$

definition $X_{Person7}$ :: OclAny $\equiv$ $\lambda - .\llap{\llap{\text{person7}}}$

definition $X_{Person8}$ :: OclAny $\equiv$ $\lambda - .\llap{\llap{\text{person8}}}$

definition $X_{Person9}$ :: Person $\equiv$ $\lambda - .\llap{\llap{\text{person9}}}$

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

lemma [code-unfold]: ((x::OclAny) .\dagger 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} .\text{salary} \prec 1000)$
\textbf{Assert} $\bigwedge_{spre} . (s_{pre}, \sigma_1') \models (X_{Person1} .\text{salary} \doteq 1300)$
\textbf{Assert} $\bigwedge_{spost} . (\sigma_1, s_{post}) \models (X_{Person1} .\text{salary}@pre \doteq 1000)$
\textbf{Assert} $\bigwedge_{spost} . (\sigma_1, s_{post}) \models (X_{Person1} .\text{salary}@pre \prec 1300)$

lemma $(\sigma_1, \sigma_1') \models (X_{Person1} . \text{oclIsMaintained})$
<proof>

lemma $\bigwedge s_{pre} s_{post}. (s_{pre}, s_{post}) \models ((X_{Person1} . \text{oclAsType}(\text{OclAny}) . \text{oclAsType}(\text{Person})) \doteq X_{Person1})$
〈proof〉

$$
\text{Assert} \quad \forall s_{\text{pre}} s_{\text{post}}. \quad (s_{\text{pre}}, s_{\text{post}}) \models \quad (X_{\text{Person}1} . \text{oclIsTypeOf}(\text{Person}))
$$

$$
\text{Assert} \quad \forall s_{\text{pre}} s_{\text{post}}. \quad (s_{\text{pre}}, s_{\text{post}}) \models \quad \text{not}(X_{\text{Person}1} . \text{oclIsTypeOf}(\text{OclAny}))
$$

$$
\text{Assert} \quad \forall s_{\text{pre}} s_{\text{post}}. \quad (s_{\text{pre}}, s_{\text{post}}) \models \quad (X_{\text{Person}1} . \text{oclIsKindOf}(\text{Person}))
$$

$$
\text{Assert} \quad \forall s_{\text{pre}} s_{\text{post}}. \quad (s_{\text{pre}}, s_{\text{post}}) \models \quad (X_{\text{Person}1} . \text{oclIsKindOf}(\text{OclAny}))
$$

$$
\text{Assert} \quad \forall s_{\text{pre}} s_{\text{post}}. \quad (s_{\text{pre}}, s_{\text{post}}) \models \quad \text{not}(X_{\text{Person}1} . \text{oclAsType}(\text{OclAny}) . \text{oclIsTypeOf}(\text{OclAny}))
$$

$$
\text{Assert} \quad \forall s_{\text{pre}} . \quad (s_{\text{pre}}, \sigma_1') \models \quad (X_{\text{Person}2} . \text{salary} \doteq 1800)
$$

$$
\text{Assert} \quad \forall s_{\text{post}}. \quad (\sigma_1, s_{\text{post}}) \models \quad (X_{\text{Person}2} . \text{salary}@\text{pre} \doteq 1200)
$$

$$
\text{lemma} \quad (\sigma_1, \sigma_1') \models \quad (X_{\text{Person}2} . \text{oclIsMaintained})
$$

〈proof〉

$$
\text{Assert} \quad \forall s_{\text{pre}} . \quad (s_{\text{pre}}, \sigma_1') \models \quad (X_{\text{Person}3} . \text{salary} \doteq \text{null})
$$

$$
\text{Assert} \quad \forall s_{\text{post}}. \quad (\sigma_1, s_{\text{post}}) \models \quad \text{not}(v(X_{\text{Person}3} . \text{salary}@\text{pre}))
$$

$$
\text{lemma} \quad (\sigma_1, \sigma_1') \models \quad (X_{\text{Person}3} . \text{oclIsNew})
$$

〈proof〉

$$
\text{lemma} \quad (\sigma_1, \sigma_1') \models \quad (X_{\text{Person}4} . \text{oclIsMaintained})
$$

〈proof〉

$$
\text{Assert} \quad \forall s_{\text{pre}} . \quad (s_{\text{pre}}, \sigma_1') \models \quad \text{not}(v(X_{\text{Person}5} . \text{salary}))
$$

$$
\text{Assert} \quad \forall s_{\text{post}}. \quad (\sigma_1, s_{\text{post}}) \models \quad (X_{\text{Person}5} . \text{salary}@\text{pre} \doteq 3500)
$$

$$
\text{lemma} \quad (\sigma_1, \sigma_1') \models \quad (X_{\text{Person}5} . \text{oclIsDeleted})
$$

〈proof〉

$$
\text{lemma} \quad (\sigma_1, \sigma_1') \models \quad (X_{\text{Person}6} . \text{oclIsMaintained})
$$

〈proof〉

$$
\text{Assert} \quad \forall s_{\text{pre}} s_{\text{post}}. \quad (s_{\text{pre}}, s_{\text{post}}) \models \quad v(X_{\text{Person}7} . \text{oclAsType}(\text{Person}))
$$

$$
\text{lemma} \quad \forall s_{\text{pre}} s_{\text{post}}. \quad (s_{\text{pre}}, s_{\text{post}}) \models \quad ((X_{\text{Person}7} . \text{oclAsType}(\text{Person}) . \text{oclAsType}(\text{OclAny}) . \text{oclAsType}(\text{Person}))
$$

$$
\doteq (X_{\text{Person}7} . \text{oclAsType}(\text{Person}))
$$

〈proof〉

$$
\text{lemma} \quad (\sigma_1, \sigma_1') \models \quad (X_{\text{Person}7} . \text{oclIsNew})
$$

〈proof〉

$$
\text{Assert} \quad \forall s_{\text{pre}} s_{\text{post}}. \quad (s_{\text{pre}}, s_{\text{post}}) \models \quad (X_{\text{Person}8} \prec\succ X_{\text{Person}7})
$$

$$
\text{Assert} \quad \forall s_{\text{pre}} s_{\text{post}}. \quad (s_{\text{pre}}, s_{\text{post}}) \models \quad \text{not}(v(X_{\text{Person}8} . \text{oclAsType}(\text{Person})))
$$

$$
\text{Assert} \quad \forall s_{\text{pre}} s_{\text{post}}. \quad (s_{\text{pre}}, s_{\text{post}}) \models \quad (X_{\text{Person}8} . \text{oclIsTypeOf}(\text{OclAny}))
$$

$$
\text{Assert} \quad \forall s_{\text{pre}} s_{\text{post}}. \quad (s_{\text{pre}}, s_{\text{post}}) \models \quad \text{not}(X_{\text{Person}8} . \text{oclIsTypeOf}(\text{Person}))
$$

$$
\text{Assert} \quad \forall s_{\text{pre}} s_{\text{post}}. \quad (s_{\text{pre}}, s_{\text{post}}) \models \quad \text{not}(X_{\text{Person}8} . \text{oclIsKindOf}(\text{Person}))
$$

$$
\text{Assert} \quad \forall s_{\text{pre}} s_{\text{post}}. \quad (s_{\text{pre}}, s_{\text{post}}) \models \quad (X_{\text{Person}8} . \text{oclIsKindOf}(\text{OclAny}))
$$

$$
\text{lemma } \sigma\text{-modifiedonly:} \quad (\sigma_1, \sigma_1') \models \quad (\text{Set}\{ X_{\text{Person}1} . \text{oclAsType}(\text{OclAny}) \\
, X_{\text{Person}2} . \text{oclAsType}(\text{OclAny}) \\
(*, X_{\text{Person}3} . \text{oclAsType}(\text{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 (σ₁,σ₁') ::= ((XPerson9 @post (λx. ⌜OclAsTypePerson-Å x⌝)) ≜ XPerson9)
<proof>

lemma (σ₁,σ₁') ::= (((XPerson9 .oclAsType(OclAny)) @pre (λx. ⌜OclAsTypeOclAny-Å x⌝)) ≜
((XPerson9 .oclAsType(OclAny)) @post (λx. ⌜OclAsTypeOclAny-Å x⌝)))

<proof>

lemma perm-σ₁' : σ₁' = () heap = empty
 oid8 ↦ inPerson person9
 (oid7 ↦ inOclAny person8)
 (oid6 ↦ inOclAny person7)
 (oid5 ↦ inPerson person6)
 (*oid4*)
 (oid3 ↦ inPerson person4)
 (oid2 ↦ inPerson person3)
 (oid1 ↦ inPerson person2)
 (oid0 ↦ inPerson person1)
 , assocs = assocs σ₁' )

<proof>

declare const-ss [simp]

lemma Xsigma1.
(σ₁,σ₁') ::= (Person .allInstances() .d Set{ XPerson1, XPerson2, XPerson3, XPerson4(*, XPerson5*),
                 XPerson6,
                 XPerson7 .oclAsType(Person)(*, XPerson8*), XPerson9 })

<proof>

lemma Xsigma1.
(σ₁,σ₁') ::= (OclAny .allInstances() .d Set{ XPerson1 .oclAsType(OclAny), XPerson2 .oclAsType(OclAny),
XPerson3 .oclAsType(OclAny), XPerson4 .oclAsType(OclAny)
(*, XPerson5*), XPerson6 .oclAsType(OclAny),
XPerson7, XPerson8, XPerson9 .oclAsType(OclAny) })

<proof>

end

theory
Analysis-OCL

imports
Analysis-UML

begin
4.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) ≡
(self .boss <> null implies (self .salary ≤<sub>int</sub> ((self .boss) .salary))))

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

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

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

where
Person-label<sub>globalinv</sub> ≡ (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 τ |= δ (X .boss) ⇒ τ |= Person .allInstances() -> includes<Set>(X .boss) ∧
τ |= Person .allInstances() -> includes<Set>(X)
proof

lemma REC-pre : τ |= Person-label<sub>globalinv</sub>
⇒ τ |= Person .allInstances() -> includes<Set>(X) (* X represented object in state *)
⇒ ∃ REC. τ |= REC(X) ≜ (Person-label<sub>inv</sub> (X) and (X .boss <> null implies REC(X .boss)))
proof

This allows to state a predicate:

axiomatization inv<sub>Person-label</sub> :: Person ⇒ Boolean

where inv<sub>Person-label-def</sub>:

(τ |= Person .allInstances() -> includes<Set>(self)) ⇒
(τ |= (inv<sub>Person-label</sub>(self) ≜ (self .boss <> null implies
(self .salary ≤<sub>int</sub> ((self .boss) .salary)) and
inv<sub>Person-label</sub>(self .boss)))))

axiomatization inv<sub>Person-labelATpre</sub> :: Person ⇒ Boolean

where inv<sub>Person-labelATpre-def</sub>:

(τ |= Person .allInstances@pre() -> includes<Set>(self)) ⇒
(τ |= (inv<sub>Person-labelATpre</sub>(self) ≜ (self .boss@pre <> null implies
(self .salary@pre ≤<sub>int</sub> ((self .boss@pre) .salary@pre)) and
inv<sub>Person-labelATpre</sub>(self .boss@pre)))))

lemma inv-1 :

(τ |= Person .allInstances() -> includes<Set>(self)) ⇒
(τ |= inv<sub>Person-label</sub>(self) = ((τ |= (self .boss ≜ null)) ∨
(τ |= (self .boss <> null) ∧
τ |= ((self .salary) ≤<sub>int</sub> (self .boss .salary)) ∧
τ |= (inv<sub>Person-label</sub>(self .boss)))))
proof
**lemma inv-2 :**

$$
\begin{align*}
(\tau \models \mathit{Person}.\mathit{allInstances}@\mathit{pre}() \rightarrow \mathit{includes}_{\mathit{Set}}(\mathit{self})) \implies \\
(\tau \models \mathit{inv}_{\mathit{Person}-\mathit{labelATpre}}(\mathit{self})) &= ((\tau \models (\mathit{self}.\mathit{boss}@\mathit{pre} \doteq \mathit{null})) \lor \\
&\qquad (\tau \models (\mathit{self}.\mathit{boss}@\mathit{pre} \prec \mathit{null}) \land \\
&\qquad (\tau \models (\mathit{self}.\mathit{boss}@\mathit{pre}.\mathit{salary}@\mathit{pre} \leq_{\mathit{int}} \mathit{self}.\mathit{salary}@\mathit{pre})) \land \\
&\qquad (\tau \models (\mathit{inv}_{\mathit{Person}-\mathit{labelATpre}}(\mathit{self}.\mathit{boss}@\mathit{pre}))))))
\end{align*}
$$

`(proof)`

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 \text{ self})) &\implies ((\tau \models (\text{self boss }\doteq\text{ null})) \lor \\
&\qquad (\tau \models (\text{self boss }\prec\text{ null}) \land (\tau \models (\text{self boss salary }\leq_{\text{int}} \text{ self salary}))) \land \\
&\qquad ((\text{inv(self boss)}\tau))) \\
&\implies (\text{inv self } \tau)
\end{align*}
$$

4.11. OCL Part: The Contract of a Recursive Query

The original specification of a recursive query :

context Person::contents():Set Integer
pre: true
post: result = if self.boss = null
then Set{i}
else self.boss contents->including(i)
endif

For the case of recursive queries, we use at present just axiomatizations:

axiomatization contents :: Person ⇒ Set-Integer ((1 (-).contents'( ')) 50)

where contents-def :

(self .contents()) = (λ τ. SOME res. let res = λ -. res in
if τ = (δ self)
then ((τ = true ) ∧
(τ = res = if (self .boss = null)
then (Set{self .salary})
else (self .boss .contents()
->including<Set>(self .salary))
endif))
else τ = res = invalid)

and cp0-contents:(X .contents()) τ = ((λ-. X τ) .contents()) τ

interpretation contents : contract0 contents λ self. true
λ self res. res = if (self .boss = null)
then (Set{self .salary})
else (self .boss .contents()
->including<Set>(self .salary))
endif

`(proof)`

Specializing [[cp E; τ = δ self; τ = true; τ = POST' self; ∧ res. (res = if self.boss = null then Set{self.salary} else self.boss contents() -> includingSet(self.salary) endif) = (POST' self and (res = BODY self))]] = (τ = E (self contents())) = (τ = E (BODY self)), one gets the following more
practical rewrite rule that is amenable to symbolic evaluation:

**theorem unfold-contents :**

assumes cp E
and $\tau \models \delta \text{ self}$

shows $\begin{align*}
(\tau \models E (\mathit{self} . \mathit{contents})) &= \\
&\quad (\tau \models E (\mathit{if self boss} \doteq \mathit{null} \\
&\qquad \quad \mathit{then Set}\{\mathit{self salary}\} \\
&\qquad \quad \mathit{else self boss contents} \rightarrow \mathit{includingSet} (\mathit{self salary} \mathit{pre})))
\end{align*}$

```
(proof)
```

Since we have only one interpretation function, we need the corresponding operation on the pre-state:

```
consts contentsATpre :: Person $\Rightarrow$ Set-Integer $((1(-).contents@pre'(')) 50)$
```

axiomatization where `contentsATpre-def`:

```
(self).contents@pre() = (\lambda \tau.
  SOME res. let res = \lambda -. res in
  if \tau \models (\delta self)
  then ((\tau \models true) $\wedge$ (* pre *)
        (\tau \models (res $\triangleq$ if (self).boss@pre $\doteq$ null (* post *)
                                 then Set{(self).salary@pre}
                                 else (self).boss@pre . contents@pre()
                                       $\rightarrow$ includingSet (self . salary@pre)
                                                           $endif)))
  else \tau \models res $\triangleq$ invalid)
```

and `cp0-contents-at-pre:(X . contents@pre()) \tau = ((\lambda-. X \tau) . contents@pre()) \tau`

interpretation `contentsATpre : contract0 contentsATpre \lambda self. true`

$$ \lambda self. res. res \triangleq \begin{cases} \text{if } (\mathit{self boss@pre} \doteq \mathit{null}) \\ \text{then } (\mathit{Set}\{\mathit{self salary@pre}\}) \\ \text{else } (\mathit{self boss@pre}.\mathit{contents@pre}()) \\ \hfill \rightarrow \mathit{includingSet}(\mathit{self salary@pre}) \end{cases} $$

$\mathit{endif}$

```
(proof)
```

Again, we derive via `contents.unfold2` a Knaster-Tarski like Fixpoint rule that is amenable to symbolic evaluation:

theorem `unfold-contentsATpre`:

assumes `cp E`

and $\tau \models \delta \text{ self}$

shows $\begin{align*}
(\tau \models E (\mathit{self} . \mathit{contents@pre})) &= \\
&\quad (\tau \models E (\mathit{if self boss@pre} \doteq \mathit{null} \\
&\qquad \quad \mathit{then Set}\{\mathit{self salary@pre}\} \\
&\qquad \quad \mathit{else self boss@pre . contents@pre()} \rightarrow \mathit{includingSet} (\mathit{self salary@pre}) \} \mathit{endif}))
\end{align*}$

```
(proof)
```

Note that these `@pre` variants on methods are only available on queries, i. e., operations without side-effect.

## 4.12. OCL Part: The Contract of a User-defined Method

The example specification in high-level OCL input syntax reads as follows:

```
context Person::insert(x:Integer)
pre: true
post: contents():Set Integer
contents() = contents@pre()->including(x)
```

This boils down to:

```
definition insert :: Person $\Rightarrow$ Integer $\Rightarrow$ Void $((1(-).insert'(-')) 50)$
```
where $\mathit{self.insert}(x) \equiv$
(λ τ. SOME res. let res = λ -. res in
if (τ |> (δ self)) ∧ (τ |> v x)
then (τ |> true ∧
(τ |> ((self).contents() ≜ (self).contents@pre() -> including$_{Set}$(x))))
else τ |> res ≜ invalid)

The semantic consequences of this definition were computed inside this locale interpretation:

interpretation insert : contract1 insert λ self x. true
λ self x res. ((self .contents()) ≜
(self .contents@pre() -> including$_{Set}$(x)))
<proof>

The result of this locale interpretation for our *Analysis-OCL.insert* contract is the following set of properties, which serves as basis for automated deduction on them:

<table><caption>Table 4.1.: Semantic properties resulting from a user-defined operation contract.</caption><thead><tr><th>Name</th><th>Theorem</th></tr></thead><tbody><tr><td>insert.strict0</td><td>(invalid.insert(X)) = invalid</td></tr><tr><td>insert nullstrict0</td><td>(null.insert(X)) = invalid</td></tr><tr><td>insert.strict1</td><td>(self.insert(invalid)) = invalid</td></tr><tr><td>insert.cp<sub>PRE</sub></td><td>true τ = true τ</td></tr><tr><td>insert.cp<sub>POST</sub></td><td>(self contents() ≜ self contents@pre() -&gt; including<sub>Set</sub> (a1.0)) τ = (λ-. self τ. contents() ≜ λ-. self τ. contents@pre() -&gt; including<sub>Set</sub> (λ-. a1.0 τ)) τ</td></tr><tr><td>insert.cp-pre</td><td>[[cp self'; cp a1']] = cp (λX. true)</td></tr><tr><td>insert.cp-post</td><td>[[cp self'; cp a1'; cp res]] = cp (λX. self' X. contents() ≜ self' X. contents@pre() -&gt; including<sub>Set</sub> (a1' X))</td></tr><tr><td>insert.cp</td><td>[[cp self'; cp a1'; cp res]] = cp (λX. self' X. insert(a1' X))</td></tr><tr><td>insert.cp0</td><td>(self.insert(a1.0)) τ = (λ-. self τ. insert(λ-. a1.0 τ)) τ</td></tr><tr><td>insert.def-scheme</td><td>self.insert(a1.0) ≡ λτ. SOME res. let res = λ-. res in if τ |> δ self ∧ τ |> v a1.0 then τ |> true ∧ τ |> self. contents() ≜ self. contents@pre() -&gt; including<sub>Set</sub> (a1.0) else τ |> res ≜ invalid</td></tr><tr><td>insert.unfold</td><td>[[cp E; τ |> δ self ∧ τ |> v a1.0; τ |> true; ∃ res. τ |> self. contents() ≜ self. contents@pre() -&gt; including<sub>Set</sub> (a1.0); ∧ res. τ |> self. contents() ≜ self. contents@pre() -&gt; including<sub>Set</sub> (a1.0) = τ |> E (λ-. res)] = τ |> E (self. insert(a1.0))</td></tr><tr><td>insert.unfold2</td><td>[[cp E; τ |> δ self ∧ τ |> v a1.0; τ |> true; τ |> POST' self a1.0; ∧ res. (self. contents() ≜ self. contents@pre() -&gt; including<sub>Set</sub> (a1.0)) = (POST' self a1.0 and (res ≜ BODY self a1.0))]] = (τ |> E (self. insert(a1.0))) = (τ |> E (BODY self a1.0))</td></tr></tbody></table>

end
# 5. Example: The Employee Design Model

**theory**

Design-UML

**imports**

../../../src/UML-Main

**begin**

## 5.1. Introduction

For certain concepts like classes and class-types, only a generic definition for its resulting semantics can be given. Generic means, there is a function outside HOL that “compiles” a concrete, closed-world class diagram into a “theory” of this data model, consisting of a bunch of definitions for classes, accessors, method, casts, and tests for actual types, as well as proofs for the fundamental properties of these operations in this concrete data model.

Such generic function or “compiler” can be implemented in Isabelle on the ML level. This has been done, for a semantics following the open-world assumption, for UML 2.0 in [4, 7]. In this paper, we follow another approach for UML 2.4: we define the concepts of the compilation informally, and present a concrete example which is verified in Isabelle/HOL.

### 5.1.1. Outlining the Example

We are presenting here a “design-model” of the (slightly modified) example Figure 7.3, page 20 of the OCL standard [32]. To be precise, this theory contains the formalization of the data-part covered by the UML class model (see Figure 5.1):

This means that the association (attached to the association class `EmployeeRanking`) with the association ends `boss` and `employees` is implemented by the attribute `boss` and the operation `employees` (to be discussed in the OCL part captured by the subsequent theory).

## 5.2. Example Data-Universe and its Infrastructure

Ideally, the following is generated automatically from a UML class model.

<figure><img src="image_14.png" /><figcaption>Figure 5.1.: A simple UML class model drawn from Figure 7.3, page 20 of [32].</figcaption></figure>
Our data universe consists in the concrete class diagram just of node's, and implicitly of the class object. Each class implies the existence of a class type defined for the corresponding object representations as follows:

datatype typePerson = mkPerson oid
    int option
    oid option

datatype typeOclAny = mkOclAny oid
    (int option × oid option) option

Now, we construct a concrete “universe of OclAny types” by injection into a sum type containing the class types. This type of OclAny will be used as instance for all respective type-variables.

datatype A = inPerson typePerson | inOclAny typeOclAny

Having fixed the object universe, we can introduce type synonyms that exactly correspond to OCL types. Again, we exploit that our representation of OCL is a “shallow embedding” with a one-to-one correspondance of OCL-types to types of the meta-language HOL.

type-synonym Boolean = A Boolean

type-synonym Integer = A Integer

type-synonym Void = A Void

type-synonym OclAny = (A, typeOclAny option option) val

type-synonym Person = (A, typePerson option option) val

type-synonym Set-Integer = (A, int option option) Set

type-synonym Set-Person = (A, typePerson option option) Set

Just a little check:

typ Boolean

To reuse key-elements of the library like referential equality, we have to show that the object universe belongs to the type class "oclany," i. e., each class type has to provide a function *oid-of* yielding the object id (oid) of the object.

instantiation typePerson :: object

begin

definition oid-of-typePerson-def: oid-of x = (case x of mkPerson oid - - ⇒ oid)

instance ⟨proof⟩

end

instantiation typeOclAny :: object

begin

definition oid-of-typeOclAny-def: oid-of x = (case x of mkOclAny oid - ⇒ oid)

instance ⟨proof⟩

end

instantiation A :: object

begin

definition oid-of-A-def: oid-of x = (case x of

inPerson person ⇒ oid-of person

| inOclAny oclany ⇒ oid-of oclany)

instance ⟨proof⟩

end

## 5.3. Instantiation of the Generic Strict Equality

We instantiate the referential equality on *Person* and *OclAny*
defsls(overloaded) StrictRefEqObject-Person : (x::Person) ÷ y ≡ StrictRefEqObject x y

defsls(overloaded) StrictRefEqObject-OclAny : (x::OclAny) ÷ y ≡ StrictRefEqObject x y

lemmas cps23 =

cp-StrictRefEqObject[of x::Person y::Person τ,
 simplified StrictRefEqObject-Person[symmetric]]

cp-intro(9) [of P::Person ⇒ PersonQ::Person ⇒ Person,
 simplified StrictRefEqObject-Person[symmetric] ]

StrictRefEqObject-def [of x::Person y::Person,
 simplified StrictRefEqObject-Person[symmetric]]

StrictRefEqObject-defargs [of - x::Person y::Person,
 simplified StrictRefEqObject-Person[symmetric]]

StrictRefEqObject-strict1

[of x::Person,
 simplified StrictRefEqObject-Person[symmetric]]

StrictRefEqObject-strict2

[of x::Person,
 simplified StrictRefEqObject-Person[symmetric]]

For each Class C, we will have a casting operation .oclAsType(C) , a test on the actual type .oclIsTypeOf(C) as well as its relaxed form .oclIsKindOf(C) (corresponding exactly to Java’s instanceof -operator.

Thus, since we have two class-types in our concrete class hierarchy, we have two operations to declare
and to provide two overloading definitions for the two static types.

5.4. OclAsType

5.4.1. Definition

constsls OclAsTypeOclAny :: 'α ⇒ OclAny ((-) .oclAsType'(OclAny'))

constsls OclAsTypePerson :: 'α ⇒ Person ((-) .oclAsType'(Person'))

definition OclAsTypeOclAny-Α = (λu. ⊢ case u of inOclAny a ⇒ a
| inPerson (mkPerson oid a b) ⇒ mkOclAny oid ⊢(a,b) ⊢)

lemma OclAsTypeOclAny-Α-some: OclAsTypeOclAny-Α x ≠ None
(proof)

defsls (overloaded) OclAsTypeOclAny-OclAny:
(X::OclAny) .oclAsType(OclAny) ≡ X

defsls (overloaded) OclAsTypeOclAny-Person:
(X::Person) .oclAsType(OclAny) ≡

(λτ. case X τ of
   ⊥ ⇒ invalid τ
  | ⊢⊥ ⇒ null τ
  | ⊢mkPerson oid a b ⊢ ⇒ ⊢ (mkOclAny oid ⊢(a,b)) ⊢])

definition OclAsTypePerson-Α =
(λu. case u of inPerson p ⇒ p
| inOclAny (mkOclAny oid ⊢(a,b)) ⇒ mkPerson oid a b
| - ⇒ None)

defsls (overloaded) OclAsTypePerson-OclAny:
(X::OclAny) .oclAsType(Person) ≡

(λτ. case X τ of
<figure><img src="image_15.png" /></figure>

```h
    def s (x : invalid τ)
    | ⊥ : null τ
    | mkOclAny : id ⊥ ⊥
    | mkOclAny : id (a,b) ⊥
```

### 5.4.2. Context Passing

lemma cp-OclAsTypeOclAny-Person-Person : cp P =⇒ cp(λX. (P (X::Person>::Person) .oclAsType(OclAny)) <proof>

lemma cp-OclAsTypeOclAny-OclAny-OclAny : cp P =⇒ cp(λX. (P (X::OclAny>::OclAny) .oclAsType(OclAny)) <proof>

lemma cp-OclAsTypePerson-Person-Person : cp P =⇒ cp(λX. (P (X::Person>::Person) .oclAsType(Person)) <proof>

lemma cp-OclAsTypePerson-OclAny-OclAny : cp P =⇒ cp(λX. (P (X::OclAny>::OclAny) .oclAsType(Person)) <proof>

lemma cp-OclAsTypeOclAny-Person-OclAny : cp P =⇒ cp(λX. (P (X::Person>::OclAny) .oclAsType(OclAny)) <proof>

lemma cp-OclAsTypeOclAny-OclAny-Person : cp P =⇒ cp(λX. (P (X::OclAny>::Person) .oclAsType(OclAny)) <proof>

lemma cp-OclAsTypePerson-Person-OclAny : cp P =⇒ cp(λX. (P (X::Person>::OclAny) .oclAsType(Person)) <proof>

lemma cp-OclAsTypePerson-OclAny-Person : cp P =⇒ cp(λX. (P (X::OclAny>::Person) .oclAsType(Person)) <proof>

lemmas [simp] =
  cp-OclAsTypeOclAny-Person-Person
  cp-OclAsTypeOclAny-OclAny-OclAny
  cp-OclAsTypePerson-Person-Person
  cp-OclAsTypePerson-OclAny-OclAny

cp-OclAsTypeOclAny-Person-OclAny
  cp-OclAsTypeOclAny-OclAny-Person
  cp-OclAsTypePerson-Person-OclAny
  cp-OclAsTypePerson-OclAny-Person

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

lemma OclAsTypeOclAny-OclAny-strict : (invalid::OclAny) .oclAsType(OclAny) = invalid <proof>

lemma OclAsTypeOclAny-OclAny-nullstrict : (null::OclAny) .oclAsType(OclAny) = null <proof>

lemma OclAsTypeOclAny-Person-strict[simp] : (invalid::Person) .oclAsType(OclAny) = invalid <proof>

lemma OclAsTypeOclAny-Person-nullstrict[simp] : (null::Person) .oclAsType(OclAny) = null <proof>

lemma OclAsTypePerson-OclAny-strict[simp] : (invalid::OclAny) .oclAsType(Person) = invalid <proof>

lemma OclAsTypePerson-OclAny-nullstrict[simp] : (null::OclAny) .oclAsType(Person) = null <proof>

lemma OclAsTypePerson-Person-strict : (invalid::Person) .oclAsType(Person) = invalid <proof>

lemma OclAsTypePerson-Person-nullstrict : (null::Person) .oclAsType(Person) = null <proof>