Skip to content

Latest commit

 

History

History
947 lines (825 loc) · 50.4 KB

README.md

File metadata and controls

947 lines (825 loc) · 50.4 KB
Raw

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.