# Safe OCL

 Title: Safe OCL Author: Denis Nikiforov Submission date: 2019-03-09 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. BibTeX: @article{Safe_OCL-AFP, author = {Denis Nikiforov}, title = {Safe OCL}, journal = {Archive of Formal Proofs}, month = mar, year = 2019, note = {\url{https://isa-afp.org/entries/Safe_OCL.html}, Formal proof development}, ISSN = {2150-914x}, } License: GNU Lesser General Public License (LGPL)