Email Gateway (Aug 22 2022 at 19:22): Email Gateway (Aug 22 2022 at 19:22):From: Manuel Eberl <eberlm@in.tum.de>
Safe OCL
by Denis Nikiforov
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.
For more details, see https://www.isa-afp.org/entries/Safe_OCL.html
Enjoy,
Manuel
Last updated: Nov 21 2024 at 12:39 UTC