\section{Introduction}
\isatagafp%
The Unified Modeling Language
(UML)~\cite{omg:uml-infrastructure:2011,omg:uml-superstructure:2011}
is one of the few modeling languages that is widely used in
industry. UML is defined in an open process by the Object Management
Group (OMG), \ie, an industry consortium.  While UML is mostly known
as diagrammatic modeling language (\eg, visualizing class models), it
also comprises a textual language, called Object Constraint Language
(OCL)~\cite{omg:ocl:2012}. OCL is a textual annotation language,
originally conceived as a three-valued logic, that turns substantial
parts of UML into a formal language.  Unfortunately the semantics of
this specification language, captured in the ``Annex A'' (originally,
based on the work of \citet{richters:precise:2002}) of the OCL
standard leads to different interpretations of corner cases.  Many of
these corner cases had been subject to formal analysis since more than
nearly fifteen years (see,
\eg,~\cite{brucker.ea:semantic:2006-b,brucker.ea:proposal:2002,mandel.ea:ocl:1999,
  hamie.ea:reflections:1998,cook.ea::amsterdam:2002}).

At its origins~\cite{richters:precise:2002,omg:ocl:1997}, OCL was
conceived as a strict semantics for undefinedness (\eg, denoted by the
element \inlineocl{invalid}\footnote{In earlier versions of the OCL
  standard, this element was called \inlineocl{OclUndefined}.}), with
the exception of the logical connectives of type \inlineocl{Boolean}
that constitute a three-valued propositional logic. At its core, OCL
comprises four layers:
\begin{enumerate}
\item Operators (\eg, \inlineocl{_ and _}, \inlineocl{_ + _}) on
  built-in data structures such as \inlineocl{Boolean},
  \inlineocl{Integer}, or typed sets (\inlineocl{Set(_)}.
\item Operators on the user-defined data model (\eg, defined as part
  of a UML class model) such as accessors, type casts and tests.
\item Arbitrary, user-defined, side-effect-free methods called \emph{queries},
\item Specification for invariants on states and contracts for
  operations to be specified via pre- and post-conditions.
\end{enumerate}

Motivated by the need for aligning OCL closer with UML, recent
versions of the OCL standard~\cite{omg:ocl:2006,omg:ocl:2012} added a
second exception element.  While the first exception element
\inlineocl{invalid} has a strict semantics, \inlineocl{null} has a non
strict semantic interpretation.  Unfortunately, this extension results
in several inconsistencies and contradictions. These problems are
reflected in difficulties to define interpreters, code-generators,
specification animators or theorem provers for OCL in a uniform manner
and resulting incompatibilities of various tools.

For the OCL community, the semantics of \inlineocl{invalid} and
\inlineocl{null} as well as many related issues resulted in the
challenge to define a consistent version of the OCL standard that is
well aligned with the recent developments of the UML\@. A syntactical
and semantical consistent standard requires a major revision of both
the informal and formal parts of the standard. To discuss the future
directions of the standard, several OCL experts met in November 2013
in Aachen to discuss possible mid-term improvements of OCL, strategies
of standardization of OCL within the OMG, and a vision for possible
long-term developments of the
language~\cite{brucker.ea:summary-aachen:2013}. During this meeting, a
Request for Proposals (RFP) for OCL 2.5 was finalized and meanwhile
proposed. In particular, this RFP requires that the future OCL 2.5
standard document shall be generated from a machine-checked
source. This will ensure
\begin{itemize}
\item the absence of syntax errors,
\item the consistency of the formal semantics,
\item a suite of corner-cases relevant for OCL tool implementors.
\end{itemize}

In this document, we present a formalization using
Isabelle/HOL~\cite{nipkow.ea:isabelle:2002} of a core language of
OCL\@. The semantic theory, based on a ``shallow embedding'', is
called \emph{Featherweight OCL}, since it focuses on a formal
treatment of the key-elements of the language (rather than a full
treatment of all operators and thus, a ``complete''
implementation). In contrast to full OCL, it comprises just the logic
captured in \verb+Boolean+, the basic data types \verb+Integer+ \verb+Real+ and 
\verb+String+, the collection types \verb+Set+, \verb+Sequence+ and \verb+Bag+, 
as well as the generic construction principle of class models, which is 
instantiated and demonstrated for two examples (an automated support for 
this type-safe construction is out of the scope of Featherweight OCL).  
This formal semantics
definition is intended to be a proposal for the standardization
process of OCL 2.5, which should ultimately replace parts of the
mandatory part of the standard document~\cite{omg:ocl:2012} as well as
replace completely its informative ``Annex A.''
\endisatagafp
%%
\isatagannexa
This annex chapter formally defines the semantics of \OCL\@. This
chapter is a, to a large extend automatically generated, summary of a
formal semantics of the core of OCL, called \FOCL\footnote{An updated,
  machine-checked version and formally complete version of the
  complete formalization is maintained by the Isabelle Archive of
  Formal Proofs (AFP), see
  \url{http://afp.sourceforge.net/entries/Featherweight_OCL.shtml}}. \FOCL
has a formal semantics in Isabelle/\HOL~\cite{nipkow.ea:isabelle:2002}.
\endisatagannexa

The semantic definitions are in large parts executable, in some parts
only provable, namely the essence of Set-and Bag-constructions. The first goal
of its construction is \emph{consistency}, \ie, it should be possible
to apply logical rules and/or evaluation rules for \OCL in an
arbitrary manner always yielding the same result. Moreover, except in
pathological cases, this result should be unambiguously defined, \ie,
represent a value.

To motivate the need for logical consistency and also the magnitude of
the problem, we focus on one particular feature of the language as
example: \inlineocl{Tuples}. Recall that tuples (in other languages
known as \emph{records}) are $n$-ary Cartesian products with named
components, where the component names are used also as projection
functions: the special case %
\inlineocl+Pair{x:First, y:Second}+ stands for the usual binary
pairing operator \inlineocl+Pair{true,null}+ and the two projection
functions \inlineocl+x.First()+ and \inlineocl+x.Second()+. For a
developer of a compiler or proof-tool (based on, say, a connection to
an SMT solver designed to animate \OCL contracts) it would be natural
to add the rules \inlineocl+Pair{X,Y}.First() = X+ and
\inlineocl+Pair{X,Y}.Second() = Y+ to give pairings the usual
semantics. At some place, the \OCL Standard requires the existence of
a constant symbol \inlineocl+invalid+ and requires all operators to be
strict. To implement this, the developer might be tempted to add a
generator for corresponding strictness axioms, producing among
hundreds of other rules
\inlineocl+Pair{invalid,Y}=invalid+,\inlineocl+Pair{X,invalid}=invalid+,
\inlineocl+invalid.First()=invalid+,
\inlineocl+invalid.Second()=invalid+, etc.  Unfortunately, this
``natural'' axiomatization of pairing and projection together with
strictness is already inconsistent. One can derive:
\begin{ocl}
   Pair{true,invalid}.First() = invalid.First() = invalid
\end{ocl}
and:
\begin{ocl}
   Pair{true,invalid}.First() = true
\end{ocl}
which then results in the absurd logical consequence that
\inlineocl+invalid = true+. Obviously, we need to be more careful on
the side-conditions of our rules\footnote{The solution to this little
  riddle can be found in \autoref{sec:collection_pairs}.}. And
obviously, only a mechanized check of these definitions, following a
rigorous methodology, can establish strong guarantees for logical
consistency of the \OCL language.

\isatagafp
 This leads us to our second goal of this document:
\endisatagafp
\isatagannexa
 This leads us to our second goal of this annex:
\endisatagannexa
it should not only be
usable by logicians, but also by developers of compilers and
proof-tools. For this end, we \emph{derived} from the Isabelle
definitions also \emph{logical rules} allowing formal interactive and
automated proofs on \UML/\OCL specifications, as well as
\emph{execution rules} and \emph{test-cases} revealing corner-cases
resulting from this semantics which give vital information for the
implementor.

\OCL is an annotation language for \UML models, in particular class
models allowing for specifying data and operations on them. As such,
it is a \emph{typed} object-oriented language. This means that it
is---like Java or C++---based on the concept of a \emph{static type},
that is the type that the type-checker infers from a \UML class model
and its \OCL annotation, as well as a \emph{dynamic type}, that is the
type at which an object is dynamically created\footnote{As
  side-effect free language, \OCL has no object-constructors, but with
  \inlineocl+OclIsNew()+, the effect of object creation can be
  expressed in a declarative way.}. Types are not only a means for
efficient compilation and a support of separation of concerns in
programming, there are of fundamental importance for our goal of
logical consistency: it is impossible to have sets that contain
themselves, \ie, to state Russels Paradox in \OCL typed set-theory.
Moreover, object-oriented typing means that types there can be in
sub-typing relation; technically speaking, this means that they can be
\emph{cast} via \inlineocl+oclIsTypeOf(T)+ one to the other, and under
particular conditions to be described in detail later, these casts are
semantically \emph{lossless}, \ie,
\begin{equation}
 (X.oclAsType(C_j).oclAsType(C_i) = X)
\end{equation}
(where $C_j$ and $C_i$ are class types.)
Furthermore, object-oriented means that operations and object-types can be
grouped to \emph{classes} on which an inheritance relation can be established;
the latter induces a sub-type relation between the corresponding types.

Here is a feature-list of  \FOCL:
\begin{itemize}
 \item it specifies key built-in types such as \inlineocl+Boolean+,
         \inlineocl+Void+, \inlineocl+Integer+, \inlineocl+Real+ and 
         \inlineocl+String+ as well as generic types such as 
         \inlineocl+Pair(T,T')+, \inlineocl+Sequence(T)+ and \inlineocl+Set(T)+.
 \item it defines the semantics of the operations of these types in 
         \emph{denotational form}---see explanation below---,
         and thus in an unambiguous (and in Isabelle/\HOL executable or 
         animatable) way.
       \item it develops the \emph{theory} of these definitions, \ie, the collection 
         of lemmas and theorems that can be proven from these definitions.
 \item all types in  \FOCL contain the elements \inlineocl{null} and \inlineocl{invalid};
         since this extends to \inlineocl+Boolean+ type, this results
         in a four-valued logic. Consequently,  \FOCL contains
         the derivation of the \emph{logic} of \OCL.
 \item collection types may contain
         \inlineocl{null} (so \inlineocl|Set{null}| is a defined set) but not
         \inlineocl{invalid} (\inlineocl|Set{invalid}| is just
         \inlineocl{invalid}).
 \item Wrt. to the static types,  \FOCL is a strongly typed language in
         the Hindley-Milner tradition.
         We assume that a pre-process for full \OCL eliminates all implicit
         conversions due to subtyping by introducing explicit casts (\eg,
         \inlineocl{oclAsType(Class)}).\footnote{The details of such a 
         pre-processing are  described in~\cite{brucker:interactive:2007}.}
 \item  \FOCL types may be arbitrarily nested. For example,
         the expression
         \inlineocl|Set{Set{1,2}} = Set{Set{2,1}}| is legal and true.
 \item  \FOCL types may be higher-order nested. For example,
         the expression \inlineocl|\<lambda> X. Set{X} = Set{Set{2,1}}| is legal.
         Higher-order pattern-matching can be easily extended following 
         the principles in the \HOL library, which can be applied also to \FOCL types.
 \item All objects types are represented in an object universe\footnote{following
         the tradition of \HOL-\OCL~\cite{brucker.ea:extensible:2008-b}}.
         The universe construction also gives semantics to type casts, dynamic type
         tests, as well as functions such as \inlineocl{allInstances()},
         or \inlineocl{oclIsNew()}. The object universe construction is
         conceptually described and demonstrated at an example.
 \item As part of the \OCL logic,  \FOCL develops the theory of
         equality in \UML/\OCL. This includes the standard equality, which is a
         computable strict equality using the object references for comparison,
         and the not necessarily computable logical equality, which expresses
         the Leibniz principle that `equals may be replaced by equals' in
         \OCL terms. 
 \item Technically,  \FOCL is a \emph{semantic embedding} into a
         powerful semantic meta-language and
         environment, namely Isabelle/\HOL~\cite{nipkow.ea:isabelle:2002}.
         It is a so-called \emph{shallow embedding} in \HOL; this means that types
         in \OCL were mapped one-to-one to types in Isabelle/\HOL.
         Ill-typed \OCL specifications can therefore not be represented in
          \FOCL and a type in  \FOCL contains exactly
         the values that are possible in \OCL\@.
% \item It supports equational reasoning and congruence reasoning, but
%         this requires a differentiation of the different equalities like
%         strict equality, strong equality, meta-equality (HOL). Strict
%         equality and strong equality require a subcalculus, ``cp'' (a
%         detailed discussion of the different equalities as well as the
%         subcalculus ``cp''---for three-valued \OCL 2.0---is given
%         in~\cite{brucker.ea:semantics:2009}), which is nasty but can be
%         hidden from the user inside tools.
\end{itemize}

\paragraph*{Context.} This document stands in a more than fifteen years
tradition of giving a formal semantics to the core of \UML and its
annotation language \OCL, starting from \citet{richters:precise:2002}
and~\cite{hamie.ea:reflections:1998,mandel.ea:ocl:1999,cook.ea::amsterdam:2002},
leading to a number of formal, machine-checked versions, most notably
\HOL-\OCL~\cite{brucker.ea:semantic:2006-b,brucker:interactive:2007,brucker.ea:hol-ocl-book:2006,brucker.ea:extensible:2008-b}
and more recent approaches~\cite{brucker.ea:path-expressions:2013}. All
of them have in common the attempt to reconcile the conflicting
demands of an industrially used specification language and its various
stakeholders, the needs of OMG standardization process and the desire
for sufficient logical precision for tool-implementors, in particular
from the Formal Methods research community.  To discuss the future
directions of the standard, several \OCL experts met in November 2013
in Aachen to discuss possible mid-term improvements of \OCL,
strategies of standardization of \OCL within the OMG, and a vision for
possible long-term developments of the
language~\cite{brucker.ea:summary-aachen:2013}. The participants
agreed that future proposals for a formal semantics should be
machine-check, to ensure the absence of syntax errors, the consistency
of the formal semantics, as well as provide a a suite of corner-cases
relevant for \OCL tool implementors.

\paragraph*{Organization of this document.}
This document is organized as follows. After a brief background section
introducing a running example and basic knowledge on Isabelle/\HOL and its formal
notations, we present the formal semantics of  \FOCL introducing:
\begin{enumerate}
\item A conceptual description of the formal semantics, highlighting the essentials
      and avoiding the definitions in detail.
\item A detailed formal description. This covers:
\begin{enumerate}
\item \OCL Types and their presentation in Isabelle/\HOL,
\item \OCL Terms, \ie, the semantics of library operators,
        together with definitions, lemmas, and test cases for the implementor,
\item \UML/\OCL Constructs, \ie, a core of \UML class models plus user-defined
        constructions on them such as class-invariants and operation contracts.
\end{enumerate}
\item Since the latter, \ie, the construction of \UML class models, has to be done on the meta-level
(so not \emph{inside} \HOL, rather on the level of a pre-compiler), we will describe this process
with two larger examples, namely formalizations of our running example.
\end{enumerate}


%A.1 Object Models
%In this sub clause, the notion of an object model is formally defined.
%An object model provides the context for \OCL expressions and constraints.
%A precise understanding of object models is required before a formal
%definition of \OCL expressions can be given. Sub clause A.1.1 proceeds with a
%formal definition of the syntax of object models. The semantics of object
%models is defined in sub clause A.1.2. This sub clause also defines the
%notion of system states as snapshots of a running system.

\section{Background}
\isatagafp
\subsection{A Running Example for \UML/\OCL}
\label{sec:guidedtour}
The Unified Modeling Language
(\UML)~\cite{omg:uml-infrastructure:2011,omg:uml-superstructure:2011}
comprises a variety of model types for describing static (\eg, class
models, object models) and dynamic (\eg, state-machines, activity
graphs) system properties.
\begin{figure*}
  \centering\scalebox{1}{\includegraphics{figures/AbstractSimpleChair}}%
  \caption{A simple \UML class model representing a conference
    system for organizing conference sessions: persons can
    participate, in different roles, in a session. \label{fig:uml}}
\end{figure*}
One of the more prominent model types of the \UML is the
\emph{class model} (visualized as \emph{class diagram}) for modeling
the underlying data model of a system in an object-oriented manner. As
a running example, we model a part of a conference management
system. Such a system usually supports the conference organizing
process, \eg, creating a conference Website, reviewing submissions,
registering attendees, organizing the different sessions and tracks,
and indexing and producing the resulting proceedings. In this example,
we constrain ourselves to the process of organizing conference
sessions; \autoref{fig:uml} shows the class model.  We model the
hierarchy of roles of our system as a hierarchy of classes (\eg,
\inlineocl{Hearer}, \inlineocl{Speaker}, or \inlineocl{Chair}) using
an \emph{inheritance} relation (also called \emph{generalization}). In
particular, \emph{inheritance} establishes a \emph{subtyping}
relationship, \ie, every \inlineocl{Speaker} (\emph{subclass}) is also
a \inlineocl{Hearer} (\emph{superclass}).

A class does not only describe a set of \emph{instances} (called
\emph{objects}), \ie, record-like data consisting of \emph{attributes}
such as \inlineocl{name} of class \inlineocl{Session}, but also
\emph{operations} defined over them. For example, for the class
\inlineocl{Session}, representing a conference session, we model an
operation \inlineocl{findRole(p:Person):Role} that should return the
role of a \inlineocl{Person} in the context of a specific session;
later, we will describe the behavior of this operation in more detail
using \UML\@. In the following, the term object describes a
(run-time) instance of a class or one of its subclasses.

Relations between classes (called \emph{associations} in \UML)
can be represented in a class diagram by connecting lines, \eg,
\inlineocl{Participant} and \inlineocl{Session} or \inlineocl{Person}
and \inlineocl{Role}. Associations may be labeled by a particular
constraint called \emph{multiplicity}, \eg, \inlineocl+0..*+ or
\inlineocl+0..1+, which means that in a relation between participants
and sessions, each \inlineocl{Participant} object is associated to at
most one \inlineocl{Session} object, while each \inlineocl{Session}
object may be associated to arbitrarily many \inlineocl{Participant}
objects. Furthermore, associations may be labeled by projection
functions like \inlineocl{person} and \inlineocl{role}; these implicit
function definitions allow for \OCL-expressions like
\inlineocl+self.person+, where \inlineocl+self+ is a variable of the
class \inlineocl{Role}. The expression \inlineocl+self.person+ denotes
persons being related to the specific object \inlineocl{self} of
type role. A particular feature of the \UML are \emph{association
  classes} (\inlineocl{Participant} in our example) which represent a
concrete tuple of the relation within a system state as an object;
\ie, associations classes allow also for defining attributes and
operations for such tuples. In a class diagram, association classes
are represented by a dotted line connecting the class with the
association. Associations classes can take part in other associations.
Moreover, \UML supports also $n$-ary associations (not shown in
our example).

We refine this data model using the Object Constraint Language (\OCL)
for specifying additional invariants, preconditions and postconditions
of operations. For example, we specify that objects of the class
\inlineocl{Person} are uniquely determined by the value of the
\inlineocl{name} attribute and that the attribute \inlineocl{name} is
not equal to the empty string (denoted by \inlineocl{''}):
\begin{ocl}
context Person
  inv: name <> '' and
       Person::allInstances()->isUnique(p:Person | p.name)
\end{ocl}
Moreover, we specify that every session has exactly one chair by the
following invariant (called \inlineocl{onlyOneChair}) of the class
\inlineocl{Session}:
\begin{ocl}
context Session
  inv onlyOneChair: self.participants->one( p:Participant |
                                      p.role.oclIsTypeOf(Chair))
\end{ocl}
where \inlineocl{p.role.oclIsTypeOf(Chair)} evaluates to true, if
\inlineocl{p.role} is of \emph{dynamic type}
\inlineocl{Chair}. Besides the usual \emph{static types} (\ie, the
types inferred by a static type inference), objects in \UML and other
object-oriented languages have a second \emph{dynamic} type concept.
This is a consequence of a family of \emph{casting functions} (written
$\typeCast{o}{C}$ for an object $o$ into another class type $C$) that
allows for converting the static type of objects along the class
hierarchy. The dynamic type of an object can be understood as its
``initial static type'' and is unchanged by casts. We complete our
example by describing the behavior of the operation
\inlineocl{findRole} as follows:
\begin{ocl}
context Session::findRole(person:Person):Role
  pre:  self.participates.person->includes(person)
  post: result=self.participants->one(p:Participant |
                                p.person = person ).role
        and self.participants = self.participants@pre
        and self.name = self.name@pre
\end{ocl}
where in post-conditions, the operator \inlineocl{@pre} allows for
accessing the previous state. Note that:
\begin{ocl}
  pre:  self.participates.person->includes(person)
\end{ocl}
is actually a syntactic abbreviation for a contraint referring to
the previous state:
\begin{ocl}
        self.participates@pre.person@pre->includes(person).
\end{ocl}
Note, further, that conventions for full-\OCL permit the suppression
of the \inlineocl$self$-parameter, following similar syntactic conventions
in other object-oriented languages such as Java:
\begin{ocl}
context Session::findRole(person:Person):Role
  pre:  participates.person->includes(person)
  post: result=participants->one(p:Participant |
                                p.person = person ).role
        and participants = participants@pre
        and name = name@pre
\end{ocl}


In \UML, classes can contain attributes of the type of the
defining class.  Thus, \UML can represent (mutually) recursive
datatypes. Moreover, \OCL introduces also recursively specified
operations.

A key idea of defining the semantics of \UML and extensions like
SecureUML~\cite{brucker.ea:transformation:2006} is to translate the
diagrammatic \UML features into a combination of more elementary
features of \UML and \OCL
expressions~\cite{gogolla.ea:expressing:2001}. For example,
associations (\ie, relations on objects) can be implemented in
specifications at the design level by aggregations, \ie, collection-valued 
class attributes together with \OCL constraints expressing the
multiplicity. Thus, having a semantics for a subset of \UML and \OCL is
tantamount for the foundation of the entire method.
\endisatagafp



\subsection{Formal Foundation}

\subsubsection{A Gentle Introduction to Isabelle}
Isabelle~\cite{nipkow.ea:isabelle:2002} is a \emph{generic} theorem
prover. New object logics can be introduced by specifying their syntax
and natural deduction inference rules. Among other logics, Isabelle
supports first-order logic, Zermelo-Fraenkel set theory and the
instance for Church's higher-order logic (HOL).

The core language of Isabelle is a typed $\lambda$-calculus providing
a uniform term language $T$ in which all logical entities where
represented:\footnote{In the Isabelle implementation, there are
  actually two further variants which were irrelevant for this
  presentation and are therefore omitted.}
\begin{gather*}
   T~~ ::=~~ C~~ |~~ V ~~|~~ \lambda~V.~~ T ~~|~~ T~T
\end{gather*}
where:
\begin{itemize}
\item $C$ is the set of \emph{constant symbols}
      like "$\operatorname{fst}$" or "$\operatorname{snd}$" as operators on pairs. Note that
       Isabelle's syntax engine supports mixfix-notation for terms: 
       "$(\_ \Longrightarrow \_)~A~B$" or  "$(\_ + \_)~A~B$" 
       can be parsed and printed as 
       "$A \Longrightarrow B$" or  "$A + B$", respectively.
\item $V$ is the set of \emph{variable symbols} like "$x$", "$y$", "$z$", \ldots
      Variables standing in the scope of a $\lambda$-operator were called
      \emph{bound} variables, all others are \emph{free} variables.
\item "$\lambda~V.~~T$" is called $\lambda$-abstraction. For example, consider the
       identity function $\lambda~x. x$.
       A $\lambda$-abstraction forms a scope for the variable $V$.
\item $T~T'$ is called an \emph{application}.  
\end{itemize}
These concepts are not at all Isabelle specific and can be found in many modern programming
languages ranging from Haskell over Python to Java.

Terms where associated to \emph{types} by a set of \emph{type
  inference rules}\footnote{Similar to
\url{https://en.wikipedia.org/w/index.php?title=Hindley\%E2\%80\%93Milner_type_system&oldid=668548458}}; only
terms for which a type can be inferred---\ie, for \emph{typed
  terms}---were considered as legal input to the Isabelle
system. The type-terms $\tau$ for $\lambda$-terms are defined
as:\footnote{Again, the Isabelle implementation is actually slightly
  different; our presentation is an abstraction in order to improve
  readability.}
\begin{gather}
\tau~~ ::=~~ TV~~ |~~ TV :: \Xi~~ |~~ \tau~\Rightarrow~\tau~~ |~~ (\tau, \ldots, \tau)TC  
\end{gather}
\begin{itemize}
\item $TV$ is the set of \emph{type variables} like $'\alpha$,
  $'\beta$, \ldots
  The syntactic categories $V$ and $TV$ are disjoint; thus,
  $'x$ is a perfectly possible type variable.
\item $\Xi$ is a set of \emph{type-classes} like \emph{ord},
  \emph{order}, \emph{linorder}, \ldots
  This feature
  in the Isabelle type system is inspired by Haskell type classes.\footnote{See \url{https://en.wikipedia.org/w/index.php?title=Type_class&oldid=672053941}.}
  A \emph{type class constraint} such as "$\alpha::\operatorname{order}$" expresses that
  the type variable $'\alpha$ may range over any type that has the algebraic
  structure of a partial ordering (as it is configured in the Isabelle/\HOL library).
\item The type  $'\alpha \Rightarrow '\beta$  denotes the total function space from
  $'\alpha$ to $'\beta$.
\item $TC$ is a set of \emph{type constructors} like "$('\alpha)\operatorname{list}$" or
  "$('\alpha)\operatorname{tree}$". Again, Isabelle's syntax engine supports mixfix-notation 
  for type terms: cartesian products $'\alpha \times '\beta $ or type sums 
  $'\alpha + '\beta $ are notations for $('\alpha,'\beta)(\_ \backslash<\operatorname{times}> \_)$ or 
  $('\alpha,'\beta)(\_ + \_)$, respectively. Also null-ary type-constructors like 
  $()\operatorname{bool}$,$()\operatorname{nat}$ and $()\operatorname{int}$ are possible;
  note that the parentheses of null-ary type constructors are usually omitted.
\end{itemize}

Isabelle accepts also the notation $t :: \tau$ as type assertion in
the term-language; $t :: \tau$ means "t is required to have type
$\tau$". Note that typed terms \emph{can} contain free variables;
terms like $x + y = y + x$ reflecting common mathematical notation
(and the convention that free variables are implicitly universally
quantified) are possible and common in Isabelle
theories.\footnote{Here, we assume that $\_ + \_$ and $\_ = \_$ are
  declared constant symbols having type
  $\operatorname{int} \Rightarrow \operatorname{int} \Rightarrow
  \operatorname{int}$
  and $'\alpha \Rightarrow '\alpha \Rightarrow \operatorname{bool}$,
  respectively.}.


An environment providing $\Xi$, $TC$ as well as a map from constant
symbols $C$ to types (built over these $\Xi$ and $TC$) is called a
\emph{global context}; it provides a kind of signature, \ie, a
mechanism to construct the syntactic material of a logical theory.

The most basic (built-in) global context of Isabelle provides just a
language to construct logical rules. More concretely, it provides a
constant declaration for the (built-in) \emph{meta-level implication}
$\_ \Implies \_$ allowing to form constructs like
$A_1 \Implies \cdots \Implies A_n \Implies A_{n+1}$, which are viewed
as a \emph{rule} of the form ``from assumptions $A_1$ to $A_n$, infer
conclusion $A_{n+1}$'' and which is written in Isabelle syntax as
\begin{gather}
  \semantics{A_1 ; \ldots; A_n}\Implies A_{n+1}
  \qquad
  \text{or, in mathematical notation,}
  \quad
  \begin{prooftree}
    A_1 \qquad \cdots \qquad A_n
    \justifies
    A_{n+1}
    \ptmi{.}
  \end{prooftree}
\end{gather}
Moreover, the built-in meta-level quantification $\operatorname{Forall} (\lambda~x.~E~x)$
(pretty-printed and parsed as $\Forall x\spot E~x$) captures
the usual side-constraints ``$x$ must not occur free in the
assumptions'' for quantifier rules; meta-quantified variables can be
considered as ``fresh'' free variables. Meta-level quantification
leads to a generalization of Horn-clauses of the form:
\begin{gather}
\Forall x_1, \ldots, x_m\spot \semantics{A_1 ; \ldots; A_n}\Implies
A_{n+1}\mi{.}
\end{gather}

Isabelle supports forward- and backward reasoning on rules.  For
backward-reasoning, a \emph{proof-state} can be initialized in a given 
global context and further transformed into others. For example, a proof of $\phi$, using
the Isar~\cite{wenzel:isabelleisar:2002} language, will look as
follows in Isabelle:
\begin{gather}
  \begin{array}{l}
    \Lemma{label} \phi\\
    \quad\apply{case\_tac}\\
    \quad\apply{simp\_all}\\
  \done
  \end{array}
\end{gather}
This proof script instructs Isabelle to prove $\phi$ by case
distinction followed by a simplification of the resulting proof state.
Such a proof state is an implicitly conjoint sequence of generalized
Horn-clauses (called \emph{subgoals}) $\phi_1$, \ldots,$\phi_n$ and a
\emph{goal} $\phi$. Proof states were usually denoted by:
\begin{gather}
\begin{array}{rl}
\pglabel{label}:& \phi \\
 1.& \phi_1 \\
    &\vdots \\
 n.& \phi_n\\
\end{array}
\end{gather}
Subgoals and goals may be extracted from the proof state into theorems
of the form $\semantics{\phi_1 ; \ldots; \phi_n}\Implies \phi$ at any
time;
% ; this mechanism helps to generate test theorems.  
% Further, Isabelle supports meta-variables (written $\meta{x}, \meta{y},
% \ldots$), which can be seen as ``holes in a term'' that can still be
% substituted. Meta-variables are instantiated by Isabelle's built-in
% higher-order unification.

By extensions of global contexts with axioms and proofs of theorems,
\emph{theories} can be constructed step by step. Beyond the basic
mechanisms to extend a global context by a type-constructor-, type-class-
constant-definition or an axiom, Isabelle offers a number of 
\emph{commands} that allow for more complex extensions of theories in
a logically safe way (avoiding the use of axioms directly).

\subsubsection{Higher-order Logic (HOL)}
\emph{Higher-order logic}
(HOL)~\cite{church:types:1940,andrews:introduction:2002} is a
classical logic based on a simple type system. Isabelle/\HOL is
a theory extension of the basic Isabelle core-language with
operators and the 7 axioms of HOL; together with large libraries
this constitutes an implementation of HOL. 
Isabelle/\HOL provides the usual
logical connectives like $\_ \land \_$, $\_ \implies\_$, $\lnot \_ $
as well as the object-logical quantifiers $\forall x\spot P\ap x$ and
$\exists x\spot P\ap x$; in contrast to first-order logic, quantifiers
may range over arbitrary types, including total functions
$f\ofType\alpha \Rightarrow \beta$. HOL is centered around
extensional equality $\_ = \_ \ofType \alpha \Rightarrow \alpha
\Rightarrow \text{bool}$. Extensional equality means that two functions $f$ and $g$
are equal if and only if they are point-wise equal; this is captured by the rule:
$(\Forall~x\spot f~x = g~x) \Longrightarrow f = g$.
HOL is more expressive than first-order
logic, since, among many other things, induction schemes can be expressed inside the
logic. For example, the standard induction rule on natural numbers in HOL:
\begin{gather*}
  P~0 \Longrightarrow (\Forall~x\spot P~x \Longrightarrow P~(x+1)) \Longrightarrow P~x
\end{gather*}
is just an ordinary rule in Isabelle which is in fact a proven theorem
in the theory of natural numbers. This example exemplifies an important
design principle of Isabelle: theorems and rules are technically the
same, paving the way to \emph{derived rules} and automated 
decision procedures based on them. This has the consequence that
that these procedures are consequently sound by construction
with respect to their logical aspects (they may be incomplete
or failing, though).

On the other hand, Isabelle/\HOL can also be viewed as a functional programming language
like SML or Haskell. Isabelle/\HOL definitions can usually be 
read just as another functional \textbf{programming} language;
if not interested in proofs and the possibilities of a 
\textbf{specification} language providing
powerful logical quantifiers or equivalent free variables, 
the reader can just ignore these aspects in theories.

%Isabelle/HOL is a logical embedding of HOL into Isabelle.  The
%(original) simple-type system underlying HOL has been extended by
%Hindley-Milner style polymorphism with type-classes similar to
%Haskell.  
%While Isabelle/HOL is usually seen as proof assistant, we
%use it as symbolic computation environment. Implementations on top of
%Isabelle/HOL can re-use existing powerful deduction mechanisms such as
%higher-order resolution, tableaux-based reasoners, rewriting
%procedures, Presburger arithmetic, and via various integration
%mechanisms, also external provers such as
%Vampire~\cite{riazanov.ea:vampire:1999} and the SMT-solver
%Z3~\cite{moura.ea:z3:2008}.

Isabelle/\HOL offers support for a particular methodology to extend
given theories in a logically safe way: A theory-extension is
\emph{conservative} if the extended theory is consistent provided that
the original theory was consistent.  Conservative extensions can be
\emph{constant definitions}, \emph{type definitions}, \emph{datatype
  definitions}, \emph{primitive recursive definitions} and
\emph{well founded recursive definitions}.

For instance, the library includes the type constructor $\up{\tau} :=
\isasymbottom ~ | ~ \lift{\_} : \alpha$ that assigns to each type
$\tau$ a type $\up{\tau}$ \emph{disjointly extended} by the
exceptional element $\isasymbottom$. The function $\drop{\_} :
\up{\alpha} \to \alpha$ is the inverse of $\lift{\_}$ (unspecified for
$\isasymbottom$). Partial functions $\alpha \isasymrightharpoonup
\beta$ are defined as functions $\alpha \isasymRightarrow \up{\beta}$
supporting the usual concepts of domain ($\dom\;\_$) and range
($\ran\;\_$).

As another example of a conservative extension, typed sets were built
in the Isabelle libraries conservatively on top of the kernel of HOL
as functions to $\HolBoolean$; consequently, the constant definitions
for membership is as follows:\footnote{To increase readability, we use
  a slightly simplified presentation.}
\begin{gather}
  \begin{array}{lrll}
    \types& \alpha \HolSet            &= \alpha \Rightarrow \HolBoolean\\[.5ex]
    \isardef &\operatorname{Collect}&\ofType (\alpha \Rightarrow
     \HolBoolean) \Rightarrow \HolSet{\alpha}  &\qquad\text{--- set comprehension}\\
    \where &\operatorname{Collect}\ap S      &\equiv S\\[.5ex]
     \isardef &\operatorname{member}           &\ofType \alpha \Rightarrow
     \alpha \Rightarrow \HolBoolean &\qquad\text{---
       membership test}\\
     \where &\operatorname{member}\ap s\ap S &\equiv S s\\
  \end{array}
\end{gather}
Isabelle's syntax engine is instructed to accept the notation
$\{x \mid P\}$ for $\operatorname{Collect}\ap\lambda x\spot P$ and the
notation $s \in S$ for $\operatorname{member}\ap s\ap S$. As can be
inferred from the example, constant definitions are axioms that
introduce a fresh constant symbol by some non-recursive expressions not 
containing free variables; this type of axiom is logically safe since it works
like an abbreviation. The syntactic side conditions of this axiom are
mechanically checked. It is straightforward to express the
usual operations on sets like $\_ \cup \_,
\_\cap\_\ofType\HolSet{\alpha} \Rightarrow \HolSet{\alpha} \Rightarrow
\HolSet{\alpha}$ as conservative extensions, too, while the rules of
typed set theory were derived by proofs from these definitions.

Similarly, a logical compiler is invoked for the following statements 
introducing the types option and list:
\begin{gather}
  \begin{array}{lrll}
    \datatype & \HolOption       &= \HolNone \mid \HolSome{\alpha}\\[.5ex]
    \datatype & \HolList{\alpha} &= \operatorname{Nil} \mid
    \operatorname{Cons}\ap a\ap l
  \end{array}
\end{gather}
Here, $[]$ or $a\#l$ are an alternative syntax for $\operatorname{Nil}$
or $\operatorname{Cons}\ap a ~l$; moreover, $[a, b, c]$ is defined as
alternative syntax for $a\#b\#c\#[]$. These (recursive) statements
were internally represented in by internal type and constant
definitions. Besides the \emph{constructors} $\HolNone$, $\HolSome$,
$[]$ and $\operatorname{Cons}$, there is the match operation
\begin{gather}
\HolCase\ap x\ap\HolOf~\HolNone \isasymRightarrow F\ap \mid
\HolSome{a} \isasymRightarrow G\ap a
\end{gather}
respectively
\begin{gather}
\HolCase\ap x\ap\HolOf~[] \isasymRightarrow F\ap \mid \operatorname{Cons}\ap a\ap
r \isasymRightarrow G\ap a\ap r\mi{.}
\end{gather}
From the internal definitions (not shown here) several properties were
automatically derived. We show only the case for lists:
\begin{gather}\label{eq:datatype-rules}
  \begin{array}{ll}
    (\HolCase\ap[]\ap\HolOf\ap[] \Rightarrow F  \ap | \ap  (a\#r) \Rightarrow
    G\ap a\ap r) = F &\\
    (\HolCase \ap  b\#t  \ap \HolOf  \ap [] \Rightarrow F  \ap  | \ap
    (a\#r) \Rightarrow G\ap a\ap r) = G~b~t &\\ %
    \mbox{}[] \neq a\#t    &\text{-- distinctness} \\
    \semantics{a = [] \implies P ; \exists~x~t\spot  a = x\#t \implies P } \Longrightarrow P &\text{-- exhaust} \\
    \semantics{P~[] ; \forall~at\spot  P~t \implies P (a\#t) } \Longrightarrow P~x      &\text{-- induct}
  \end{array}
\end{gather}
Finally, there is a compiler for primitive and well founded recursive
function definitions. For example, we may define the
$\operatorname{sort}$ operation on linearly ordered lists by:
\begin{gather}\label{eq:sortdef}
  \begin{array}{lll}
    \fun
    &\enspace\operatorname{ins} & \ofType
    [\alpha\ofType\mathrm{linorder}, \HolList{\alpha}]
    \Rightarrow
    \HolList{\alpha}\\
    \where
    &\enspace \operatorname{ins}\ap x \ap  [\;] &= [x]\\
    &\enspace \operatorname{ins}\ap x \ap (y\#\mathit{ys})&=
    \HolIf x < y
    \HolThen x\#  y \# ys
    \HolElse y\#(\operatorname{ins} \ap x \ap ys)
 \end{array}\\
  \begin{array}{lll}
    \fun
    &\enspace\operatorname{sort} & \ofType
    \HolList{(\alpha\ofType\mathrm{linorder})}
    \Rightarrow
    \HolList{\alpha}\\
    \where
    &\enspace \operatorname{sort}\ap [\;] &= [\;]\\
    &\enspace \operatorname{sort} (x\#\mathit{xs})&=
    \operatorname{ins}\ap x\ap (\operatorname{sort}\ap xs)
   \end{array}
\end{gather}
The internal (non-recursive) constant definition for these operations
is quite involved; however, the logical compiler will finally derive
all the equations in the statements above from this definition and
make them available for automated simplification.

Thus, Isabelle/\HOL also provides a large collection of theories like
sets, lists, orderings, and various arithmetic theories
which only contain rules derived from conservative definitions. 
This library constitutes a comfortable basis for defining the OCL
library and language constructs.

In particular, Isabelle manages a set of \emph{executable types and
  operators}, \ie, types and operators for which a compilation to
SML, OCaml or Haskell is possible. Setups for arithmetic types
such as $\text{int}$ have been done; moreover any datatype and any
recursive function were included in this executable set (providing
that they only consist of executable operators). This forms the 
basis that many OCL terms can be executed directly.
Using the value command, it is possible to compile many OCL ground expressions
(no free variables) to code and to execute them; for example
\inlineisar$value "3 + 7"$ just answers with \inlineisar$10$ in Isabelle's 
output window. This is even true for many expressions containing types which
in themselves are not executable. For example, the Set type, which is 
defined in Featherweight OCL as the type of potentially infinite sets,
is consequently not in itself executable; however, due to special setups
of the code-generator, expressions like \inlineisar$value "Set{1,2}"$ are,
because the underlying constructors in this expression allow for automatically 
establishing that this set is finite and reducible to constructs that \emph{are}
in this special case executable.


% Similarly, Isabelle
%manages a large set of (higher-order) rewrite rules into which
%recursive function definitions were included. Provided that this
%rule set represents a terminating and confluent rewrite system, the
%Isabelle simplifier provides also a highly potent decision procedure
%for many fragments of theories underlying the constraints to be
% processed when constructing test theorems.

\subsection{How this Annex A was Generated from Isabelle/HOL Theories}
\begin{figure*}[tb]
  \mbox{}\hfill
  \subfloat%
  [The Isabelle jEdit environment. ]%
  {\label{fig:jedit} \includegraphics[height=6.2cm]{jedit}}%
  \hfill%
  \hfill%
    \subfloat[The generated formal document.]%
    {\label{fig:pdf} \includegraphics[height=6.2cm]{pdf}}
    \hfill\mbox{}
  \caption{Generating documents with guaranteed  syntactical and
    semantical consistency.}
  \label{fig:gener-docum-where}
\end{figure*}
Isabelle, as a framework for building formal
tools~\cite{wenzel.ea:building:2007}, provides the means for
generating \emph{formal documents}.  With formal documents (such as
the one you are currently reading) we refer to documents that are
machine-generated and ensure certain formal guarantees. In particular,
all formal content (\eg, definitions, formulae, types) are checked for
consistency during the document generation.

For writing documents, Isabelle supports the embedding of informal
texts using a \LaTeX-based markup language within the theory files. To
ensure the consistency, Isabelle supports to use, within these
informal texts, \emph{antiquotations} that refer to the formal parts
and that are checked while generating the actual document as
PDF\@. For example, in an informal text, the antiquotation
\inlineisar|@{$\text{thm}$ "not_not"}| will instruct Isabelle to
lock-up the (formally proven) theorem of name \inlineisar"ocl_not_not"
and to replace the antiquotation with the actual theorem, \ie,
\inlineocl{not (not x) $=$ x}.

\autoref{fig:gener-docum-where}
illustrates this approach: \autoref{fig:jedit} shows the jEdit-based
development environment of Isabelle with an excerpt of one of the core
theories of \FOCL\@. \autoref{fig:pdf} shows the generated
PDF document where all antiquotations are replaced. Moreover,
the document generation tools allows for defining syntactic sugar as
well as skipping technical details of the formalization.

\isatagannexa
Thus, applying the  \FOCL approach to writing an updated
Annex A that provides a formal semantics of the most fundamental
concepts of \OCL ensures
\begin{enumerate}
\item that all formal context is syntactically correct and well-typed,
  and
\item all formal definitions and the derived logical rules are
  semantically consistent.
\end{enumerate}
% Overall, this would contribute to one of the main goals of the \OCL 2.5
% RFP, as discussed at the \OCL meeting in
% Aachen~\cite{brucker.ea:summary-aachen:2013}.
\endisatagannexa
\isatagafp
Featherweight OCL is a formalization of the core of OCL
aiming at formally investigating the relationship between the
various concepts. At present, it does not attempt to define the complete
OCL library. Instead, it concentrates on the core concepts of
OCL as well as the types \inlineocl{Boolean},
\inlineocl{Integer}, and typed sets (\inlineocl|Set(T)|).  Following
the tradition of
HOL-OCL~\cite{brucker.ea:hol-ocl:2008,brucker.ea:hol-ocl-book:2006},
Featherweight OCL is based on the following principles:
\begin{enumerate}
\item It is an embedding into a powerful semantic meta-language and
  environment, namely
  Isabelle/HOL~\cite{nipkow.ea:isabelle:2002}.
\item It is a \emph{shallow embedding} in HOL; types
  in OCL were injectively mapped to types in Featherweight
  OCL\@. Ill-typed OCL specifications cannot be represented in
  Featherweight OCL and a type in Featherweight OCL contains exactly
  the values that are possible in OCL\@. Thus, sets may contain
  \inlineocl{null} (\inlineocl|Set{null}| is a defined set) but not
  \inlineocl{invalid} (\inlineocl|Set{invalid}| is just
  \inlineocl{invalid}).
\item Any Featherweight OCL type contains at least
  \inlineocl{invalid} and \inlineocl{null} (the type \inlineocl{Void}
  contains only these instances). The logic is consequently
  four-valued, and there is a \inlineocl{null}-element in the type
  \inlineocl{Set(A)}.
\item It is a strongly typed language in the Hindley-Milner tradition.
  We assume that a pre-process eliminates all implicit conversions due
  to sub-typing by introducing explicit casts (\eg,
  \inlineocl{oclAsType()}). The details of such a pre-processing are
  described in~\cite{brucker:interactive:2007}.  Casts are semantic
  functions, typically injections, that may convert data between the
  different Featherweight OCL types.
\item All objects are represented in an object universe in the HOL-OCL
  tradition~\cite{brucker.ea:extensible:2008-b}. The universe
  construction also gives semantics to type casts, dynamic type
  tests, as well as functions such as \inlineocl{oclAllInstances()},
  or \inlineocl{oclIsNew()}.
\item Featherweight OCL types may be arbitrarily nested. For example,
  the expression
  \inlineocl|Set{Set{1,2}} = Set{Set{2,1}}| is legal and true.
\item For demonstration purposes, the set type in Featherweight OCL
  may be infinite, allowing infinite quantification and a constant
  that contains the set of all Integers.  Arithmetic laws like
  commutativity may therefore be expressed in OCL itself.  The
  iterator is only defined on finite sets.
\item It supports equational reasoning and congruence reasoning, but
  this requires a differentiation of the different equalities like
  strict equality, strong equality, meta-equality (HOL). Strict
  equality and strong equality require a sub-calculus, ``cp'' (a
  detailed discussion of the different equalities as well as the
  sub-calculus ``cp''---for three-valued OCL 2.0---is given
  in~\cite{brucker.ea:semantics:2009}), which is nasty but can be
  hidden from the user inside tools.
\end{enumerate}
Overall, this would contribute to one of the main goals of the \OCL 2.5
RFP, as discussed at the \OCL meeting in
Aachen~\cite{brucker.ea:summary-aachen:2013}.
\endisatagafp


\section{The Essence of UML-OCL Semantics}
\subsection{The Theory Organization}
The semantic theory is organized in a quite conventional manner in
three layers. The first layer, called the \emph{denotational
  semantics} comprises a set of definitions of the operators of the
language.  Presented as \emph{definitional axioms} inside
Isabelle/\HOL, this part assures the logically consistency of the
overall construction. The denotational definitions of types, constants
and operations, and \OCL contracts represent the ``gold standard'' of the
semantics. The second layer, called \emph{logical layer},
is derived from the former and centered around the notion of validity
of an \OCL formula $P$. For a state-transition from pre-state $\sigma$
to post-state $\sigma'$, a validity statement is written $(\sigma,
\sigma') \isasymMathOclValid P$. Its major purpose is to logically establish facts
(lemmas and theorems) about the denotational definitions.
The third layer, called \emph{algebraic layer},
also derived from the former layers, tries to establish algebraic laws
of the form $P = P'$; such laws are amenable to equational reasoning
and also help for automated reasoning and code-generation. For an
implementor of an \OCL compiler, these consequences are of most interest.

For space reasons, we will restrict ourselves in this document to a few
operators and make a traversal through all three layers to give a
high-level description of our formalization.  Especially, the details
of the semantic construction for sets and the handling of objects and
object universes were excluded from a presentation here.

\subsection{Denotational Semantics of Types}
The syntactic material for type expressions, called $\text{TYPES}(C)$, is 
inductively defined as follows:
\begin{itemize}
\item $C \subseteq \text{TYPES}(C)$
\item $\text{Boolean}$, $\text{Integer}$, $\text{Real}$, $\text{Void}$, \ldots
      are elements of $\text{TYPES}(C)$
\item $\text{Set}(X)$, $\text{Bag}(X)$, $\text{Sequence}(X)$,  and 
      $\text{Pair}(X,Y)$ (as example for a Tuple-type)
      are in  $\text{TYPES}(C)$ (if $X, Y \in \text{TYPES}(C)$).
\end{itemize}

Types were directly represented in \FOCL by types in \HOL; consequently,
any \FOCL type must provide elements for a bottom element (also denoted $\bot$)
and a null element; this is enforced in Isabelle by a type-class $\TCnull$ that
contains two distinguishable elements $\HolBot$ and $\HolNull$ 
(see \autoref{sec:focl-types} for the details of the construction).

Moreover, the representation mapping from \OCL types to \FOCL is
one-to-one (\ie, injective), and the corresponding \FOCL types were
constructed to represent \emph{exactly} the elements (``no junk, no confusion
  elements'') of their \OCL counterparts. The corresponding \FOCL types were
constructed in two stages: First, a \emph{base type} is constructed whose
carrier set contains exactly the elements of the \OCL type. Secondly, this
base type is lifted to a \emph{valuation} type that we use for type-checking
\FOCL constants, operations, and expressions. The valuation type takes into account
that some \UML-\OCL functions of its \OCL type (namely: accessors in path-expressions)
depend on a pre- and a post-state.

For most base types like $\text{Boolean}_{\text{base}}$ or 
$\text{Integer}_{\text{base}}$, it suffices to double-lift a \HOL library type:
\begin{equation}
\typesynonym \qquad  \text{Boolean}_{\text{base}} \defeq \up{{\up{bool}}}
\end{equation}
As a consequence of this definition of the type, we have the elements
$\isasymbottom, \lift{\isasymbottom}, \lift{\lift{\HolTrue}},
\lift{\lift{\HolFalse}}$ in the carrier-set of  $\text{Boolean}_{\text{base}}$. 
We can therefore use the element$\isasymbottom$ to define the generic type 
class element $\bot$ and $\lift{\bot}$ for the generic type class $\HolNull$.
For collection types and object types this definition
is more evolved (see \autoref{sec:focl-types}).

For object base types, we assume a typed universe $\isaAA$ of objects to be 
discussed later, for the moment we will refer it by its polymorphic variable.

With respect the valuation types for \OCL expression in general and Boolean 
expressions in particular, they depend on the pair $(\sigma, \sigma')$ of 
pre-and post-state. Thus, we define valuation types by the synonym:
\begin{equation}
\typesynonym \qquad  \V{\isaAA}{\alpha} \defeq \state{\isaAA} \times 
                                \state{\isaAA} \to \alpha \ofType \TCnull \mi{.}
\end{equation}
The valuation type for boolean,integer, etc. \OCL terms is therefore defined as:
\begin{gather*}
\typesynonym \qquad \text{Boolean}_{\isaAA} \defeq  \V{\isaAA}{\text{Boolean}_{\text{base}}} \\
\typesynonym \qquad \text{Integer}_{\isaAA} \defeq  \V{\isaAA}{\text{Integer}_{\text{base}}} \\
\ldots
\end{gather*}
the other cases are analogous. In the subsequent subsections, we will drop the 
index $\isaAA$ since it is constant in all formulas and expressions except for 
operations related to the object universe construction in \autoref{sec:universe}

The rules of the logical layer (there are no algebraic rules related to the 
semantics of types), and more details can be found in  \autoref{sec:focl-types}.

\subsection{Denotational Semantics of Constants and Operations}
We use the notation $I\semantics{E}\tau$ for the semantic interpretation 
function as commonly used in mathematical textbooks and the variable $\tau$ 
standing for pairs of pre- and post state $(\sigma, \sigma')$. Note that we will 
also use $\tau$ to denote the \emph{type} of a state-pair; since both syntactic 
categories are independent, we can do so without arising confusion. \OCL 
provides for all \OCL types the constants \mocl{invalid} for the exceptional 
computation result and \mocl{null} for the non-existing value. Thus we define:
\begin{gather*}
\begin{alignedat}{3}
I\semantics{\mocl{invalid}\ofType V(\alpha)} \tau &\equiv \HolBot &
\qquad I\semantics{\mocl{null}\ofType V(\alpha)}  \tau    &\equiv \HolNull\\
\end{alignedat}
\end{gather*}
For the concrete \mocl{Boolean}-type, we define similarly the boolean constants 
$\mocl{true}$ and $\mocl{false}$ as well as the fundamental tests for definedness 
and validity (generically defined for all types):
\begin{gather*}
\begin{alignedat}{3}
I\semantics{\mocl{true}\ofType\mocl{Boolean}} \tau &= \lift{\lift{\HolTrue}} &
\qquad I\semantics{\mocl{false}} \tau &= \lift{\lift{\HolFalse}}\\
\end{alignedat}\\
I\semantics{X\mocl{.oclIsUndefined()}} \tau =
    (\HolIf I\semantics{X}\tau \in \{\HolBot, \HolNull\} \HolThen I\semantics{\mocl{true}}\tau \HolElse I\semantics{\mocl{false}}\tau)\\
 I\semantics{X\mocl{.oclIsInvalid()}} \tau =
    (\HolIf I\semantics{X}\tau = \HolBot \HolThen I\semantics{\mocl{true}}\tau \HolElse I\semantics{\mocl{false}}\tau)
\end{gather*}

For reasons of conciseness, we will write $\delta~X$ for 
$\mocl{not}(X\mocl{.oclIsUndefined())}$ and $\upsilon~X$ for 
$\mocl{not}(X\mocl{.oclIsInvalid())}$ throughout this document.

Due to the used style of semantic representation (a shallow embedding) $I$ is 
in fact superfluous and defined semantically as the identity $\lambda x.~x$; 
instead of:
\begin{gather*}
I\semantics{\mocl{true}\ofType\mocl{Boolean}} \tau = \lift{\lift{\HolTrue}}
\shortintertext{we can therefore write:}
\mocl{true}\ofType\mocl{Boolean}  = \lambda \tau.  \lift{\lift{\HolTrue}}
\end{gather*}
In Isabelle theories, this particular presentation of definitions
paves the way for an automatic check that the underlying equation
has the form of an \emph{axiomatic definition} and is therefore logically safe.

\isatagannexa
Since all operators of the assertion language depend on the context 
$\tau$ = $(\sigma, \sigma')$ and result in values that can be $\isasymbottom$, 
all expressions can be viewed as \emph{evaluations} from $(\sigma, \sigma')$ to 
a type $\alpha$ which must posses a $\bottom$ and a $\text{null}$-element. Given 
that such constraints can be expressed in Isabelle/HOL via \emph{type classes} 
(written: $\alpha::\kappa$), all types for OCL-expressions are of a form captured 
by
\begin{equation*}
 \V{}{\alpha} \defeq \state{} \times \state{} \to \alpha::\{bot,null\}  \mi{,}
 \end{equation*}
where $\state{}$ stands for the system state and $\state{} \times
\state{}$ describes the pair of pre-state and post-state and
$\_\defeq\_$ denotes the type abbreviation.

Previous versions of the OCL semantics~\cite[Annex A]{omg:ocl:2003} used different
interpretation functions for invariants and pre-conditions; we achieve
their semantic effect by a syntactic transformation $\__\text{pre}$
which replaces, for example, all accessor functions
$\getAttrib{\_}{a}$ by their counterparts
$\getAttrib{\_}{a\isasymOclATpre}$ (see \autoref{sec:invlogic}). For example,
$(\getAttrib{\self}{a} > 5)_\text{pre}$ is just
$(\getAttrib{\self}{a\isasymOclATpre} > 5)$. This way, also invariants
and pre-conditions can be interpreted by the same interpretation
function and have the same type of an evaluation $\V{}{\alpha}$.
\endisatagannexa

On this basis, one can define the core logical operators $\mocl{not}$
and $\mocl{and}$ as follows:
\begin{gather*}
  \begin{array}{ll}
    I\semantics{\mocl{not}\; X}  \tau
    &=  (\HolCase I\semantics{X} \tau  \HolOf\\
    &\quad\begin{array}{ll}
                     ~ \bottom                    &\Rightarrow  \bottom \\
                     | \lfloor  \bottom  \rfloor  &\Rightarrow  \lfloor  \bottom  \rfloor  \\
                     | \lfloor \lfloor  x \rfloor \rfloor  &\Rightarrow  \lfloor \lfloor  \lnot  x \rfloor \rfloor )
          \end{array}
  \end{array}
\end{gather*}
\begin{gather*}
  \begin{array}{ll}
   I\semantics{X\;\mocl{and}\; Y}  \tau
    &=  (\HolCase I\semantics{X} \tau  \HolOf\\
    &\quad\begin{array}{ll}
      ~ \bottom                    &\Rightarrow
      (\HolCase I\semantics{Y} \tau  \HolOf\\
      &\quad\begin{array}{ll}
                     ~ \bottom                    &\Rightarrow  \bottom \\
                     | \lfloor  \bottom  \rfloor  &\Rightarrow  \bottom  \\
                     | \lfloor \lfloor  \HolTrue \rfloor \rfloor
                     &\Rightarrow  \bottom\\
                     | \lfloor \lfloor  \HolFalse \rfloor \rfloor
                     &\Rightarrow  \lfloor \lfloor  \HolFalse \rfloor \rfloor )\\
                   \end{array}
      \\
                     | \lfloor  \bottom  \rfloor  &\Rightarrow
      (\HolCase I\semantics{Y} \tau  \HolOf\\
      &\quad\begin{array}{ll}
                     ~ \bottom                    &\Rightarrow
                     \bottom \\
                     | \lfloor  \bottom  \rfloor  &\Rightarrow  \lfloor
                     \bottom \rfloor \\
                     | \lfloor \lfloor  \HolTrue \rfloor \rfloor
                     &\Rightarrow  \lfloor \bottom\rfloor\\
                     | \lfloor \lfloor  \HolFalse \rfloor \rfloor
                     &\Rightarrow  \lfloor \lfloor  \HolFalse \rfloor \rfloor )\\
                   \end{array}
      \\
                     | \lfloor \lfloor  \HolTrue \rfloor \rfloor  &\Rightarrow
      (\HolCase I\semantics{Y} \tau  \HolOf\\
      &\quad\begin{array}{ll}
                     ~ \bottom                    &\Rightarrow
                     \bottom \\
                     | \lfloor  \bottom  \rfloor  &\Rightarrow  \lfloor
                     \bottom \rfloor \\
                     | \lfloor \lfloor y \rfloor \rfloor
                     &\Rightarrow  \lfloor \lfloor  y \rfloor \rfloor )\\
                   \end{array}
      \\
                     | \lfloor \lfloor  \HolFalse \rfloor \rfloor
                     &\Rightarrow   \lfloor \lfloor  \HolFalse \rfloor
                     \rfloor )\\
                   \end{array}\\
\end{array}
\end{gather*}
These non-strict operations were used to define the other logical connectives in 
the usual classical way: $X\; \mocl{or}\; Y \equiv (\mocl{not}\; X)\;
\mocl{and}\; (\mocl{not}\; Y)$ or
$X\;\mocl{implies}\;Y \equiv (\mocl{not}\; X)\;\mocl{or}\; Y$.

The default semantics for an \OCL library operator is strict
semantics; this means that the result of an operation $f$ is
\inlineisar+invalid+ if one of its arguments is \mocl+invalid+ or \mocl+null+.
The definition of the addition for integers as default variant reads as follows:
\begin{gather*}
   \begin{array}{rl}
   I\semantics{x \;\mocl{+}\; y}\tau  = &\HolIf I\semantics{\delta ~ x}\tau =I\semantics{\mocl{true}}\tau
                 \land  I\semantics{\delta  ~ y}\tau =I\semantics{\mocl{true}}\tau \\
                &\HolThen \lfloor \lfloor \lceil \lceil I\semantics{x}\tau \rceil \rceil  + \lceil \lceil I\semantics{y}\tau \rceil \rceil \rfloor \rfloor\\
                &\HolElse \bottom
   \end{array}
\end{gather*}
where the operator ``\mocl{+}'' on the left-hand
side of the equation denotes the \OCL addition of type
$\mocl{Integer} \Rightarrow \mocl{Integer} \Rightarrow \mocl{Integer}$ while 
the ``$+$'' on the right-hand side of the equation of type 
$[\HolInteger,\HolInteger]\Rightarrow \HolInteger$ denotes the integer-addition 
from the HOL library.

\subsection{Logical Layer}
The topmost goal of the logic for OCL is to define the \emph{validity statement}:
\begin{equation*}
   (\sigma, \sigma') \isasymMathOclValid P\mi{,}
\end{equation*}
where $\sigma$ is the pre-state and $\sigma'$ the post-state of the
underlying system and $P$ is a formula, \ie, and \OCL expression of type \mocl{Boolean}.
Informally, a formula $P$ is valid if and only if its evaluation in
$(\sigma, \sigma')$ (\ie, $\tau$ for short) yields true. Formally this means:
\begin{equation*}
\tau \isasymMathOclValid P \equiv \bigl(I\semantics{P} \tau = \lift{\lift{\HolTrue }} \bigr)\mi{.}
\end{equation*}
On this basis, classical, two-valued inference rules can be established for
reasoning over the logical connectives, the different notions of equality,
definedness and validity. Generally speaking, rules over logical validity can
relate bits and pieces in various \OCL terms and allow---via strong
logical equality discussed below---the replacement
of semantically equivalent sub-expressions. The core inference rules are:
\begin{gather*}
\begin{array}{lccr}
  \tau \isasymMathOclValid \mocl{true} &\quad
  \lnot(\tau \isasymMathOclValid \mocl{false})&\quad
  \lnot(\tau \isasymMathOclValid \mocl{invalid})&\quad
  \lnot(\tau \isasymMathOclValid \mocl{null})
\end{array}\\
  \tau \isasymMathOclValid \mocl{not}\; P \Longrightarrow \lnot (\tau \isasymMathOclValid P)\\
\begin{array}{lcr}
  \tau \isasymMathOclValid P \;\mocl{and}\; Q \Longrightarrow \tau \isasymMathOclValid P&\qquad&
  \tau \isasymMathOclValid P \;\mocl{and}\; Q \Longrightarrow \tau \isasymMathOclValid Q \\
  \tau \isasymMathOclValid P \Longrightarrow \tau \isasymMathOclValid P \;\mocl{or}\; Q  &\qquad&
   \tau \isasymMathOclValid Q \tau \Longrightarrow \isasymMathOclValid P \;\mocl{or}\; Q  \\
\end{array}\\
  \tau \isasymMathOclValid P \Longrightarrow
     (\mocl{if}\; P \;\mocl{then}\; B_1 \;\mocl{else}\; B_2 \;\mocl{endif})\tau = B_1\ap \tau\\
  \tau \isasymMathOclValid \mocl{not}\; P \Longrightarrow
       (\mocl{if}\; P \;\mocl{then}\; B_1 \;\mocl{else}\; B_2 \;\mocl{endif})\tau = B_2\ap \tau\\
\begin{array}[lcr]{lcr}
  \tau \isasymMathOclValid P \Longrightarrow \tau \isasymMathOclValid \delta \ap P &\qquad&
  \tau \isasymMathOclValid \delta \ap X \Longrightarrow \tau \isasymMathOclValid \upsilon \ap X
\end{array}
\end{gather*}

By the latter two properties it can be inferred that any valid
property $P$ (so for example: a valid invariant) is defined, which
allows to infer for terms composed by strict operations that their
arguments and finally the variables occurring in it are valid or
defined.

The mandatory part of the \OCL standard refers to an equality
(written \mocl{x = y} or \mocl{x <> y} for its negation), which is
intended to be a strict operation (thus: \mocl{invalid = y} evaluates
  to \mocl{invalid}) and which uses the references of objects in a state
when comparing objects, similarly to C++ or Java. In order to avoid
confusions, we will use the following notations for equality:
\begin{enumerate}
\item The symbol $\_ = \_$ remains to be reserved to the \HOL equality,
      \ie, the equality of our semantic meta-language,
\item The symbol $\_ \isasymMathOclStrongEq \_$ will be used for
      the \emph{strong logical equality},  which follows the general
      logical principle that ``equals can be replaced by equals,''\footnote{Strong logical equality is also referred as ``Leibniz''-equality.}
      and is at the heart of the \OCL logic,
\item The symbol $\_ \isasymMathOclStrictEq \_$ is used for the
      strict referential equality, \ie, the equality the mandatory part
      of the \OCL standard refers to by the \mocl{_ = _}- symbol.
\end{enumerate}

The strong logical equality is a polymorphic
concept which is defined using polymorphism for all \OCL types by:
\begin{gather*}
  I\semantics{X \triangleq  Y}  \tau  \equiv
  \lift {\lift{I\semantics{X}  \tau = I\semantics{Y} \tau  }}
\shortintertext{It enjoys nearly the laws of a congruence:}
\tau \isasymMathOclValid (x \triangleq x)\\
\tau \isasymMathOclValid (x \triangleq y) \Longrightarrow \tau \isasymMathOclValid (y \triangleq x)\\
\tau \isasymMathOclValid (x \triangleq y) \Longrightarrow \tau \isasymMathOclValid (y \triangleq z) \Longrightarrow \tau \isasymMathOclValid (x \triangleq z)\\
\HolOclCp P \Longrightarrow \tau \isasymMathOclValid (x \triangleq y) \Longrightarrow \tau \isasymMathOclValid (P\ap x) \Longrightarrow \tau \isasymMathOclValid (P\ap y)
\end{gather*}
where the predicate $\HolOclCp$ stands for \emph{context-passing}, a
property that is true for all pure \OCL expressions (but not
arbitrary mixtures of \OCL and HOL) in \FOCL\@.  The
necessary side-calculus for establishing $\HolOclCp$ can be fully
automated; the reader interested in the details is referred to
\autoref{sec:equality}.

The strong logical equality of \FOCL give rise to a number
of further rules and derived properties, that clarify the role of strong 
logical equality and the Boolean constants in \OCL specifications:
\begin{gather*}
\tau \isasymMathOclValid \delta \ap x \lor \tau \isasymMathOclValid x \triangleq \mocl{invalid} \lor \tau \isasymMathOclValid x \triangleq \mocl{null} \mi{,}\\
(\tau \isasymMathOclValid A \triangleq \mocl{invalid}) = (\tau \isasymMathOclValid \mocl{not} (\upsilon A))\\
% (*  foundation15 *)
\begin{multlined}
 (\tau \isasymMathOclValid A \triangleq \mocl{true}) = (\tau \isasymMathOclValid A)  \qquad
 (\tau \isasymMathOclValid A \triangleq \mocl{false}) = (\tau \isasymMathOclValid \mocl{not} A) \\
 (\tau \isasymMathOclValid \mocl{not} (\delta x)) = (\lnot \tau \isasymMathOclValid \delta x) \qquad
 (\tau \isasymMathOclValid \mocl{not} (\upsilon x)) = (\lnot \tau \isasymMathOclValid \upsilon x) % (*  UML_Logic.foundation7':*)
\end{multlined}
\end{gather*}
%   (not A \<triangleq> not B) = (A \<triangleq> B) (*foundation21*)

The logical layer of the  \FOCL rules gives also a means
to convert an \OCL formula living in its four-valued world into a
representation that is classically two-valued and can be processed by
standard SMT solvers such as CVC3~\cite{barrett.ea:cvc3:2007} or
Z3~\cite{moura.ea:z3:2008}. $\delta$-closure rules for all logical
connectives have the following format, \eg:
\begin{gather*}
\tau \isasymMathOclValid \delta \ap x \Longrightarrow (\tau \isasymMathOclValid \ap\mocl{not}\ap x) = (\lnot (\tau \isasymMathOclValid x))\\
\tau \isasymMathOclValid \delta \ap x \Longrightarrow \tau \isasymMathOclValid \delta \ap y \Longrightarrow (\tau \isasymMathOclValid x \ap\mocl{and}\ap y) = ( \tau \isasymMathOclValid x \land \tau \isasymMathOclValid y)\\
\begin{multlined}
\tau \isasymMathOclValid \delta \ap x \Longrightarrow  \tau \isasymMathOclValid \delta \ap y \\
\Longrightarrow (\tau \isasymMathOclValid (x \ap\mocl{implies}\ap y)) = ( (\tau \isasymMathOclValid x) \longrightarrow (\tau \isasymMathOclValid y))
\end{multlined}
\end{gather*}
Together with the already mentioned general case-distinction
\begin{gather*}
\tau \isasymMathOclValid \delta \ap x \lor \tau \isasymMathOclValid x \triangleq \mocl{invalid} \lor \tau \isasymMathOclValid x \triangleq \mocl{null}
\end{gather*}
which is possible for any \OCL type, a case distinction on the
variables in a formula can be performed; due to strictness rules,
formulae containing somewhere a variable $x$ that is known to be
$\mocl{invalid}$ or $\mocl{null}$ reduce usually quickly to
contradictions.  For example, we can infer from an invariant $\tau
\isasymMathOclValid x \isasymMathOclStrictEq y \;\mocl{-}\; \mocl{3}$ 
that we have 
$\tau \isasymMathOclValid x \isasymMathOclStrictEq y \;\mocl{-}\; \mocl{3} \land \tau \isasymMathOclValid
\delta \ap x \land \tau \isasymMathOclValid \delta \ap y$.  
We call the latter formula the $\delta$-closure of the former.  Now, we  can 
convert a formula like 
$\tau \isasymMathOclValid x \;\mocl{>}\; \mocl{0} \ap\mocl{or}\ap \mocl{3} \;\mocl{*}\; y \;\mocl{>}\;
x \;\mocl{*}\; x$ into the equivalent formula
$\tau \isasymMathOclValid x \;\mocl{>}\; \mocl{0} \lor \tau
\isasymMathOclValid \mocl{3} \;\mocl{*}\; y \;\mocl{>}\; x \;\mocl{*}\; x$ and 
thus internalize the \OCL-logic into a classical (and more tool-conform) logic. 
This works---for the price of a potential, but due to the usually ``rich''
$\delta$-closures of invariants rare---exponential blow-up of the
formula for all \OCL formulas.

\subsection{Algebraic Layer}
Based on the logical layer, we build a system with simpler rules which
are amenable to automated reasoning. We restrict ourselves to pure
equations on \OCL expressions.

Our denotational definitions on \inlineocl+not+ and \inlineocl+and+
can be re-formulated in the following ground equations:
\begin{gather*}
  \begin{aligned}
  \upsilon\; \mocl{invalid} &= \mocl{false}&\qquad
  \upsilon\; \mocl{null} &= \mocl{true}\\
  \upsilon\; \mocl{true} &= \mocl{true}&\qquad
  \upsilon\; \mocl{false} &= \mocl{true}\\
\end{aligned}\\[.04\baselineskip]
\begin{aligned}
  %
  \delta\; \mocl{invalid} &= \mocl{false}&\qquad
  \delta\; \mocl{null} &= \mocl{false}\\
  \delta\; \mocl{true} &= \mocl{true}&\qquad
  \delta\; \mocl{false} &= \mocl{true}\\
\end{aligned}\\[.04\baselineskip]
\begin{aligned}
  %
  \mocl{not}\; \mocl{invalid} &= \mocl{invalid}&\qquad
  \mocl{not}\; \mocl{null} &= \mocl{null}\\
  \mocl{not}\; \mocl{true} &= \mocl{false}&\qquad
  \mocl{not}\; \mocl{false} &= \mocl{true}\\
\end{aligned}\\[.04\baselineskip]
\begin{aligned}
  %
  (\mocl{null} \;\mocl{and}\; \mocl{true}) &= \mocl{null}&\qquad
  (\mocl{null} \;\mocl{and}\; \mocl{false}) &= \mocl{false}\\
  (\mocl{null} \;\mocl{and}\; \mocl{null}) &= \mocl{null}&\qquad
  (\mocl{null} \;\mocl{and}\; \mocl{invalid}) &= \mocl{invalid}\\
\end{aligned}\\[.04\baselineskip]
\begin{aligned}
  %
  (\mocl{false} \;\mocl{and}\; \mocl{true}) &= \mocl{false}&\qquad
  (\mocl{false} \;\mocl{and}\; \mocl{false}) &= \mocl{false}\\
  (\mocl{false} \;\mocl{and}\; \mocl{null}) &= \mocl{false}&\qquad
  (\mocl{false} \;\mocl{and}\; \mocl{invalid}) &= \mocl{false}\\
\end{aligned}\\[.04\baselineskip]
\begin{aligned}
  %
  (\mocl{true} \;\mocl{and}\; \mocl{true}) &= \mocl{true}&\qquad
  (\mocl{true} \;\mocl{and}\; \mocl{false}) &= \mocl{false}\\
  (\mocl{true} \;\mocl{and}\; \mocl{null}) &= \mocl{null}&\qquad
  (\mocl{true} \;\mocl{and}\; \mocl{invalid}) &= \mocl{invalid}
\end{aligned}\\[.04\baselineskip]
\begin{aligned}
  (\mocl{invalid} \;\mocl{and}\; \mocl{true}) &= \mocl{invalid} &\qquad
  (\mocl{invalid} \;\mocl{and}\; \mocl{false}) &= \mocl{false}\\
  (\mocl{invalid} \;\mocl{and}\; \mocl{null}) &= \mocl{invalid} &\qquad
  (\mocl{invalid} \;\mocl{and}\; \mocl{invalid}) &= \mocl{invalid}\\
\end{aligned}
\shortintertext{On this core, the structure of a conventional lattice arises:}
  \begin{aligned}
    X \;\mocl{and}\; X &= X        &\qquad     X \;\mocl{and}\; Y &= Y \;\mocl{and}\; X
  \end{aligned}\\
  \begin{aligned}
    \mocl{false} \;\mocl{and}\; X &= \mocl{false} &\qquad
    X \;\mocl{and}\; \mocl{false} &= \mocl{false}  \\
    \mocl{true} \;\mocl{and}\; X  &= X &\qquad
    X \;\mocl{and}\; \mocl{true} &= X
  \end{aligned}\\
  \begin{aligned}
             X \;\mocl{and}\; (Y \;\mocl{and}\; Z) &= X \;\mocl{and}\; Y \;\mocl{and}\; Z
  \end{aligned}
\end{gather*}
as well as the dual equalities for \inlineocl|_ or _| and the De Morgan
rules.  This wealth of algebraic properties makes the understanding of
the logic easier as well as automated analysis possible: for example, it allows
for computing a DNF of invariant systems (by term-rewriting techniques) 
which are a prerequisite for $\delta$-closures.

The above equations explain the behavior for the most-important
non-strict operations. The clarification of the exceptional behaviors
is of key-importance for a semantic definition of the standard and the
major deviation point from
\HOLOCL~\cite{brucker.ea:hol-ocl:2008,brucker.ea:hol-ocl-book:2006}
to \FOCL as presented here.  Expressed in algebraic equations,
``strictness-principles'' boil down to:
\begin{gather*}
  \begin{aligned}
    \mocl{invalid} \;\mocl{+}\; X &= \mocl{invalid} &\qquad
    X \;\mocl{+}\; \mocl{invalid} &= \mocl{invalid}\\
    \mocl{invalid->including(}X\mocl{)} &= \mocl{invalid} &\qquad
    \mocl{null->including(}X\mocl{)} &= \mocl{invalid}\\
    X \isasymMathOclStrictEq  \mocl{invalid} &= \mocl{invalid}&\qquad
    \mocl{invalid} \isasymMathOclStrictEq X &= \mocl{invalid} \\
  \end{aligned}\\
      \mocl{S->including(invalid)}=\mocl{invalid} \\
       X \isasymMathOclStrictEq X =  (\mocl{if}\; \upsilon\; x\; \mocl{then true}
                                         \mocl{else invalid endif}) \\
  \begin{aligned}
    \mocl{1} \;\mocl{/}\; \mocl{0} &= \mocl{invalid} \quad &\quad
    \mocl{1} \;\mocl{/}\; \mocl{null} &= \mocl{invalid} \\
    \mocl{invalid->isEmpty()}&=\mocl{invalid} \quad &\quad \mocl{null->isEmpty()}&=\mocl{null}\\
  \end{aligned}\\
\end{gather*}

Algebraic rules are also the key for execution and compilation
of  \FOCL expressions. We derived, \eg:
\begin{gather*}
\delta\; \mocl{Set\{\}} = \mocl{true}\\
\delta\; (X\mocl{->including(}x\mocl{)}) = \delta \ap X \;\mocl{and}\;
 \upsilon \ap x\\
\begin{aligned}
\mocl{Set\{\}->includes(}x\mocl{)} = (\mocl{if}\; \upsilon\; x\; &\mocl{then false}\\
&\mocl{else invalid endif})
\end{aligned}\\
\begin{multlined}
  {(X\mocl{->including(}x\mocl{)->includes(}y\mocl{)})=}\\
  \mbox{\hspace{3.2cm}}\qquad{\begin{aligned}
   (&\mocl{if}\; \delta\; X\\
  &\mocl{then}\;
\begin{array}[t]{l}
\mocl{if}\; x \doteq y\\
\mocl{then}\ap \mocl{true} \\
\mocl{else}\ap X\mocl{->includes(}y\mocl{)}\\
\mocl{endif}
  \end{array}\\
&\mocl{else invalid} \\
         &\mocl{endif})
  \end{aligned}}
\end{multlined}
\end{gather*}
As \inlineocl+Set{1,2}+ is only syntactic sugar for
\begin{ocl}
  Set{}->including(1)->including(2)
\end{ocl}
an expression like \inlineocl+Set{1,2}->includes(null)+ becomes
decidable in  \FOCL by applying these algebraic laws (which can give
  rise to efficient compilations). The reader interested in the list of
``test-statements'' like:
\begin{isar}[mathescape]
value  "\<tau> \<Turnstile> ($\mathtt{Set\{Set\{2,null\}\}}$ \<doteq> $\;\mathtt{Set\{Set\{null,2\}\}}$)"
\end{isar}
make consult \autoref{formal-set}; these test-statements
 have been machine-checked and proven consistent with the denotational and logic
 semantics of \FOCL.
% It fairly readable information for \OCL tool manufactures and users.


\subsection{Object-oriented Datatype Theories}
In the following, we will refine the concepts of a user-defined
data-model implied by a \emph{class-model} (\emph{visualized} by a class-\emph{diagram})
as well as the notion of $\state{}$ used in the
previous section to much more detail.  \UML class models represent in a compact
and visual manner quite complex, object-oriented data-types with a surprisingly rich
theory. In this section, this theory is made explicit
and corner cases were pointed out.

A \UML class model underlying a
given \OCL invariant or operation contract
produces several implicit operations which
become accessible via appropriate \OCL syntax.
A class model is a four-tuple $(C, \_ < \_, Attrib, Assoc)$ where:
\begin{enumerate}
\item $C$ is a  set of class names (written as $\{C_1, \ldots, C_n\}$). To each class
  name a type of data in \OCL is associated. Moreover, class names declare two projector
  functions to the set of all objects in a state:
  $C_i$\inlineocl{.allInstances()} and
  $C_i$\inlineocl{.allInstances}$\isasymOclATpre$\inlineocl{()},
\item $\_ < \_$ is an inheritance relation on classes,
\item $Attrib(C_i)$ is a collection of
  attributes associated to classes $C_i$. It declares two families of accessors; for each attribute $a \in Attrib(C_i) $ in a
  class definition $C_i$ (denoted
  $\getAttrib{X}{\text{$a$}}               :: C_i \rightarrow A $ and
  $\getAttrib{X}{\text{$a$}\isasymOclATpre}:: C_i \rightarrow A $ for
  $A\in TYPES(C)$),
\item $Assoc(C_i,C_j)$ is a collection of associations\footnote{Given the fact that there is at present no consensus on the
  semantics of n-ary associations, \FOCL{} restricts itself to binary associations. }.
   An association $(n, rn_{from}, rn_{to})\in Assoc(C_i,C_j)$ between to classes
   $C_i$ and $C_j$ is a triple consisting of a (unique) association name $n$,
    and the role-names $rn_{to}$ and $rn_{from}$. To each role-name belong two
    families of accessors   denoted
    $\getRole{X}{\text{$a$}}               :: C_i \rightarrow A$ and
    $\getRole{X}{\text{$a$}\isasymOclATpre}:: C_i \rightarrow A$ for
    $A\in TYPES(C)$),
\item for each pair $C_i < C_j$ ($C_i, C_j < C$), there is a
     cast operation of type $C_j \rightarrow C_i$ that can change the static type
     of an object of type $C_i$:
     $\getAttrib{obj::C_i}{\mocl{oclAsType(}\text{$C_j$}\mocl{)}}$,
\item for each class $C_i\in C$, there are two dynamic type tests
     ($\getAttrib{X}{\mocl{oclIsTypeOf(}\text{$C_i$}\mocl{)}}$ and
     $\getAttrib{X}{\mocl{oclIsKindOf(}\text{$C_i$}\mocl{)}}$ ),
\item and last but not least, for each class name $C_i\in C$ there is an
     instance of the overloaded referential equality (written $\_
     \isasymMathOclStrictEq \_$).
\end{enumerate}


Assuming a strong static type discipline in the sense of
Hindley-Milner types,  \FOCL has no ``syntactic
subtyping.''  In contrast, sub-typing can be expressed
\emph{semantically} in  \FOCL by adding suitable type-casts which do
have a formal semantics. Thus, sub-typing becomes an issue of the front-end 
that can make implicit type-coercions explicit. Our perspective shifts the 
emphasis on the semantic properties of casting, and the necessary universe of 
object representations (induced by a class model) that allows to establish
them.

As a pre-requisite of a denotational semantics for these operations induced
by a class-model, we need an \emph{object-universe} in which these operations can
be defined in a denotational manner and from which the necessary properties
for constructors, accessors, tests and casts
can be derived. A concrete universe constructed from a class model will be
used to instantiate the implicit type parameter $\isaAA$ of all \OCL operations
discussed so far.

\subsubsection{A Denotational Space for Class-Models: Object Universes}

It is natural to construct system states by a set of partial functions
$f$ that map object identifiers $\oid$ to some representations of
objects:
\begin{gather}
       \typedef \qquad \mathfrak{A}~\state{} \defeq \{\sigma ::
        \oid \isasymrightharpoonup \alpha \ap|\ap \inv_\sigma(\sigma) \}
\end{gather}
where $\inv_\sigma$ is a to be discussed invariant on states.

The key point is that we need a common type $\mathfrak{A}$ for the set of all
possible \emph{object representations}.  Object representations model
``a piece of typed memory,'' \ie, a kind of record comprising
administration information and the information for all attributes of
an object; here, the primitive types as well as collections over them
are stored directly in the object representations, class types and
collections over them are represented by $\oid$'s (respectively lifted
collections over them).

In a shallow embedding which must represent
\UML types one-to-one by HOL types, there are two fundamentally
different ways to construct such a set of object representations,
which we call an \emph{object universe} $\mathfrak{A}$:
\begin{enumerate}
\item an object universe can be constructed from a given class model,
  leading to \emph{closed world semantics}, and
\item an object universe can be constructed for a given class model
  \emph{and all its extensions by new classes added into the leaves of
    the class hierarchy}, leading to an \emph{open world semantics}.
\end{enumerate}
For the sake of simplicity, the present semantics chose the first option for
 \FOCL, while HOL-\OCL~\cite{brucker.ea:extensible:2008-b}
used an involved construction allowing the latter.

A na\"ive attempt to construct $\mathfrak{A}$ would look like this:
the class type $C_i$ induced by a class will be the type of such an
object representation: $C_i \defeq (\oid \times A_{i_1} \times \cdots
\times A_{i_k} )$ where the types $A_{i_1}$, \ldots, $A_{i_k}$ are the
attribute types (including inherited attributes) with class types
substituted by $\oid$. The function $\HolOclOidOf$ projects the first
component, the $\oid$, out of an object representation. Then the
object universe will be constructed by the type definition:
\begin{gather}
\mathfrak{A} := C_1 + \cdots +  C_n\mi{.}
\end{gather}
It is possible to define constructors, accessors, and the referential
equality on this object universe. However, the treatment of type casts
and type tests cannot be faithful with common object-oriented
semantics, be it in \UML or Java: casting up along the class hierarchy
can only be implemented by loosing information, such that casting up
and casting down will \emph{not} give the required identity, whenever $C_k  < C_i$ and $X$ is valid:
\begin{gather}
        X.\mocl{oclIsTypeOf(}C_k\mocl{)} ~ ~  \mocl{implies} ~ ~ X\mocl{.oclAsType(}C_i\mocl{)}\mocl{.oclAsType(}C_k\mocl{)} \isasymMathOclStrictEq
   X
\end{gather}

To overcome this limitation, we introduce an auxiliary type
$C_{i\text{ext}}$ for \emph{class type extension}; together, they were
inductively defined for a given class diagram:

Let $C_i$ be a class with a possibly empty set of subclasses
$\{C_{j_{1}}, \ldots, C_{j_{m}}\}$.
\begin{itemize}
\item Then the  \emph{class type extension} $C_{i\text{ext}}$
        associated to $C_i$ is
        $A_{i_{1}} \times \cdots \times A_{i_{n}} \times \up{(C_{j_{1}\text{ext}} + \cdots + C_{j_{m}\text{ext}})}$
        where $A_{i_{k}}$ ranges over the local
        attribute types of $C_i$ and $C_{j_{l}\text{ext}}$
        ranges over all class type extensions of the subclass $C_{j}$ of $C_i$.
\item Then the \emph{class type} for $C_i$ is
        $oid \times A_{i_{1}} \times \cdots \times A_{i_{n}} \times \up{(C_{j_{1}\text{ext}} + \cdots + C_{j_{m}\text{ext}})}$
        where $A_{i_{k}}$ ranges over the inherited \emph{and} local
        attribute types of $C_i$ and $C_{j_{l}\text{ext}}$
        ranges over all class type extensions of the subclass $C_{j}$ of $C_i$.
\end{itemize}

\isatagafp
Example instances of this scheme---outlining a compiler---can be found
in \autoref{ex:employee-analysis:uml} and \autoref{ex:employee-design:uml}.
\endisatagafp
\isatagannexa
Example instances of this scheme---outlining a compiler---can be found
in \autoref{ex:employee-analysis:uml}.
\endisatagannexa

This construction can \emph{not} be done in HOL itself since it
involves quantifications and iterations over the ``set of class-types'';
rather, it is a meta-level construction.  Technically, this means that
we need a compiler to be done in SML on the syntactic
``meta-model''-level of a class model.

With respect to our semantic construction here,
which above all means is intended to be type-safe, this has the following consequences:
\begin{itemize}
\item there is a generic theory of states, which must be formulated independently
      from a concrete object universe,
\item there is a principle of translation (captured by the inductive scheme for
      class type extensions and class types above) that converts a given class model
      into an concrete object universe,
\item there are fixed principles that allow to derive the semantic theory of any
      concrete object universe, called the \emph{object-oriented datatype theory.}
\end{itemize}
\isatagafp
We will work out concrete examples for the construction of the
object-universes in \autoref{ex:employee-analysis:uml} and \autoref{ex:employee-design:uml} and the
derivation of the respective datatype theories. While an
automatization is clearly possible and desirable for concrete
applications of  \FOCL, we consider this out of the scope
of this document which has a focus on the semantic construction and its
presentation.
\endisatagafp
\isatagannexa
We will work out concrete examples for the construction of the
object-universes in \autoref{ex:employee-analysis:uml} and the
derivation of the respective datatype theories. While an
automatization is clearly possible and desirable for concrete
applications of  \FOCL, we consider this out of the scope
of this annex which has a focus on the semantic construction and its
presentation.
\endisatagannexa


\subsubsection{Denotational Semantics of Accessors on Objects and Associations}
Our choice to use a shallow embedding of \OCL in HOL and, thus having
an injective mapping from \OCL types to HOL types, results in
type-safety of  \FOCL\@. Arguments and results of accessors
are based on type-safe object representations and \emph{not} $\oid$'s.
This implies the following scheme for an accessor:
\begin{itemize}
\item The \emph{evaluation and extraction} phase. If the argument
  evaluation results in an object representation, the $\oid$ is
  extracted, if not, exceptional cases like \inlineocl{invalid} are
  reported.
\item The \emph{de-referentiation} phase. The $\oid$ is interpreted in
  the pre- or post-state, %(depending on the suffix of accessor),
  the resulting object is cast to the expected format.  The
  exceptional case of non-existence in this state must be treated.
\item The \emph{selection} phase. The corresponding attribute is
  extracted from the object representation.
\item The \emph{re-construction} phase.  The resulting value has to be
  embedded in the adequate HOL type.  If an attribute has the type of
  an object (not value), it is represented by an optional (set of)
  $\oid$, which must be converted via de-referentiation in one of the
  states to produce an object representation again. The
  exceptional case of non-existence in this state must be treated.
\end{itemize}

The first phase directly translates into the following formalization:
\begin{multline}
  \shoveleft{\isardef}\quad\\
  \begin{array}{rllr}
 \operatorname{eval\_extract} X\ap f = (\lambda \tau\spot \HolCase
 X\ap
 \tau \HolOf & \bottom &\Rightarrow
 \mocl{invalid}\ap\tau&\text{exception}\\
 |& \lift{\bottom} &\Rightarrow
 \mocl{invalid}\ap\tau&\text{deref. null}\\
 |& \lift{\lift{\mathit{obj}}} &\Rightarrow f\ap (\operatorname{oid\_of} \ap \mathit{obj})\ap\tau)&
  \end{array}
\end{multline}

For each class $C$, we introduce the de-referentiation phase of this
form:
\begin{multline}
  \isardef \ap
  \operatorname{deref\_oid}_C \ap \mathit{fst\_snd}\ap f\ap \mathit{oid} =
                     (\lambda \tau\spot \HolCase\ap (\operatorname{heap}\ap
                     (\mathit{fst\_snd}\ap \tau))\ap \mathit{oid}\ap
                     \HolOf\\
  \begin{array}{ll}
           \phantom{|}\ap \lift{\operatorname{in}_C obj} &\Rightarrow f\ap
                     \mathit{obj} \ap \tau\\
                     |\ap \_ &\Rightarrow \mocl{invalid}\ap \tau)
      \end{array}
   \end{multline}

The operation yields undefined if the $\oid$ is uninterpretable in the
state or referencing an object representation not conforming to the
expected type.

We turn to the selection phase: for each class $C$ in the class model
with at least one attribute,
and each attribute $a$ in this class,
we introduce the selection phase of this form:
\begin{gather}
  \begin{array}{rlcll}
  \isardef \ap
    \operatorname{select}_a \ap f = (\lambda &
                  \operatorname{mk}_C \ap oid & \cdots \bottom \cdots & C_{X\text{ext}} & \Rightarrow \mocl{null}\\
                  |& \operatorname{mk}_C \ap oid & \cdots \lift{a} \cdots & C_{X\text{ext}}
                    &\Rightarrow f\ap (\lambda \ap x \ap \_\spot
                   \lift{\lift{x}})\ap a)
  \end{array}
\end{gather}

This works for definitions of basic values as well as for object
references in which the $a$ is of type $\oid$.  To increase
readability, we introduce the functions:
\begin{gather}
\begin{array}{llrlr}
\qquad\qquad&\isardef\enspace&\operatorname{in\_pre\_state}    &= \operatorname{fst} & \qquad \text{first component}\\
\qquad\qquad&\isardef\enspace&\operatorname{in\_post\_state}   &= \operatorname{snd} & \qquad \text{second component} \\
\qquad\qquad&\isardef\enspace&\operatorname{reconst\_basetype} &= \operatorname{id} & \qquad \text{identity function}
\end{array}
\end{gather}


Let \_\inlineocl{.getBase} be an accessor of class $C$ yielding a
value of base-type $A_{base}$. Then its definition is of the form:
\begin{gather}
\begin{array}{lll}
\isardef&\_\mocl{.getBase} &\ofType \ap C \Rightarrow A_{base}\\
\where\enspace&X\mocl{.getBase} &= \operatorname{eval\_extract}\ap X\ap
                       (\operatorname{deref\_oid}_C\ap \operatorname{in\_post\_state}\ap\\
              &          &\quad   (\operatorname{select}_\text{getBase}\ap \operatorname{reconst\_basetype}))
\end{array}
\end{gather}

Let \_\inlineocl{.getObject} be an accessor of class $C$ yielding a
value of object-type $A_{object}$. Then its definition is of the form:
\begin{gather}
\begin{array}{lll}
\isardef&\_\mocl{.getObject} &\ofType \ap C \Rightarrow A_{object}\\
\where\enspace&X\mocl{.getObject} &= \operatorname{eval\_extract}\ap X\ap
                        (\operatorname{deref\_oid}_C\ap \operatorname{in\_post\_state}\ap\\
     &                    &\quad (\operatorname{select}_\text{getObject}\ap
                          (\operatorname{deref\_oid}_C\ap\operatorname{in\_post\_state})))
\end{array}
\end{gather}
The variant for an accessor yielding a collection is omitted here; its
construction follows by the application of the principles of the
former two.  The respective variants
$\getAttrib{\_}{\text{$a$}\isasymOclATpre}$ were produced when
\inlineisar+in_post_state+ is replaced by
$\operatorname{in\_pre\_state}$.

\isatagafp
Examples for the construction of accessors via associations can be found in
\autoref{sec:eam-accessors}, the construction of accessors via attributes in
\autoref{sec:edm-accessors}. The construction of casts and type tests \inlineocl{->oclIsTypeOf()} and
\inlineocl{->oclIsKindOf()} is similarly.
\endisatagafp
\isatagannexa
Examples for the construction of accessors via associations can be found in
\autoref{sec:eam-accessors}. The construction of casts and type tests \inlineocl{->oclIsTypeOf()} and
\inlineocl{->oclIsKindOf()} is similarly.
\endisatagannexa

In the following, we discuss the role of multiplicities on the types of the
accessors.
Depending on the specified multiplicity, the evaluation of an attribute can
yield just a value (multiplicity \inlineocl{0..1} or \inlineocl{1})
or a collection type like Set or Sequence of values (otherwise).
A multiplicity defines a lower bound as well as a possibly infinite upper
bound on the cardinality of the attribute's values.


\paragraph{Single-Valued Attributes}\label{sec:single-valued-properties}
If the upper bound specified by the attribute's multiplicity is one,
then an evaluation of the attribute yields a single value.
Thus, the evaluation result is \emph{not} a collection. If the lower bound specified by the
multiplicity is zero, the evaluation is not required to yield a non-null value. In this case an
evaluation of the attribute can return $\isasymOclNull$ to indicate an
absence of value.

To facilitate accessing attributes with multiplicity \inlineocl{0..1}, the \OCL
standard states that single values can be used as sets by calling collection
operations on them. This implicit conversion of a value to a
\inlineocl{Set} is not defined by the standard. We argue that the resulting set
cannot be constructed the same way as when evaluating a \inlineocl{Set}
literal. Otherwise, $\isasymOclNull$ would be mapped to the singleton set
containing $\isasymOclNull$, but the standard demands that
the resulting set is empty in this case. The conversion should instead
be defined as follows:
\begin{ocl}
context OclAny::asSet():T
  post: if self = null then result = Set{}
        else result = Set{self} endif
\end{ocl}
% Changed self.isTypeOf(\OCLVoid) to self = null to make it easier for the superficial reader

\paragraph{Collection-Valued Attributes}\label{sec:collection-valued-properties}
If the upper bound specified by the attribute's multiplicity is larger than one,
then an evaluation of the attribute yields a collection of values.  This raises
the question whether $\isasymOclNull$ can belong to this collection. The \OCL
standard states that $\isasymOclNull$ can be owned by collections. However, if
an attribute can evaluate to a collection containing $\isasymOclNull$, it is not
clear how multiplicity constraints should be interpreted for this attribute. The
question arises whether the $\isasymOclNull$ element should be counted or not
when determining the cardinality of the collection. Recall that $\isasymOclNull$
denotes the absence of value in the case of a cardinality upper bound of one, so
we would assume that $\isasymOclNull$ is not counted. On the other hand, the
operation \inlineocl{size} defined for collections in \OCL does count
$\isasymOclNull$.

We propose to resolve this dilemma by regarding multiplicities as optional. This
point of view complies with the \UML standard, that does not require lower and
upper bounds to be defined for multiplicities.\footnote{We are however aware
  that a well-formedness rule of the \UML standard does define a default bound
  of one in case a lower or upper bound is not specified.} In case a
multiplicity is specified for an attribute, \ie, a lower and an upper bound
are provided, we require for any collection the attribute evaluates to 
a collection not containing $\isasymOclNull$. This allows for a straightforward 
interpretation of
the multiplicity constraint. If bounds are not provided for an attribute, we
consider the attribute values to not be restricted in any way. Because in
particular the cardinality of the attribute's values is not bounded, the result
of an evaluation of the attribute is of collection type. As the range of values
that the attribute can assume is not restricted, the attribute can evaluate to a
collection containing $\isasymOclNull$. The attribute can also evaluate to
$\isasymOclInvalid$. Allowing multiplicities to be optional in this way gives
the modeler the freedom to define attributes that can assume the full ranges of
values provided by their types. However, we do not permit the omission of
multiplicities for association ends, since the values of association ends are
not only restricted by multiplicities, but also by other constraints enforcing
the semantics of associations. Hence, the values of association ends cannot be
completely unrestricted.

\paragraph{The Precise Meaning of Multiplicity Constraints}
We are now ready to define the meaning of multiplicity constraints by giving
equivalent invariants written in \OCL\@. Let \inlineocl{a} be an attribute of a
class \inlineocl{C} with a multiplicity specifying a lower bound $m$ and an
upper bound $n$. Then we can define the multiplicity constraint on the values of
attribute \inlineocl{a} to be equivalent to the following invariants written in
\OCL:
\begin{ocl}
context C inv lowerBound: a->size() >= m
          inv upperBound: a->size() <= n
          inv notNull: not a->includes(null)
\end{ocl}
If the upper bound $n$ is infinite, the second invariant is omitted. For the
definition of these invariants we are making use of the conversion of single
values to sets described in \autoref{sec:single-valued-properties}. If $n
\leq 1$, the attribute \inlineocl{a} evaluates to a single value, which is then
converted to a \inlineocl{Set} on which the \inlineocl{size} operation is
called.

If a value of the attribute \inlineocl{a} includes a reference to a non-existent
object, the attribute call evaluates to $\isasymOclInvalid$. As a result, the
entire expressions evaluate to $\isasymOclInvalid$, and the invariants are not
satisfied. Thus, references to non-existent objects are ruled out by these
invariants. We believe that this result is appropriate, since we argue that the
presence of such references in a system state is usually not intended and likely
to be the result of an error. If the modeler wishes to allow references to
non-existent objects, she can make use of the possibility described above to
omit the multiplicity.

\subsubsection{Logic Properties of Class-Models}\label{sec:logicprop-datamodel}
In this section, we assume to be $C_z,C_i,C_j \in C$ and  $C_i < C_j$.
Let $C_z$ be a smallest element with respect to the class hierarchy $\_ < \_$.
The operations induced from a class-model have the following properties:
\begin{gather*}
  \tau \isasymMathOclValid X \mocl{.oclAsType(}C_i\mocl{)} \isasymMathOclStrongEq X   \\
 \tau \isasymMathOclValid \mocl{invalid .oclAsType(}C_i\mocl{)} \isasymMathOclStrongEq \mocl{invalid} \\
 \tau \isasymMathOclValid \mocl{null .oclAsType(}C_i\mocl{)} \isasymMathOclStrongEq \mocl{null} \\
 \tau \isasymMathOclValid \mocl{((}X::C_i) \mocl{.oclAsType(C_j) .oclAsType(}C_i\mocl{)} \isasymMathOclStrongEq X\mocl{)}  \\
 \tau \isasymMathOclValid X \mocl{.oclAsType(}C_j\mocl{) .oclAsType(}C_i) \isasymMathOclStrongEq X  \\
 \tau \isasymMathOclValid \mocl{(}X::OclAny\mocl{) .oclAsType(}OclAny\mocl{)} \isasymMathOclStrongEq X \\
 \tau \isasymMathOclValid \upsilon (X :: C_i)  \Longrightarrow %\qquad \qquad \qquad \qquad \\
    \tau \isasymMathOclValid (X \mocl{.oclIsTypeOf(}C_i\mocl{) implies (}X \mocl{.oclAsType(}C_j\mocl{).oclAsType(}C_i\mocl{))} \isasymMathOclStrictEq X) \\
 \tau \isasymMathOclValid \upsilon (X :: C_i) \Longrightarrow  %\qquad \qquad \qquad \qquad \\
    \tau \isasymMathOclValid X \mocl{.oclIsTypeOf(}C_i\mocl{) implies (}X \mocl{.oclAsType(}C_j\mocl{) .oclAsType(}C_i\mocl{))} \isasymMathOclStrictEq X \\
 \tau \isasymMathOclValid \delta X \Longrightarrow \tau \isasymMathOclValid X \mocl{.oclAsType(}C_j\mocl{) .oclAsType(}C_i\mocl{)} \isasymMathOclStrongEq X \\
 \tau \isasymMathOclValid \upsilon X \Longrightarrow \tau \isasymMathOclValid X \mocl{.oclIsTypeOf(}C_i\mocl{) implies} X \mocl{.oclAsType(}C_j\mocl{) .oclAsType(}C_i\mocl{)} \isasymMathOclStrictEq X \\
 \tau \isasymMathOclValid X \mocl{.oclIsTypeOf(}C_j\mocl{)} \Longrightarrow \tau \isasymMathOclValid \delta X \Longrightarrow \tau \isasymMathOclValid \mocl{not} (\upsilon X \mocl{.oclAsType(}C_i\mocl{))} \\
 \tau \isasymMathOclValid \mocl{invalid} \mocl{.oclIsTypeOf(}C_i\mocl{)} \isasymMathOclStrongEq \mocl{invalid} \\
 \tau \isasymMathOclValid \mocl{null .oclIsTypeOf(}C_i\mocl{)} \isasymMathOclStrongEq \mocl{true} \\
 \tau \isasymMathOclValid Person \mocl{.allInstances()->forAll(}X\mocl{|}X \mocl{.oclIsTypeOf(}C_z\mocl{))} \\
 \tau \isasymMathOclValid Person \mocl{.allInstances@pre()->forAll(}X\mocl{|}X \mocl{.oclIsTypeOf(}C_z\mocl{))} \\
 \tau \isasymMathOclValid Person \mocl{.allInstances()->forAll(}X\mocl{|}X \mocl{.oclIsKindOf(}C_i\mocl{))} \\
 \tau \isasymMathOclValid Person \mocl{.allInstances@pre()->forAll(}X\mocl{|}X \mocl{.oclIsKindOf(}C_i\mocl{))} \\
 \tau \isasymMathOclValid (X::C_i)\mocl{.oclIsTypeOf(}C_j\mocl{)} \Longrightarrow \tau \isasymMathOclValid \mocl{(}X::C_i\mocl{).oclIsKindOf(}C_i\mocl{)} \\
(\tau \isasymMathOclValid (X::C_j) \isasymMathOclStrictEq X) = (\tau \isasymMathOclValid \mocl{if } \upsilon X \mocl{then true else invalid endif}) \\
 \tau \isasymMathOclValid (X::C_j) \isasymMathOclStrictEq Y \Longrightarrow  \tau \isasymMathOclValid Y \isasymMathOclStrictEq X \\
 \tau \isasymMathOclValid (X::C_j) \isasymMathOclStrictEq Y \Longrightarrow  \tau \isasymMathOclValid Y \isasymMathOclStrictEq Z  \Longrightarrow   \tau \isasymMathOclValid X \isasymMathOclStrictEq Z
\end{gather*}

\subsubsection{Algebraic Properties of the Class-Models}\label{sec:algprop-datamodel}
In this section, we assume to be $C_i,C_j \in C$ and  $C_i < C_j$.
The operations induced from a class-model have the following  properties:
\begin{gather*}
\begin{array}{ll}
 \mocl{invalid} \mocl{.oclIsTypeOf(}C_i\mocl{)} = \mocl{invalid}  \qquad
 \mocl{null}  \mocl{.oclIsTypeOf(}C_i\mocl{)} = \mocl{true}     \\
 \mocl{invalid} \mocl{.oclIsKindOf(}C_i\mocl{)} = \mocl{invalid}   \qquad
 \mocl{null} \mocl{.oclIsKindOf(}C_i\mocl{)} = \mocl{true}       \\
 (X::C_i) \mocl{.oclAsType(}C_i\mocl{)} = X                    \qquad
 \mocl{invalid} \mocl{.oclAsType(}C_i\mocl{)} = \mocl{invalid}     \\
 \mocl{null} \mocl{.oclAsType(}C_i\mocl{)} = \mocl{null}         \qquad
 (X::C_i) \mocl{.oclAsType(}C_j\mocl{).oclAsType(}C_i\mocl{)} = X
\end{array} \\
 (X::C_i) \isasymMathOclStrictEq X = \mocl{if } \upsilon ~ X \mocl{ then true els invalid endif} \\
\end{gather*}
With respect to attributes $\getAttrib{\_}{\text{a}}$ or $\getAttrib{\_}{\text{a}\isasymOclATpre}$
and role-ends $\getAttrib{\_}{\text{r}}$ or $\getAttrib{\_}{\text{r}\isasymOclATpre}$ we have
\begin{gather*}
 \getAttrib{\mocl{invalid}}{\text{a}} = \mocl{invalid} \qquad
 \getAttrib{\mocl{null}}{\text{a}} = \mocl{invalid} \\
 \getAttrib{\mocl{invalid}}{\text{a}\isasymOclATpre} = \mocl{invalid} \qquad
 \getAttrib{\mocl{null}}{\text{a}\isasymOclATpre} = \mocl{invalid} \\
 \getRole{\mocl{invalid}}{\text{r}} = \mocl{invalid} \qquad
 \getRole{\mocl{null}}{\text{r}} = \mocl{invalid} \\
 \getRole{\mocl{invalid}}{\text{r}\isasymOclATpre} = \mocl{invalid} \qquad
 \getRole{\mocl{null}}{\text{r}\isasymOclATpre} = \mocl{invalid}
\end{gather*}

\subsubsection{Other Operations on States}\label{sec:otherStateOperations}
Defining $\_\isasymOclAllInstances$
is straight-forward; the only difference is the property
$T\isasymOclAllInstances\isasymOclExcludes(\isasymOclNull)$ which is a
consequence of the fact that $\Null{}$'s are values and do not ``live'' in the
state.  \OCL semantics admits states with ``dangling references,''; it is
the semantics of accessors or roles which maps these references to \mocl{invalid},
which makes it possible to rule out these situations in invariants.

%it is
%possible to define a counterpart to \inlineocl+_.oclIsNew()+ called
%\inlineocl+_.oclIsDeleted()+ which asks if an object id (represented by an object
%representation) is contained in the pre-state, but not the post-state.

\OCL does not guarantee that an operation only modifies the path-expressions
mentioned in the postcondition, \ie, it allows arbitrary relations from
pre-states to post-states.  This framing problem is well-known (one of the
suggested solutions is~\cite{kosiuczenko:specification:2006}). We define
\begin{ocl}
 (S:Set(OclAny))->oclIsModifiedOnly():Boolean
\end{ocl}
where \inlineocl|S| is a set of object representations, encoding
a set of $\oid$'s. The semantics of this operator is defined such that
for any object whose $\oid$ is \emph{not }represented in \inlineocl|S|
and that is defined in pre and post state, the corresponding object representation will not change
in the state transition. A simplified presentation is as follows:
\begin{gather*}
I\semantics{X\isasymMathOclIsModifiedOnly} (\sigma, \sigma')  \equiv
  \begin{cases}
    \isasymbottom & \text{if $X' = \bottom \lor \text{null}\in X'$}    \\
     \lift{\isasymforall i \isasymin M\spot
        \sigma~i = \sigma'~i} & \text{otherwise}\mi{.}
   \end{cases}
\end{gather*}
where $X' = I\semantics{X} (\sigma, \sigma')$ and $M=
(\dom~\sigma\cap\dom~\sigma') - \{ \HolOclOidOf x |~x \in\drop{X'}\}$.  Thus, if
we require in a postcondition \inlineocl|Set{}->oclIsModifiedOnly()| and exclude via
\inlineocl+_.oclIsNew()+ and \inlineocl+_.oclIsDeleted()+ the existence of new
or deleted objects, the operation is a query in the sense of the \OCL standard, \ie,
the \inlineocl|isQuery| property is true. So, whenever we have $ \tau
\isasymMathOclValid X\isasymOclExcluding(s.a)\isasymMathOclIsModifiedOnly$ and $ \tau
\isasymMathOclValid X\mocl{->forAll(}x\mocl{|not}(x \doteq s.a) \mocl{)}$, we can infer that $\tau
\isasymMathOclValid s.a \triangleq s.a\isasymOclATpre$.


\subsection{Data Invariants}
\label{sec:invlogic}
Since the present \OCL semantics uses one interpretation function\footnote{This has been handled
differently in previous versions of the Annex A.}, we express the effect of \OCL terms
occurring in preconditions and invariants by a syntactic transformation $\__\text{pre}$ which
replaces:
\begin{itemize}
\item all accessor functions $\getAttrib{\_}{a}$ from the class model $a \in Attrib(C)$ by their
counterparts $\getAttrib{\_}{i\isasymOclATpre}$. For example, $(\getAttrib{\self}{salary} >
500)_\text{pre}$ is transformed to $(\getAttrib{\self}{salary\isasymOclATpre} > 500)$.
\item all role accessor functions  $\getRole{\_}{rn_{from}}$ or  $\getRole{\_}{rn_{to}}$
      within the class model (\ie, $(id, rn_{from},  rn_{to}) \in Assoc(C_i, C_j)$)
      were replaced by their counterparts $\getRole{\_}{rn\isasymOclATpre}$.
      For example, $(\getAttrib{\self}{boss} = null)_\text{pre}$ is transformed to
      $\getAttrib{\self}{boss\isasymOclATpre} = null$.
\item The operation $\_\isasymOclAllInstances$ is also substituted by its
$\isasymOclATpre$ counterpart.
\end{itemize}
Thus, we formulate the semantics of the invariant specification  as follows:
\begin{gather}\label{eq:inv}
\begin{aligned}
& I\semantics{\mathtt{context}~c:C_i~\mathtt{inv}~n: \phi(c)} \tau \equiv  \\
&\qquad \tau  \isasymMathOclValid  (C_i\isasymOclAllInstances\isasymOclForAll(x
\text{|} \phi(x)))~\land \\
&\qquad \tau  \isasymMathOclValid (C_i\isasymOclAllInstances\isasymOclForAll(x
\text{|} \phi(x)))_\text{pre}
\end{aligned}
\end{gather}
Recall that  expressions containing $\isasymOclATpre$ constructs in
invariants or preconditions are syntactically forbidden; thus, mixed forms cannot arise.

\subsection{Operation Contracts}
Since operations have strict semantics in \OCL, we have to distinguish for a specification of an
operation $\mathit{op}$ with the arguments $a_1$, \ldots, $a_n$ the
two cases where all arguments are valid and additionally, $\self$ is non-null (\ie, it must be defined), or not.
In former case, a method call can be replaced by a $\mathit{result}$
that satisfies the contract, in the latter case the result is
\mocl{invalid}. This is reflected by the following definition of the contract semantics:
\begin{gather}\label{eq:contract}
\begin{aligned}
 I\semantics{& \mathtt{context}~C~:: \mathit{op}(a_1, \ldots, a_n) : T \\
                     & \qquad\mathtt{pre}~ \phi(\self, a_1, \ldots, a_n)  \\
                     & \qquad\mathtt{post}~\psi(\self, a_1, \ldots, a_n, \mathit{result})}  \equiv \\
 & \qquad \quad \lambda  s,  x_1, \ldots, x_n, \tau.  \\
 & \qquad\qquad \text{if}  ~ ~ \tau
\isasymMathOclValid \isasymMathOclIsDefined s \land \tau \isasymMathOclValid
\isasymupsilon~x_1 \land \ldots \land  \tau \isasymMathOclValid
\isasymupsilon~ x_n \\
 & \qquad\qquad \text{then} ~ \text{SOME}~ \mathit{result}. ~ ~ ~ ~\tau \isasymMathOclValid \phi(s, x_1, \ldots, x_n)_\text{pre} \\
 & \qquad\qquad\qquad\qquad\qquad\qquad ~ ~          \land \tau \isasymMathOclValid \psi(s, x_1, \ldots, x_n, \mathit{result}))\\
 &\qquad\qquad  \text{else}  ~  \isasymMathOclUndefined
\end{aligned}
\end{gather}
where $\text{SOME}~ x. ~P(x)$ is the Hilbert-Choice Operator that
chooses an arbitrary element satisfying $P$; if such an element does not exist, it chooses
an arbitrary one\footnote{In \HOL, the Hilbert-Choice operator is a first-class element of
the logical language.}. Thus, using the Hilbert-Choice Operator, a contract can be associated
to a function definition:
\begin{gather}\label{eq:contractdef}
    f_{op}  \equiv I\semantics{ \mathtt{context}~C~:: \mathit{op}(a_1, \ldots, a_n) : T \ldots }
\end{gather}
provided that neither $\phi$  nor $\psi$ contain recursive method calls of $\mathit{op}$.
In the case of a query operation (\ie, $\tau$ must have the form: $(\sigma,\sigma)$, which
means that query operations do not change the state; c.f. \mocl{oclIsModifiedOnly()} in
\autoref{sec:otherStateOperations}), this constraint can be relaxed: the above
equation is then stated as \emph{axiom}. Note however, that the consistency of the overall
theory is for recursive query contracts left to the user (it can be shown, for example, by a proof
of termination, \ie, by showing that all recursive calls were applied to  argument vectors that are
smaller wrt. a well-founded ordering). Under this condition, an $f_{op}$ resulting from recursive
query operations can be used safely inside pre- and post-conditions of other contracts.

For the general case of a user-defined contract, the following rule can be established
that reduces the proof of a property $E$ over a method call $f_{op}$ to a proof
of $E(res)$ (where $res$ must be one of the values that satisfy the post-condition $\psi$):
\begin{gather}
  \begin{prooftree}
     \[ \big[ \tau \isasymMathOclValid \psi~self~a_1\ldots a_n~res \big]_{res}
        \leadsto
        \tau \isasymMathOclValid E(res)
     \]
    \justifies
    \tau \isasymMathOclValid E(f_{op}~self~a_1 \ldots a_n)
    \end{prooftree}
\end{gather}
under the conditions:
\begin{itemize}
\item $E$ must be an \OCL term and
\item $\self$ must be defined, and the arguments valid in $\tau$: \\
      $\tau \isasymMathOclValid \isasymMathOclIsDefined~\self \land \tau \isasymMathOclValid \isasymupsilon~a_1 \land \ldots \land  \tau \isasymMathOclValid \isasymupsilon~ a_n$
\item the post-condition must be satisfiable (``the operation must be implementable''):
      $\exists res.~ \tau \isasymMathOclValid \psi ~\self ~a_1 \ldots a_n~res $.
\end{itemize}
For the special case of a (recursive) query method, this rule can be specialized to the following
executable ``unfolding principle'':
\begin{gather}
  \begin{prooftree}
  \tau \isasymMathOclValid \phi~self~a_1\ldots a_n
  \justifies
  (\tau \isasymMathOclValid E(f_{op}~self~a_1\ldots a_n)) = e
  (\tau \isasymMathOclValid E (BODY~self~a_1
  \cdots a_n))
  \end{prooftree}
\end{gather}
where
\begin{itemize}
\item $E$ must be an \OCL term.
\item $\self$ must be defined, and the arguments valid in $\tau$: \\
      $\tau \isasymMathOclValid \isasymMathOclIsDefined~\self \land \tau \isasymMathOclValid \isasymupsilon~a_1 \land \ldots \land  \tau \isasymMathOclValid \isasymupsilon~ a_n$
\item the postcondition $\psi~self~a_1~\ldots~a_n~result$ must be decomposable
      into: \\
      $\psi'~self~a_1~\ldots a_n$ and $result \isasymMathOclStrongEq BODY~self~a_1~\ldots~a_n$.
\end{itemize}
Currently, \FOCL neither supports overloading nor overriding for
user-defined operations: the \FOCL compiler needs to be extended to
generate pre-conditions that constrain the classes on which an
overridden function can be called as well as the dispatch order. This
construction, overall, is similar to the virtual function table that,
e.g., is generated by C++ compilers. Moreover, to avoid logical
contradictions (inconsistencies) between different instances of an
overridden operation, the user has to prove Liskov's principle for
these situations: pre-conditions of the superclass must imply
pre-conditions of the subclass, and post-conditions of a subclass must
imply post-conditions of the superclass.

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End:

%  LocalWords:  \UML \OCL implementors RFP OMG provers invariants
%  LocalWords:  wellfounded Denotational equalities
