### Abstract

The theory is a formalization of the OCL type system, its abstract syntax and expression typing rules. The theory does not define a concrete syntax and a semantics. In contrast to Featherweight OCL, 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 non-nullable types. Also the theory gives a formal definition of safe navigation operations. 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, basic types, generic types, errorable types. We introduce the following new types: non-nullable types (T[1]), nullable types (T[?]), OclSuper. OclSuper is 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 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.

### License

GNU Lesser General Public License (LGPL)

### Topics

- Computer science/Programming languages/Language definitions

### Session Safe_OCL

- Errorable
- Transitive_Closure_Ext
- Finite_Map_Ext
- Tuple
- Object_Model
- OCL_Basic_Types
- OCL_Types
- OCL_Syntax
- OCL_Object_Model
- OCL_Typing
- OCL_Normalization
- OCL_Examples

## Cite

×

Safe_OCL-AFP

    @article{Safe_OCL-AFP,
      author  = {Denis Nikiforov},
      title   = {Safe OCL},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Safe_OCL.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Mar 14, 2019 : Isabelle2018