Here is an informal outline of the theory.

Abstract

The theory is a formalization of the OCL type system, its abstract syntax and expression typing rules [1]. The theory does not define a concrete syntax and a semantics. In contrast to Featherweight OCL [2], it is based on a deep embedding approach. The type system is defined from scratch, it is not based on the Isabelle HOL type system.

The Safe OCL distincts nullable and null-free types, errorable and error-free types. Also the theory gives a formal definition of safe navigation operations [3]. The Safe OCL typing rules are much stricter than rules given in the OCL specification. It allows one to catch more errors on a type checking phase.

The type theory presented is four-layered: classes, ordinary types, nullable types, errorable types. We introduce the following new types: error-free null-free types (τ[1]), error-free nullable types (τ[?]), errorable null-free types (τ[1!]), errorable nullable types (τ[?!]). Also we define formaly the Map type, which is absent in the current OCL specification. We define OclAny as a supertype of all other types (basic types, collections, tuples). This type allows us to define a total supremum function, so types form an upper semilattice. It allows us to define rich expression typing rules in an elegant manner.

The theory defines expression normalization rules for implicit types, safe navigation operations, navigation short-hands, and closure body.

The Preliminaries Chapter of the theory defines a number of helper lemmas for transitive closures and tuples. It defines also a generic object model independent from OCL. It allows one to use the theory as a reference for formalization of analogous languages.

[1] Object Management Group, "Object Constraint Language (OCL). Version 2.4", Feb. 2014. http://www.omg.org/spec/OCL/2.4/.

[2] A. D. Brucker, F. Tuong, and B. Wolff, "Featherweight OCL: A proposal for a machine-checked formal semantics for OCL 2.5", Archive of Formal Proofs, Jan. 2014. http://isa-afp.org/entries/Featherweight_OCL.html, Formal proof development.

[3] E. D. Willink, "Safe navigation in OCL" in Proceedings of the 15th International Workshop on OCL and Textual Modeling co-located with 18th International Conference on Model Driven Engineering Languages and Systems (MoDELS 2015), Ottawa, Canada, September 28, 2015. (A. D. Brucker, M. Egea, M. Gogolla, and F. Tuong, eds.), vol. 1512 of CEUR Workshop Proceedings, pp. 81-88, CEUR-WS.org, 2015.

Types

Definition

Ordinary and nullable types defined as mutually recursive algebraic datatypes. All of the primitive types, tuple types, collection types, map types can be either nullable or null-free (non-nullable).

Types are parameterized over classes. A type paramater 'a can be replaced by a datatype representing some classes.

datatype 'a type =
  OclAny
| OclVoid

| Boolean
| Real
| Integer
| UnlimitedNatural
| String

| Enum "'a enum_type"
| ObjectType 'a ("⟨_⟩𝒯")
| Tuple "telem ⇀f 'a typeN"

| Collection "'a typeN"
| Set "'a typeN"
| OrderedSet "'a typeN"
| Bag "'a typeN"
| Sequence "'a typeN"

| Map "'a typeN" "'a typeN"

and 'a typeN =
  Required "'a type" ("_[1]")
| Optional "'a type" ("_[?]")

Errorable types are defined on the base of nullable and null-free types. Tuple, collection and map types can have elements only with error-free types.

datatype 'a errorable = ErrorFree 'a | Errorable 'a

type_synonym 'a typeNE = "'a typeN errorable"

Subtype Relation

lemma type_less_left_simps:
  "OclAny < σ = False"
  "OclVoid < σ = (σ ≠ OclVoid)"

  "Boolean < σ = (σ = OclAny)"
  "Real < σ = (σ = OclAny)"
  "Integer < σ = (σ = OclAny ∨ σ = Real)"
  "UnlimitedNatural < σ = (σ = OclAny)"
  "String < σ = (σ = OclAny)"

  "Enum ℰ < σ = (σ = OclAny)"
  "ObjectType 𝒞 < σ = (∃𝒟.
      σ = OclAny ∨
      σ = ObjectType 𝒟 ∧ 𝒞 < 𝒟)"
  "Tuple π < σ = (∃ξ.
      σ = OclAny ∨
      σ = Tuple ξ ∧ strict_subtuple (≤) π ξ)"

  "Collection τ < σ = (∃φ.
      σ = OclAny ∨
      σ = Collection φ ∧ τ < φ)"
  "Set τ < σ = (∃φ.
      σ = OclAny ∨
      σ = Collection φ ∧ τ ≤ φ ∨
      σ = Set φ ∧ τ < φ)"
  "OrderedSet τ < σ = (∃φ.
      σ = OclAny ∨
      σ = Collection φ ∧ τ ≤ φ ∨
      σ = OrderedSet φ ∧ τ < φ)"
  "Bag τ < σ = (∃φ.
      σ = OclAny ∨
      σ = Collection φ ∧ τ ≤ φ ∨
      σ = Bag φ ∧ τ < φ)"
  "Sequence τ < σ = (∃φ.
      σ = OclAny ∨
      σ = Collection φ ∧ τ ≤ φ ∨
      σ = Sequence φ ∧ τ < φ)"

  "Map τ φ < σ = (∃ρ υ.
      σ = OclAny ∨
      σ = Map ρ υ ∧ τ = ρ ∧ φ < υ ∨
      σ = Map ρ υ ∧ τ < ρ ∧ φ = υ ∨
      σ = Map ρ υ ∧ τ < ρ ∧ φ < υ)"

lemma type_less_right_simps:
  "τ < OclAny = (τ ≠ OclAny)"
  "τ < OclVoid = False"

  "τ < Boolean = (τ = OclVoid)"
  "τ < Real = (τ = Integer ∨ τ = OclVoid)"
  "τ < Integer = (τ = OclVoid)"
  "τ < UnlimitedNatural = (τ = OclVoid)"
  "τ < String = (τ = OclVoid)"

  "τ < Enum ℰ = (τ = OclVoid)"
  "τ < ObjectType 𝒟 = (∃𝒞.
      τ = ObjectType 𝒞 ∧ 𝒞 < 𝒟 ∨
      τ = OclVoid)"
  "τ < Tuple ξ = (∃π.
      τ = Tuple π ∧ strict_subtuple (≤) π ξ ∨
      τ = OclVoid)"

  "τ < Collection σ = (∃φ.
      τ = Collection φ ∧ φ < σ ∨
      τ = Set φ ∧ φ ≤ σ ∨
      τ = OrderedSet φ ∧ φ ≤ σ ∨
      τ = Bag φ ∧ φ ≤ σ ∨
      τ = Sequence φ ∧ φ ≤ σ ∨
      τ = OclVoid)"
  "τ < Set σ = (∃φ.
      τ = Set φ ∧ φ < σ ∨
      τ = OclVoid)"
  "τ < OrderedSet σ = (∃φ.
      τ = OrderedSet φ ∧ φ < σ ∨
      τ = OclVoid)"
  "τ < Bag σ = (∃φ.
      τ = Bag φ ∧ φ < σ ∨
      τ = OclVoid)"
  "τ < Sequence σ = (∃φ.
      τ = Sequence φ ∧ φ < σ ∨
      τ = OclVoid)"

  "τ < Map ρ υ = (∃φ σ.
      τ = Map φ σ ∧ φ = ρ ∧ σ < υ ∨
      τ = Map φ σ ∧ φ < ρ ∧ σ = υ ∨
      τ = Map φ σ ∧ φ < ρ ∧ σ < υ ∨
      τ = OclVoid)"

lemma typeN_less_left_simps:
  "Required ρ < σ = (∃υ.
      σ = Required υ ∧ ρ < υ ∨
      σ = Optional υ ∧ ρ ≤ υ)"
  "Optional ρ < σ = (∃υ.
      σ = Optional υ ∧ ρ < υ)"

lemma typeN_less_right_simps:
  "τ < Required υ = (∃ρ.
      τ = Required ρ ∧ ρ < υ)"
  "τ < Optional υ = (∃ρ.
      τ = Required ρ ∧ ρ ≤ υ ∨
      τ = Optional ρ ∧ ρ < υ)"

lemma errorable_less_left_simps:
  "ErrorFree ρ < σ = (∃υ.
      σ = ErrorFree υ ∧ ρ < υ ∨
      σ = Errorable υ ∧ ρ ≤ υ)"
  "Errorable ρ < σ = (∃υ.
      σ = Errorable υ ∧ ρ < υ)"

lemma errorable_less_right_simps:
  "τ < ErrorFree υ = (∃ρ.
      τ = ErrorFree ρ ∧ ρ < υ)"
  "τ < Errorable υ = (∃ρ.
      τ = ErrorFree ρ ∧ ρ ≤ υ ∨
      τ = Errorable ρ ∧ ρ < υ)"

Upper Semilattice of Types

fun type_sup (infixl "⊔T" 65)
and type_supN (infixl "⊔N" 65) where
  "OclAny ⊔T σ = OclAny"
| "OclVoid ⊔T σ = σ"

| "Boolean ⊔T σ = (case σ
    of Boolean ⇒ Boolean
     | OclVoid ⇒ Boolean
     | _ ⇒ OclAny)"
| "Real ⊔T σ = (case σ
    of Real ⇒ Real
     | Integer ⇒ Real
     | OclVoid ⇒ Real
     | _ ⇒ OclAny)"
| "Integer ⊔T σ = (case σ
    of Real ⇒ Real
     | Integer ⇒ Integer
     | OclVoid ⇒ Integer
     | _ ⇒ OclAny)"
| "UnlimitedNatural ⊔T σ = (case σ
    of UnlimitedNatural ⇒ UnlimitedNatural
     | OclVoid ⇒ UnlimitedNatural
     | _ ⇒ OclAny)"
| "String ⊔T σ = (case σ
    of String ⇒ String
     | OclVoid ⇒ String
     | _ ⇒ OclAny)"

| "Enum ℰ ⊔T σ = (case σ
    of Enum ℰ' ⇒ if ℰ = ℰ' then Enum ℰ else OclAny
     | OclVoid ⇒ Enum ℰ
     | _ ⇒ OclAny)"
| "⟨𝒞⟩𝒯 ⊔T σ = (case σ
    of ⟨𝒟⟩𝒯 ⇒ ⟨𝒞 ⊔ 𝒟⟩𝒯
     | OclVoid ⇒ ⟨𝒞⟩𝒯
     | _ ⇒ OclAny)"
| "Tuple π ⊔T σ = (case σ
    of Tuple ξ ⇒ Tuple (fmmerge_fun (⊔N) π ξ)
     | OclVoid ⇒ Tuple π
     | _ ⇒ OclAny)"

| "Collection τ ⊔T σ = (case σ
    of Collection ρ ⇒ Collection (τ ⊔N ρ)
     | Set ρ ⇒ Collection (τ ⊔N ρ)
     | OrderedSet ρ ⇒ Collection (τ ⊔N ρ)
     | Bag ρ ⇒ Collection (τ ⊔N ρ)
     | Sequence ρ ⇒ Collection (τ ⊔N ρ)
     | OclVoid ⇒ Collection τ
     | _ ⇒ OclAny)"
| "Set τ ⊔T σ = (case σ
    of Collection ρ ⇒ Collection (τ ⊔N ρ)
     | Set ρ ⇒ Set (τ ⊔N ρ)
     | OrderedSet ρ ⇒ Collection (τ ⊔N ρ)
     | Bag ρ ⇒ Collection (τ ⊔N ρ)
     | Sequence ρ ⇒ Collection (τ ⊔N ρ)
     | OclVoid ⇒ Set τ
     | _ ⇒ OclAny)"
| "OrderedSet τ ⊔T σ = (case σ
    of Collection ρ ⇒ Collection (τ ⊔N ρ)
     | Set ρ ⇒ Collection (τ ⊔N ρ)
     | OrderedSet ρ ⇒ OrderedSet (τ ⊔N ρ)
     | Bag ρ ⇒ Collection (τ ⊔N ρ)
     | Sequence ρ ⇒ Collection (τ ⊔N ρ)
     | OclVoid ⇒ OrderedSet τ
     | _ ⇒ OclAny)"
| "Bag τ ⊔T σ = (case σ
    of Collection ρ ⇒ Collection (τ ⊔N ρ)
     | Set ρ ⇒ Collection (τ ⊔N ρ)
     | OrderedSet ρ ⇒ Collection (τ ⊔N ρ)
     | Bag ρ ⇒ Bag (τ ⊔N ρ)
     | Sequence ρ ⇒ Collection (τ ⊔N ρ)
     | OclVoid ⇒ Bag τ
     | _ ⇒ OclAny)"
| "Sequence τ ⊔T σ = (case σ
    of Collection ρ ⇒ Collection (τ ⊔N ρ)
     | Set ρ ⇒ Collection (τ ⊔N ρ)
     | OrderedSet ρ ⇒ Collection (τ ⊔N ρ)
     | Bag ρ ⇒ Collection (τ ⊔N ρ)
     | Sequence ρ ⇒ Sequence (τ ⊔N ρ)
     | OclVoid ⇒ Sequence τ
     | _ ⇒ OclAny)"

| "Map τ σ ⊔T φ = (case φ
    of Map ρ υ ⇒ Map (τ ⊔N ρ) (σ ⊔N υ)
     | OclVoid ⇒ Map τ σ
     | _ ⇒ OclAny)"

| "Required τ ⊔N σ = (case σ
    of Required ρ ⇒ Required (τ ⊔T ρ)
     | Optional ρ ⇒ Optional (τ ⊔T ρ))"
| "Optional τ ⊔N σ = (case σ
    of Required ρ ⇒ Optional (τ ⊔T ρ)
     | Optional ρ ⇒ Optional (τ ⊔T ρ))"

primrec sup_errorable where
  "ErrorFree τ ⊔ σ = (case σ
    of ErrorFree ρ ⇒ ErrorFree (τ ⊔ ρ)
     | Errorable ρ ⇒ Errorable (τ ⊔ ρ))"
| "Errorable τ ⊔ σ = (case σ
    of ErrorFree ρ ⇒ Errorable (τ ⊔ ρ)
     | Errorable ρ ⇒ Errorable (τ ⊔ ρ))"

Type Notation

Notation	Meaning
τ	a type with unspecified nullability and errorability
τ[1]	a null-free and error-free type
τ[?]	a nullable and error-free type
τ[1!]	a null-free and errorable type
τ[?!]	a nullable and errorable type
τ[!]	an errorable variant of a type τ
τ[??]	a variant of a type τ with all null-free types replaced by their nullable variants recursively
Collectionk(τ)	a collection type of a kind k with element type τ; k is optional
OrderedCollectionk(τ)	an ordered collection type of a kind k with element type τ; k is optional
NonOrderedCollectionk(τ)	a non-ordered collection type of a kind k with element type τ; k is optional
UniqueCollectionk(τ)	an unqie collection type of a kind k with element type τ; k is optional
NonUniqueCollectionk(τ)	an non-unqie collection type of a kind k with element type τ; k is optional
NonCollection(τ)	a non-collection type; τ is an inner ordinary type
Iterable(τ)	either a collection type of any kind with element type τ, or a map type with a key type τ
NonIterable(τ)	a non-collection and non-map type; τ is an inner ordinary type

Typing

Operations Typing

A strict operation is an operation that is defined for invalid source and arguments and returns an invalid value if any of its source or arguments is invalid.

A non-strict operation is an operation that either is not defined for invalid source and arguments or returns a valid value for invalid source or arguments.

A null-safe operation is an operation that is defined for a nullable source.

All metaclass and type operations are non-strict, because neither source nor argument types can be invalid. For these operations we define rules for errorable types explicitly.

Most of the other operations are strict by default. The typing rules for errorable source and arguments are defined implicitly. The only exclusion from this rule is the following non-strict operations:

• oclIsUndefined()
• oclIsInvalid()
• and
• or
• xor
• implies

For non-strict operations, we specify typing rules for errorable types explicitly.

Please take a note that most of the operations are undefined for nullable types. This is a significant difference from the current version of the OCL specification. The OCL specification allows operation invocation with null sources and arguments with invalid result. We prohibit it.

Metaclass Operations

allInstances() is not defined for errorable source types, because a resulting collection can not contain invalid.

Operation	Source Type	Result Type	Precondition
allInstances	τ[1]	Set(τ[1])[1]	finite_type τ
allInstances	τ[?]	Set(τ[?])[1]	finite_type τ

Type Operations

selectByKind() and selectByType() are not defined for errorable argument types, because a source collection can not contain invalid.

Operation	Source Type	Argument Type	Result Type	Precondition
oclAsType	τ	σ	σ	τ < σ
oclAsType	τ	σ	σ[!]	σ < τ
oclIsTypeOf	τ[1]	σ	Boolean[1]	σ < τ[1]
oclIsTypeOf	τ[?]	σ	Boolean[1!]	σ < τ[?]
oclIsTypeOf	τ[?!]	σ	Boolean[1!]	σ < τ[1!]
oclIsTypeOf	τ[?!]	σ	Boolean[1!]	σ < τ[?!]
oclIsKindOf	τ[1]	σ	Boolean[1]	σ < τ[1]
oclIsKindOf	τ[?]	σ	Boolean[1!]	σ < τ[?]
oclIsKindOf	τ[?!]	σ	Boolean[1!]	σ < τ[1!]
oclIsKindOf	τ[?!]	σ	Boolean[1!]	σ < τ[?!]
selectByKind	Collectionk(τ)[1]	σ	Collectionk(σ)[1]	σ < τ
selectByType	Collectionk(τ)[1]	σ	Collectionk(σ)[1]	σ < τ

OclAny Operations

oclAsSet() is not defined for a source with an errorable type, because a resulting collection can not contain invalid.

Operation	Source Type	Result Type	Precondition
oclAsSet	NonIterable(τ)[_]	Set(τ[1])[1]
oclIsNew	ObjectType(𝒞)[_]	Boolean[1]
oclIsUndefined	τ[?]	Boolean[1]
oclIsUndefined	τ[1!]	Boolean[1]
oclIsUndefined	τ[?!]	Boolean[1]
oclIsInvalid	τ[1!]	Boolean[1]
oclIsInvalid	τ[?!]	Boolean[1]
toString	τ	String[1]

Operation	Source Type	Argument Type	Result Type	Precondition
=	τ	σ	Boolean[1]	τ ≤ σ ∨ σ < τ
<>	τ	σ	Boolean[1]	τ ≤ σ ∨ σ < τ

Boolean Operations

Operation	Source Type	Result Type	Precondition
not	τ	τ	τ ≤ Boolean[?!]

Operation	Source Type	Argument Type	Result Type	Precondition
and	τ	σ	τ ⊔ σ	τ ⊔ σ ≤ Boolean[?!]
or	τ	σ	τ ⊔ σ	τ ⊔ σ ≤ Boolean[?!]
xor	τ	σ	τ ⊔ σ	τ ⊔ σ ≤ Boolean[?!]
implies	τ	σ	τ ⊔ σ	τ ⊔ σ ≤ Boolean[?!]

Numeric Operations

Operation	Source Type	Result Type	Precondition
-	Real[1]	Real[1]
-	Integer[1]	Integer[1]
abs	Real[1]	Real[1]
abs	Integer[1]	Integer[1]
floor	Real[1]	Integer[1]
round	Real[1]	Integer[1]
toInteger	UnlimitedNatural[1]	Integer[1!]

Operation	Source Type	Argument Type	Result Type	Precondition
+	τ	σ	τ ⊔ σ	Integer[1] ≤ τ ≤ Real[1] ∧ Integer[1] ≤ σ ≤ Real[1]
+	τ	σ	UnlimitedNatural[1!]	τ = UnlimitedNatural[1] ∧ σ = UnlimitedNatural[1]
-	τ	σ	τ ⊔ σ	Integer[1] ≤ τ ≤ Real[1] ∧ Integer[1] ≤ σ ≤ Real[1]
*	τ	σ	τ ⊔ σ	Integer[1] ≤ τ ≤ Real[1] ∧ Integer[1] ≤ σ ≤ Real[1]
*	τ	σ	UnlimitedNatural[1!]	τ = UnlimitedNatural[1] ∧ σ = UnlimitedNatural[1]
/	τ	σ	Real[1!]	Integer[1] ≤ τ ≤ Real[1] ∧ Integer[1] ≤ σ ≤ Real[1]
/	τ	σ	Real[1!]	τ = UnlimitedNatural[1] ∧ σ = UnlimitedNatural[1]
div	τ	σ	Integer[1!]	τ = Integer[1] ∧ σ = Integer[1]
div	τ	σ	UnlimitedNatural[1!]	τ = UnlimitedNatural[1] ∧ σ = UnlimitedNatural[1]
mod	τ	σ	Integer[1!]	τ = Integer[1] ∧ σ = Integer[1]
mod	τ	σ	UnlimitedNatural[1!]	τ = UnlimitedNatural[1] ∧ σ = UnlimitedNatural[1]
max	τ	σ	τ ⊔ σ	Integer[1] ≤ τ ≤ Real[1] ∧ Integer[1] ≤ σ ≤ Real[1]
max	τ	σ	UnlimitedNatural[1]	τ = UnlimitedNatural[1] ∧ σ = UnlimitedNatural[1]
min	τ	σ	τ ⊔ σ	Integer[1] ≤ τ ≤ Real[1] ∧ Integer[1] ≤ σ ≤ Real[1]
min	τ	σ	UnlimitedNatural[1]	τ = UnlimitedNatural[1] ∧ σ = UnlimitedNatural[1]
<	τ	σ	Boolean[1]	Integer[1] ≤ τ ≤ Real[1] ∧ Integer[1] ≤ σ ≤ Real[1]
<	τ	σ	Boolean[1]	τ = UnlimitedNatural[1] ∧ σ = UnlimitedNatural[1]
<=	τ	σ	Boolean[1]	Integer[1] ≤ τ ≤ Real[1] ∧ Integer[1] ≤ σ ≤ Real[1]
<=	τ	σ	Boolean[1]	τ = UnlimitedNatural[1] ∧ σ = UnlimitedNatural[1]
>	τ	σ	Boolean[1]	Integer[1] ≤ τ ≤ Real[1] ∧ Integer[1] ≤ σ ≤ Real[1]
>	τ	σ	Boolean[1]	τ = UnlimitedNatural[1] ∧ σ = UnlimitedNatural[1]
>=	τ	σ	Boolean[1]	Integer[1] ≤ τ ≤ Real[1] ∧ Integer[1] ≤ σ ≤ Real[1]
>=	τ	σ	Boolean[1]	τ = UnlimitedNatural[1] ∧ σ = UnlimitedNatural[1]

String Operations

Operation	Source Type	Result Type	Precondition
size	String[1]	Integer[1]
characters	String[1]	Sequence(String[1])[1]
toUpperCase	String[1]	String[1]
toLowerCase	String[1]	String[1]
toBoolean	String[1]	Boolean[1!]
toReal	String[1]	Real[1!]
toInteger	String[1]	Integer[1!]

Operation	Source Type	Argument Type	Result Type	Precondition
concat	String[1]	String[1]	String[1]
equalsIgnoreCase	String[1]	String[1]	Boolean[1]
<	String[1]	String[1]	Boolean[1]
<=	String[1]	String[1]	Boolean[1]
>	String[1]	String[1]	Boolean[1]
>=	String[1]	String[1]	Boolean[1]
indexOf	String[1]	String[1]	Integer[1]
at	String[1]	Integer[1]	String[1!]

Operation	Source Type	Argument Type	2nd Argument Type	Result Type	Precondition
substring	String[1]	Integer[1]	Integer[1]	String[1!]

Iterable Operations

Operation	Source Type	Result Type	Precondition
size	Iterable(τ)[1]	Integer[1]
isEmpty	Iterable(τ)[1]	Boolean[1]
notEmpty	Iterable(τ)[1]	Boolean[1]
max	Collection(τ)[1]	τ	a binary operation "max" is defined for τ
min	Collection(τ)[1]	τ	a binary operation "min" is defined for τ
sum	Collection(τ)[1]	τ	a binary operation "+" is defined for τ
asSet	Collection(τ)[1]	Set(τ)[1]
asOrderedSet	Collection(τ)[1]	OrderedSet(τ)[1]
asBag	Collection(τ)[1]	Bag(τ)[1]
asSequence	Collection(τ)[1]	Sequence(τ)[1]
flatten	Collectionk(τ)[1]	Collectionk(to_single_type τ)[1]
first	OrderedCollection(τ)[1]	τ[!]
last	OrderedCollection(τ)[1]	τ[!]
reverse	OrderedCollection(τ)[1]	OrderedCollection(τ)[1]
keys	Map(τ, σ)[1]	Set(τ)[1]
values	Map(τ, σ)[1]	Bag(τ)[1]

Operation	Source Type	Argument Type	Result Type	Precondition
count	Collection(τ)[1]	σ	Integer[1]	σ ≤ τ[??]
includes	Iterable(τ)[1]	σ	Boolean[1]	σ ≤ τ[??]
excludes	Iterable(τ)[1]	σ	Boolean[1]	σ ≤ τ[??]
includesValue	Map(τ, ρ)[1]	σ	Boolean[1]	σ ≤ ρ[??]
excludesValue	Map(τ, ρ)[1]	σ	Boolean[1]	σ ≤ ρ[??]
includesAll	Iterable(τ)[1]	Collection(σ)[1]	Boolean[1]	σ ≤ τ[??]
excludesAll	Iterable(τ)[1]	Collection(σ)[1]	Boolean[1]	σ ≤ τ[??]
includesMap	Map(τ, ρ)[1]	Map(σ, υ)[1]	Boolean[1]	σ ≤ τ[??] ∧ υ ≤ ρ[??]
excludesMap	Map(τ, ρ)[1]	Map(σ, υ)[1]	Boolean[1]	σ ≤ τ[??] ∧ υ ≤ ρ[??]
product	Collection(τ)[1]	Collection(σ)[1]	Set(Tuple(first: τ, second: σ)[1])[1]
union	Set(τ)[1]	Set(σ)[1]	Set(τ ⊔ σ)[1]
union	Set(τ)[1]	Bag(σ)[1]	Bag(τ ⊔ σ)[1]
union	Bag(τ)[1]	Set(σ)[1]	Bag(τ ⊔ σ)[1]
union	Bag(τ)[1]	Bag(σ)[1]	Bag(τ ⊔ σ)[1]
intersection	Set(τ)[1]	Set(σ)[1]	Set(τ ⊔ σ)[1]
intersection	Set(τ)[1]	Bag(σ)[1]	Set(τ ⊔ σ)[1]
intersection	Bag(τ)[1]	Set(σ)[1]	Set(τ ⊔ σ)[1]
intersection	Bag(τ)[1]	Bag(σ)[1]	Bag(τ ⊔ σ)[1]
-	Set(τ)[1]	Set(σ)[1]	Set(τ)[1]	τ ≤ σ ∨ σ ≤ τ
symmetricDifference	Set(τ)[1]	Set(σ)[1]	Set(τ ⊔ σ)[1]
including	Collectionk(τ)[1]	σ	Collectionk(τ ⊔ σ)[1]
excluding	Collection(τ)[1]	σ	Collection(τ)[1]	σ ≤ τ
includingAll	Collectionk(τ)[1]	Collection(σ)[1]	Collectionk(τ ⊔ σ)[1]
excludingAll	Collection(τ)[1]	Collection(σ)[1]	Collection(τ)[1]	σ ≤ τ
includingMap	Map(τ, ρ)[1]	Map(σ, υ)[1]	Map(τ ⊔ σ, ρ ⊔ υ)[1]
excludingMap	Map(τ, ρ)[1]	Map(σ, υ)[1]	Map(τ, ρ)[1]	σ ≤ τ ∧ υ ≤ ρ
append	OrderedCollection(τ)[1]	σ	OrderedCollection(τ)[1]	σ ≤ τ
prepend	OrderedCollection(τ)[1]	σ	OrderedCollection(τ)[1]	σ ≤ τ
appendAll	OrderedCollection(τ)[1]	OrderedCollection(σ)[1]	OrderedCollection(τ)[1]	σ ≤ τ
prependAll	OrderedCollection(τ)[1]	OrderedCollection(σ)[1]	OrderedCollection(τ)[1]	σ ≤ τ
at	OrderedCollection(τ)[1]	Integer[1]	τ[!]
at	Map(τ, ρ)[1]	σ	ρ[!]	σ ≤ τ
indexOf	OrderedCollection(τ)[1]	σ	Integer[1]	σ ≤ τ

Operation	Source Type	Argument Type	2nd Argument Type	Result Type	Precondition
insertAt	OrderedCollection(τ)[1]	Integer[1]	σ	OrderedCollection(τ)[1!]	σ ≤ τ
subOrderedSet	OrderedSet(τ)[1]	Integer[1]	Integer[1]	OrderedSet(τ)[1!]
subSequence	Sequence(τ)[1]	Integer[1]	Integer[1]	Sequence(τ)[1!]
includes	Map(τ, ρ)[1]	σ	υ	Boolean[1]	σ ≤ τ ∧ υ ≤ ρ
excludes	Map(τ, ρ)[1]	σ	υ	Boolean[1]	σ ≤ τ ∧ υ ≤ ρ
including	Map(τ, ρ)[1]	σ	υ	Map(τ ⊔ σ, ρ ⊔ υ)[1]
excluding	Map(τ, ρ)[1]	σ	υ	Map(τ, ρ)[1]	σ ≤ τ ∧ υ ≤ ρ

Expressions Typing

inductive typing :: "('a :: ocl_object_model) typeNE env ⇒ 'a expr ⇒ 'a typeNE ⇒ bool"
       ("(1_/ ⊢E/ (_ :/ _))" [51,51,51] 50)
      and collection_part_typing ("(1_/ ⊢C/ (_ :/ _))" [51,51,51] 50)
      and iterator_typing ("(1_/ ⊢I/ (_ :/ _))" [51,51,51] 50)
      and expr_list_typing ("(1_/ ⊢L/ (_ :/ _))" [51,51,51] 50) where

― ‹Primitive Literals›

 NullLiteralT:
  "Γ ⊢E NullLiteral : OclVoid[?]"
|BooleanLiteralT:
  "Γ ⊢E BooleanLiteral c : Boolean[1]"
|RealLiteralT:
  "Γ ⊢E RealLiteral c : Real[1]"
|IntegerLiteralT:
  "Γ ⊢E IntegerLiteral c : Integer[1]"
|UnlimitedNaturalLiteralT:
  "Γ ⊢E UnlimitedNaturalLiteral c : UnlimitedNatural[1]"
|StringLiteralT:
  "Γ ⊢E StringLiteral c : String[1]"
|EnumLiteralT:
  "has_literal enm lit ⟹
   Γ ⊢E EnumLiteral enm lit : (Enum enm)[1]"

― ‹Tuple Literals›

|TupleLiteralNilT:
  "Γ ⊢E TupleLiteral [] : (Tuple fmempty)[1]"
|TupleLiteralConsT:
  "Γ ⊢E tuple_literal_element_expr el : τ ⟹
   tuple_literal_element_type el = Some σ ⟹
   τ ≤ σ ⟹
   ρ ↩ Tuple([tuple_literal_element_name el ↦⇩f σ])[1] ⟹
   Γ ⊢E TupleLiteral elems : υ ⟹
   Γ ⊢E TupleLiteral (el # elems) : ρ ⊔ υ"

― ‹Collection Literals›

|CollectionLiteralNilT:
  "k ≠ CollectionKind ⟹
   σ ↩ Collectionk(OclVoid[1])[1] ⟹
   Γ ⊢E CollectionLiteral k [] : σ"
|CollectionLiteralConsT:
  "k ≠ CollectionKind ⟹
   Γ ⊢C x : τ ⟹
   σ ↩ Collectionk(τ)[1] ⟹
   Γ ⊢E CollectionLiteral k xs : ρ ⟹
   Γ ⊢E CollectionLiteral k (x # xs) : σ ⊔ ρ"

|CollectionPartItemT:
  "Γ ⊢E a : τ ⟹
   Γ ⊢C CollectionItem a : τ"
|CollectionPartRangeT:
  "Γ ⊢E a : Integer[1] ⟹ Γ ⊢E b : Integer[1] ⟹
   Γ ⊢C CollectionRange a b : Integer[1]"
|LowerErrorableCollectionPartRangeT:
  "Γ ⊢E a : Integer[1!] ⟹ Γ ⊢E b : Integer[1] ⟹
   Γ ⊢C CollectionRange a b : Integer[1!]"
|UpperErrorableCollectionPartRangeT:
  "Γ ⊢E a : Integer[1] ⟹ Γ ⊢E b : Integer[1!] ⟹
   Γ ⊢C CollectionRange a b : Integer[1!]"
|ErrorableCollectionPartRangeT:
  "Γ ⊢E a : Integer[1!] ⟹ Γ ⊢E b : Integer[1!] ⟹
   Γ ⊢C CollectionRange a b : Integer[1!]"

― ‹Map Literals›

|MapNilT:
  "τ ↩ Map(OclVoid[1], OclVoid[1])[1] ⟹
   Γ ⊢E MapLiteral [] : τ"
|MapConsT:
  "Γ ⊢E map_literal_element_key x : τ ⟹
   Γ ⊢E map_literal_element_value x : σ ⟹
   ρ ↩ Map(τ, σ)[1] ⟹
   Γ ⊢E MapLiteral xs : υ ⟹
   Γ ⊢E MapLiteral (x # xs) : ρ ⊔ υ"

― ‹Misc Expressions›

|LetT:
  "Γ ⊢E init : σ ⟹
   σ ≤ τ ⟹
   Γ(v ↦⇩f τ) ⊢E body : ρ ⟹
   Γ ⊢E Let v (Some τ) init body : ρ"
|VarT:
  "fmlookup Γ v = Some τ ⟹
   Γ ⊢E Var v : τ"
|IfT:
  "Γ ⊢E cnd : Boolean[1] ⟹
   Γ ⊢E thn : σ ⟹
   Γ ⊢E els : ρ ⟹
   Γ ⊢E If cnd thn els : σ ⊔ ρ"
|ErrorableIfT:
  "Γ ⊢E cnd : Boolean[1!] ⟹
   Γ ⊢E thn : σ ⟹
   Γ ⊢E els : ρ ⟹
   Γ ⊢E If cnd thn els : (σ ⊔ ρ)[!]"

― ‹Call Expressions›

|MetaOperationCallT:
  "mataop_type τ op σ ⟹
   Γ ⊢E MetaOperationCall τ op : σ"

|StaticOperationCallT:
  "Γ ⊢L params : π ⟹
   static_operation τ op π oper ⟹
   ¬ fBex (fset_of_list π) errorable_type ⟹
   Γ ⊢E StaticOperationCall τ op params : oper_type oper"
|ErrorableStaticOperationCallT:
  "Γ ⊢L params : π ⟹
   static_operation τ op π oper ⟹
   fBex (fset_of_list π) errorable_type ⟹
   Γ ⊢E StaticOperationCall τ op params : (oper_type oper)[!]"

|TypeOperationCallT:
  "Γ ⊢E a : τ ⟹
   typeop_type k op τ σ ρ ⟹
   Γ ⊢E TypeOperationCall a k op σ : ρ"

|OperationCallT:
  "Γ ⊢E src : τ ⟹
   Γ ⊢L params : π ⟹
   op_type op k τ π σ ⟹
   Γ ⊢E OperationCall src k op params : σ"

|AttributeCallT:
  "Γ ⊢E src : ⟨𝒞⟩𝒯[1] ⟹
   attribute 𝒞 prop 𝒟 τ ⟹
   Γ ⊢E AttributeCall src prop : τ"
|ErrorableAttributeCallT:
  "Γ ⊢E src : ⟨𝒞⟩𝒯[1!] ⟹
   attribute 𝒞 prop 𝒟 τ ⟹
   Γ ⊢E AttributeCall src prop : τ[!]"

|AssociationEndCallT:
  "Γ ⊢E src : ⟨𝒞⟩𝒯[1] ⟹
   association_end 𝒞 from role 𝒟 end ⟹
   Γ ⊢E AssociationEndCall src from role : assoc_end_type end"
|ErrorableAssociationEndCallT:
  "Γ ⊢E src : ⟨𝒞⟩𝒯[1!] ⟹
   association_end 𝒞 from role 𝒟 end ⟹
   Γ ⊢E AssociationEndCall src from role : (assoc_end_type end)[!]"

|AssociationClassCallT:
  "Γ ⊢E src : ⟨𝒞⟩𝒯[1] ⟹
   referred_by_association_class 𝒞 from 𝒜 𝒟 ⟹
   Γ ⊢E AssociationClassCall src from 𝒜 : class_assoc_type 𝒜"
|ErrorableAssociationClassCallT:
  "Γ ⊢E src : ⟨𝒞⟩𝒯[1!] ⟹
   referred_by_association_class 𝒞 from 𝒜 𝒟 ⟹
   Γ ⊢E AssociationClassCall src from 𝒜 : (class_assoc_type 𝒜)[!]"

|AssociationClassEndCallT:
  "Γ ⊢E src : ⟨𝒜⟩𝒯[1] ⟹
   association_class_end 𝒜 role end ⟹
   Γ ⊢E AssociationClassEndCall src role : class_assoc_end_type end"
|ErrorableAssociationClassEndCallT:
  "Γ ⊢E src : ⟨𝒜⟩𝒯[1!] ⟹
   association_class_end 𝒜 role end ⟹
   Γ ⊢E AssociationClassEndCall src role : (class_assoc_end_type end)[!]"

|TupleElementCallT:
  "Γ ⊢E src : (Tuple π)[1] ⟹
   fmlookup π elem = Some τ ⟹
   Γ ⊢E TupleElementCall src elem : ErrorFree τ"
|ErrorableTupleElementCallT:
  "Γ ⊢E src : (Tuple π)[1!] ⟹
   fmlookup π elem = Some τ ⟹
   Γ ⊢E TupleElementCall src elem : Errorable τ"

― ‹Iterator Expressions›

|CollectionLoopT:
  "Γ ⊢E src : τ ⟹
   τ ↪ Collection(σ)[1] ⟹
   σ ≤ its_ty ⟹
   list_all (λit. snd it = None) its ⟹
   Γ ++⇩f iterators its its_ty ⊢E body : ρ ⟹
   Γ ⊢I (src, its, (Some its_ty, None), body) : (τ, σ, ρ)"
|MapLoopT:
  "Γ ⊢E src : τ ⟹
   τ ↪ Map(σ, υ)[1] ⟹
   σ ≤ its_key_ty ⟹
   υ ≤ its_val_ty ⟹
   Γ ++⇩f iterators its its_key_ty ++⇩f coiterators its its_val_ty ⊢E body : ρ ⟹
   Γ ⊢I (src, its, (Some its_key_ty, Some its_val_ty), body) : (τ, σ, ρ)"

|IterateT:
  "Γ ⊢I (src, its, its_ty, Let res (Some res_t) res_init body) : (τ, σ, ρ) ⟹
   ρ ≤ res_t ⟹
   Γ ⊢E IterateCall src its its_ty res (Some res_t) res_init body : ρ"

|AnyIterationT:
  "Γ ⊢I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
   length its ≤ 1 ⟹
   ρ ≤ Boolean[?] ⟹
   Γ ⊢E AnyIterationCall src its its_ty body : σ[!]"
|ClosureIterationT:
  "Γ ⊢I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
   length its ≤ 1 ⟹
   τ ↪ Collectionk(σ)[1] ⟹
   ρ ↪ Collectionk(φ)[1] ⟹
   φ ≤ σ ⟹
   υ ↩ UniqueCollectionk(σ)[1] ⟹
   Γ ⊢E ClosureIterationCall src its its_ty body : υ"

|CollectionCollectIterationT:
  "Γ ⊢I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
   length its ≤ 1 ⟹
   to_single_type ρ ρ' ⟹
   τ ↪ Collectionk(σ)[1] ⟹
   υ ↩ NonUniqueCollectionk(ρ')[1] ⟹
   Γ ⊢E CollectIterationCall src its its_ty body : υ"
|MapCollectIterationT:
  "Γ ⊢I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
   length its ≤ 1 ⟹
   to_single_type ρ ρ' ⟹
   τ ↪ Map(_, _)[1] ⟹
   υ ↩ Bag(ρ')[1] ⟹
   Γ ⊢E CollectIterationCall src its its_ty body : υ"

|CollectByIterationT:
  "Γ ⊢I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
   length its ≤ 1 ⟹
   υ ↩ Map(σ, ρ)[1] ⟹
   Γ ⊢E CollectByIterationCall src its its_ty body : υ"

|CollectionCollectNestedIterationT:
  "Γ ⊢I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
   length its ≤ 1 ⟹
   τ ↪ Collectionk(σ)[1] ⟹
   υ ↩ NonUniqueCollectionk(ρ)[1] ⟹
   Γ ⊢E CollectNestedIterationCall src its its_ty body : υ"
|MapCollectNestedIterationT:
  "Γ ⊢I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
   length its ≤ 1 ⟹
   τ ↪ Map(υ, _)[1] ⟹
   φ ↩ Map(υ, ρ)[1] ⟹
   Γ ⊢E CollectNestedIterationCall src its its_ty body : φ"

|ExistsIterationT:
  "Γ ⊢I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
   ρ ≤ Boolean[?!] ⟹
   Γ ⊢E ExistsIterationCall src its its_ty body : ρ"
|ForAllIterationT:
  "Γ ⊢I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
   ρ ≤ Boolean[?!] ⟹
   Γ ⊢E ForAllIterationCall src its its_ty body : ρ"
|OneIterationT:
  "Γ ⊢I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
   length its ≤ 1 ⟹
   ρ ≤ Boolean[?] ⟹
   Γ ⊢E OneIterationCall src its its_ty body : Boolean[1]"
|IsUniqueIterationT:
  "Γ ⊢I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
   length its ≤ 1 ⟹
   Γ ⊢E IsUniqueIterationCall src its its_ty body : Boolean[1]"
|SelectIterationT:
  "Γ ⊢I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
   length its ≤ 1 ⟹
   ρ ≤ Boolean[?] ⟹
   Γ ⊢E SelectIterationCall src its its_ty body : τ"
|RejectIterationT:
  "Γ ⊢I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
   length its ≤ 1 ⟹
   ρ ≤ Boolean[?] ⟹
   Γ ⊢E RejectIterationCall src its its_ty body : τ"
|SortedByIterationT:
  "Γ ⊢I (src, its, its_ty, body) : (τ, σ, ρ) ⟹
   length its ≤ 1 ⟹
   τ ↪ Collectionk(σ)[1] ⟹
   υ ↩ OrderedCollectionk(σ)[1] ⟹
   Γ ⊢E SortedByIterationCall src its its_ty body : υ"

― ‹Expression Lists›

|ExprListNilT:
  "Γ ⊢L [] : []"
|ExprListConsT:
  "Γ ⊢E expr : τ ⟹
   Γ ⊢L exprs : π ⟹
   Γ ⊢L expr # exprs : τ # π"

Normalization

The following variables are used in the table:

• x is a non-nullable single or tuple value,
• n is a nullable single or tuple value,
• xs is a non-nullable iterable value of non-nullable values,
• ns is a non-nullable iterable value of nullable values.
• nxs is a nullable iterable value of non-nullable values,
• nns is a nullable iterable value of nullable values.

The following type variables are used in the table:

• T[1] is a non-nullable variant of a value's type,
• S[1] is a non-nullable variant of a iterable value's type.

Original Expression	Normalized Closure Body
src->closure(x)	src->closure(x.oclAsSet())
src->closure(n)	src->closure(n.oclAsSet())
src?->closure(x)	src?->closure(x.oclAsSet())
src?->closure(n)	src?->closure(n.oclAsSet())
src->closure(xs)	src->closure(xs)
src->closure(ns)	src->closure(ns)
src->closure(nxs)	src->closure(nxs)
src->closure(nns)	src->closure(nns)
src?->closure(xs)	src?->closure(xs)
src?->closure(ns)	src?->closure(ns->selectByKind(T[1]))
src?->closure(nxs)	src?->closure(if nxs <> null then nxs.oclAsType(S[1]) else Collectionk(T)[1] endif)
src?->closure(nns)	src?->closure(if nns <> null then nns.oclAsType(S[1])->selectByKind(T[1]) else Collectionk(T)[1] endif)

Original Expression	Normalized Expression	Note
x.op()	x.op()
n.op()	n.op()	(1)
x?.op()	–
n?.op()	if n <> null then n.oclAsType(T[1]).op() else null endif	(2)
x->op()	x.oclAsSet()->op()
n->op()	n.oclAsSet()->op()
x?->op()	–
n?->op()	–
xs.op()	xs->collect(x | x.op())
ns.op()	ns->collect(n | n.op())	(1)
xs?.op()	–
ns?.op()	ns->selectByKind(T[1])->collect(x | x.op())
xs->op()	xs->op()
ns->op()	ns->op()
xs?->op()	–
ns?->op()	ns->selectByKind(T[1])->op()
nxs.op()	–
nns.op()	–
nxs?.op()	if nxs <> null then nxs.oclAsType(S[1])->collect(x | x.op()) else null endif
nns?.op()	if nns <> null then nns.oclAsType(S[1])->selectByKind(T[1])->collect(x | x.op()) else null endif
nxs->op()	nxs->op()	(1)
nns->op()	nns->op()	(1)
nxs?->op()	if nxs <> null then nxs.oclAsType(S[1])->op() else null endif
nns?->op()	if nns <> null then nns.oclAsType(S[1])->selectByKind(T[1])->op() else null endif

(1) The resulting expression will be ill-typed if the operation is unsafe. An unsafe operation is an operation which is not well-typed for a nullable source.

(2) It would be a good idea to prohibit such a transformation for safe operations. A safe operation is an operation which is well-typed for a nullable source. However, it is hard to define safe operations formally considering operations overloading, complex relations between operation parameters types (please see the typing rules for the equality operator), and user-defined operations.