\documentstyle[fleqn,wics]{llncs}

\newstytheorem{algorithm}{\bf}{\rm}[theorem]{Algorithm}
\renewcommand{\crossbox}{\ \mbox{$\otimes$} \ }

\title{\titlesize\bf Integrity Enforcement in Object-Oriented Databases\thanks{This work has been supported in part by research grants
from the E.E.C. Basic Research Action 3070 FIDE: ``Formally Integrated Data
Environments''.}}

\author{\large Klaus--Dieter Schewe\inst{1}, Bernhard Thalheim\inst{2},\\Joachim W. Schmidt\inst{1}, Ingrid Wetzel\inst{1}}

\institute{University of Hamburg, Dept. of Computer Science,\\Vogt-K\"olln-Str. 30, D-W-2000 Hamburg 54, FRG \and University of Rostock, Dept. of Computer Science,\\Albert-Einstein-Str. 21, D-O-2500 Rostock, FRG}

\begin{document}

\maketitle
\thispagestyle{empty}

\begin{abstract}

In contrast to the relational model methods in OODBs must enforce structurally defined constraints such as inclusion and referential constraints. It has been shown that this is possible for basic {\em generic update operations}\/ that are determined by the schema. However, such operations only exist for value-representable classes.

In this paper we generalize this result and show that integrity enforcement is always possible. Given some arbitrary method $S$ and some static or transition constraint $\cal I$ there exists a {\em greatest consistent specialization}\/ (GCS) $S_{\cal I}$ of $S$ with respect to $\cal I$. Such a GCS behaves nice in that it is compatible with the conjunction of constraints, inheritance and refinement.

Moreover, it is possible to derive simple representations of GCSs for basic update operations with respect to distinguished classes of explicitly stated static constraints. For the GCS construction of a user-defined operation, however, it is in general not sufficient to replace the involved primitive update operations by their GCSs.

\end{abstract}

\section{Introduction}

Consistency is a crucial property of database application systems. In general a database may be considered as a triplet ($\cal S, O, C$), where $\cal S$ defines a structure, $\cal O$ denotes a collection of state changing operations and $\cal C$ is a set of constraints. Constraints can be classified into static, transition and general dynamic constraints describing legal states, state transitions or state sequences respectively. Then the {\em consistency problem}\/ is to guarantee that each specified operation $o \in {\cal O}$ will never violate any constraint $\cal I \in C$. {\em Integrity enforcement} aims at the derivation of a new set $\cal O^\prime$ of operations such that ($\cal S, O^\prime, C$) satisfies this property.

In this paper we address the integrity enforcement problem with respect
to static and transition constraints. Our analysis will be based on the object
oriented datamodel (OODM) introduced in \cite{icdt} which is based on a clear
distinction between {\em values} and {\em objects} as required e.g. in
\cite{beeri2,beeri}. In this model an object $o$ consists of a unique
identifier $id$, a set of (type-, value-)pairs $( T_i , v_i )$, a set of
(reference-, object-)pairs $( \mbox{\it ref}_j , o_j )$ and a set of methods
$\mbox{\it meth}_k$. A type is defined algebraically by constructors,
selectors, functions and axioms similar to \cite{bk,troll,lipeck2,ehma}. 

The class concept provides the grouping of objects having
the same structure which uniformly combines aspects of object values
and references. The extent of classes varies over time, whereas types are
immutable. Relationships between classes are represented by references
together with referential constraints on the object identifiers involved.
Moreover, each class is accompanied by a collection of methods. A schema is
given by a collection of class definitions together with explicit
constraints. This datamodel is related to some other work on the
foundations of object oriented databases
\cite{abiteboul,beeri,ehrich,oid,jan}, but it is distinct from existing
systems \cite{manifesto,iql,heuer}. The description of the OODM
will appear in Section \ref{fundamentals}.

In general, verification techniques based on predicate transformers are applicable \cite{iwsds}. This includes to show that each update operation starting in a legal state with respect to the static constraints can only end up in legal states. This also comprises that methods on subclasses overriding inherited methods must be specializations. The latter proof obligation can be exploited to formalize the satisfaction of transition constraints, since each transition constraint can be regarded as a general predicatively specified method. Then a method satisfies a transition constraint iff it specializes the method associated with the constraint. In Section \ref{theory} we describe in part the theoretical background of consistency verification.

An obvious disadvantage of the verification approach is that it does not help the user in writing consistent operations. An alternative is to generate a {\em Greatest Consistent Specialization} (GCS) of a given method with respect to the given constraints. This comprises the following problems:

\begin{enumerate}

\item Does a GCS exist in general? Is it compatible with the conjunction of constraints, optimization, inheritance and refinement?

\item How does a GCS look like in the OODM with respect to distinguished classes of constraints?

\item How to enforce integrity of general user-defined operations with respect to arbitrary constraints? Is it sufficient to replace involved primitive operations by their GCSs?

\end{enumerate}

\noindent
In Section \ref{enforcement} we address these problems for
static constraints. We show the existence of GCSs and also discuss
compatibility results with respect to the conjunction of constraints,
specialization and refinement. These positive result set up a fundamental
distinction to trigger approaches \cite{tanca}, where conjunctivity can not
be guaranteed. In Section \ref{oodm-integrity} we describe the structure of
GCSs in the OODM with respect to specific classes of constraints. Moreover,
we show that the general enforcement problem can not be reduced to primitive
operations. In Section \ref{dynamic} we derive the existence of GCSs for
transition constraints and also discuss compatibility properties. We conclude
in Section \ref{open} discussing some open problems concerning the handling
of general dynamic constraints and the structure of GCSs in general.

\section{Theoretical Background} \label{theory}

For the moment let us abstract from the specific database context. Look at a database being defined as some {\em state space} $X$ with typed state variables $x_1 :: T_1 , \ldots , x_n :: T_n$. Then {\em state transitions} on $X$ are expressible by (partial, non-deterministic) guarded commands with a sophisticated axiomatic semantics defined by predicate transformers. Formulae in first-order logic can be used to express both static and transition integrity {\em constraints} on $X$. We adopt this approach in order to formalize OODM as well as the integrity enforcement problem within a strict mathematical framework that will later be applied to the OODM.

\subsection{Types} \label{types}

In general a type is specified by a collection of constructors, selectors
and other functions -- the signature of the type -- and axioms defined by
universal Horn formulae \cite{stacs}. Now let $N_P$, $N_T$, $N_F$, and $V$
denote arbitrary pairwise disjoint, countably infinite sets representing a
reservoir of parameter-, type-, function-, and variable-names respectively.

\begin{definition} \label{def-signature}

\ A {\em type signature} $\Sigma$ consists of a type name $t \in N_T$, a finite set of supertype-/function-pairs $T \subseteq N_T \times N_F$, a
finite set of parameters $P \subseteq N_P$, a finite set of base types $B
\subseteq N_T$ and pairwise disjoint finite sets $C, \, S, \, F \subseteq
N_F$ of constructors, selectors and functions such that there exist
predefined arities $ar(c) \in (P \cup B^* \cup \{ t \} )^* \times \{ t \}$,
$ar(s) \in \{ t \} \times (P \cup B^* \cup \{ t \} )$ and
$ar(f) \in (P \cup B^* \cup \{ t \} )^* \times (P \cup B^* \cup \{ t \} )$ for
each $c \in C$, $s \in S$ and $f \in F$.

\end{definition}

\noindent
We write $f : t \rightarrow t^\prime$ to denote a {\em supertype-/function-pair} $(t^\prime,f) \in T$.
We write $c : t_1 \times \ldots \times t_n \rightarrow t$ to denote a {\em
constructor} of arity $(t_1 \ldots t_n , t )$, $s : t \rightarrow t^\prime$
to denote a {\em selector} of arity $( t , t^\prime )$ and
$f : t_1 \times \ldots \times t_n \rightarrow t^\prime$ to denote a {\em
function} of arity $(t_1 \ldots t_n , t^\prime )$. If $t_i = b_i^0 \ldots b_i^m \in B^*$, we write $b_i^0 ( b_i^1 \ldots b_i^m )$. We call ${\cal S} = P
\cup B \cup \{ t \} $ the set of {\em sorts} of the signature $\Sigma$. 

\begin{definition} \label{type}

\ A {\em type declaration} consists of a type signature $\Sigma$ with type
name $t$ such that there exists a type declaration for each $b \in B - \{ t \}$ and
a set $Ax$ of Horn formulae over $\Sigma$. Moreover, if $b_i^0 ( b_i^1 \ldots b_i^m )$ with $b_i^j \in B$ occurs within a constructor, selector or function, then $b_i^0$ must have been declared as a parameterized type with $m$ parameters. We say that $( \Sigma , Ax )$
defines the {\em parameterized type} $t ( \alpha_1 , \ldots , \alpha_n )$,
iff $P = \{ \alpha_1 , \ldots , \alpha_n \} \neq \emptyset$ or the {\em proper
type} $t$ respectively.\\
A {\em type} $t$ is defined either by a type declaration or by mutually recursive equations involving $t$ as a variable.

\end{definition}

\noindent
The semantics of a type is given by term generated algebras that are quotients of the term algebra defined by the constructors. Subtyping is modelled by the use of a continous function taking the subtype to the supertype. Recursive types are fixpoints of functors. It can be shown that even the guarded commands give rise to a type $GC(\alpha,\beta,\gamma)$, where $\alpha$ ($\beta$) is the type of the input (output) and $\gamma$ is the type of the underlying state space. See \cite{iwsds} for more details.

\subsection{State Transitions} \label{transitions}

In general non-deterministic partial state transitions $S$ on a state space $X$ can be described by a subset of $\cal D \times D_\bot$, where $\cal D$ denotes the set of possible states on $X$ and $\cal D_\bot = D \cup \{ \bot \}$, where $\bot$ is a special symbol used to indicate non-termination. It can be shown that this is equivalent to defining two predicate transformers $wp(S)$ and $wlp(S)$ associated with $S$ satisfying the pairing condition $wp(S)({\cal R}) \Leftrightarrow wlp(S)({\cal R}) \wedge wp(S)(true)$ and the universal conjunctivity of $wlp(S)$. They assign to some postcondition $\cal R$ the {\em weakest (liberal) precondition} of $S$ to establish $\cal R$. Informally these conditions can be characterized as follows:

\begin{itemize}

\item $wlp(S)({\cal R})$ characterizes those initial states such that all terminating executions of $S$ will reach a final state characterized by $\cal R$ provided $S$ is defined in that initial state, and

\item $wp(S)({\cal R})$ characterizes those initial states such that all executions of $S$ terminate and will reach a final state characterized by $\cal R$ provided $S$ is defined.

\end{itemize}

\noindent
Such operations $S$ can be specified by guarded commands in the style
of Dijkstra \cite{dij,nelson}:

\begin{definition} \label{guardedcommand}

Let $X$ be some state space. A {\em guarded command} $S$ on $X$ consists 
of a name $S$, a set of input-parameters $\{ \iota_1 , \ldots ,
\iota_k \}$, a set of output-parameters $\{ o_1 , \ldots , o_l \}$ and a body. To each input-parameter $\iota_i$ corresponds a type $T_i$ and to each output-parameter $o_j$ corresponds a type $O_j$. The
{\em body} of $S$ is recursively built from the following constructs:

\begin{enumerate}

\item assignment $x := E$, where $x$ is a state variable in $X$ or a local variable within $S$ and $E$ is a term of the same type as $x$,

\item $skip$, $fail$, $loop$,

\item sequential composition $S_1 ; S_2$, choice $S_1 \Box S_2$, projection 
$x :: T \mid S$, guard ${\cal P} \rightarrow S$, restricted choice $S_1 \crossbox
S_2$, where $\cal P$ is a well-formed formula and $x$ is a variable of type $T$, and

\item instantiation $x_1^\prime , \ldots , x_i^\prime \leftarrow {S^\prime} ( 
E_1^\prime , \ldots , E_j^\prime )$, where ${S^\prime}$ is the name of another operation ($S = S^\prime$ is possible)
on $X$ with input-parameters $\iota_1^\prime ,
\ldots , \iota_j^\prime$ and output-parameters $o_1^\prime , \ldots ,
o_i^\prime$, such that the variables $o_f^\prime$, $x_f^\prime$ have the same
type and the term $E_g^\prime$ has the same type as the variable
$\iota_g^\prime$.

\end{enumerate}

\end{definition}

\noindent
Each variable occurring in the $S$ has a well-defined scope. The scoping rules are omitted. Furthermore, we omit the detailed definition of the predicate transformers $wlp(S)$ and $wp(S)$ \cite{nelson,iwsds}. We only give an informal description of the less usual operations {\em projection}, {\em guard} and {\em restricted choice}. Projection gives the introduction of a new local variable $x$ of the given type. A guard ${\cal P} \rightarrow S$ gives a precondition $\cal P$ for $S$. If $\cal P$ is not satisfied, the whole operation is undefined. Restricted choice $S \crossbox T$ means to execute $S$ unless it is undefined in which case $T$ is taken. The basic commands $skip$, $fail$, $loop$ are only introduced for theoretical completeness: $skip$ does nothing, $fail$ is always undefined, and $loop$ never terminates.

Here we dispense with any structuring of state spaces into modules. However, in order to define ``extended operations'' we need to know for each operation $S$ the subspace $Y \subseteq X$ such that $S$ does neither read nor change the values in $X - Y$. In this case we call $S$ a $Y$-operation on $X$. We omit the formal details \cite{nelson,iwsds}.

\subsection{Consistency Proof Obligations} \label{verification}

General constraints and arbitrary operations on a state space $X$ raise the problem whether consistency as defined by the constraints is always satisfied by the operations. One approach to address this problem is to use general verification techniques. The verification approach consists in the derivation (and proof) of general proof obligations expressed in the predicate transformer calculus. 

The static constraints on a state space $X$, i.e. first-order formulae $\cal I$ with $fr({\cal I}) \subseteq X$ partition the state space, i.e. the collection of the mutable classes into two distinguished subspaces. States not satisfying the constraints should never be reached. 

In general inherited operations can be overwritten. Unless inheritance is simply regarded as a copying mechanism we should ensure that this can be done in a concise way, i.e., overriding should be restricted to ``specialization''. The intuition behind this definition is that whenever an execution of the specialized operation $T$ establishes some post-predicate $\cal R$, then this execution should already be one of the general method $S$. 

Transition constraints on $X$ are expressible as first-order formulae $\cal J$ with $fr({\cal J}) \subseteq X \disunion X^\prime$, where $X^\prime$ is a disjoint copy of $X$. We may then exploit a weak equivalence between guarded commands and predicative specifications. We may associate with the transition constraint $\cal J$ the guarded command $\;  \Phi({\cal J}) = x^\prime \mid {\cal J} \rightarrow x := x^\prime \;$ where $x$ ($x^\prime$) is used as an abbreviation for the collection $x_1 , \ldots ,x_n$ ($x_1^\prime , \ldots ,x_n^\prime$) of (state) variables. Satisfying $\cal J$ is equivalent to each operation $S$ specializing $\Phi({\cal J})$. Hence the following formal definitions:

\begin{definition} \label{cons} \label{nelson-order}

Let $X$ be a state space, $Z \subseteq Y \subseteq X$ subspaces, $\cal I$ a static and $\cal J$ a transition constraint on $X$, $S$ a $Z$-operation and $T$ a $Y$-operation. 

\begin{enumerate}

\item $S$ is {\em consistent} with respect to $\cal I$ iff $ \; {\cal I} \; \Rightarrow \; wlp(S)({\cal I}) \; $ holds on $X$.

\item $T$ {\em specializes} $S$ iff $wp(S)(true) \,
\Rightarrow \, wp(T)(true)$ and $\; wlp(S)({\cal R}) \, \Rightarrow$\\
$wlp(T)({\cal R}) \;$ hold for all $Z$-predicates $\cal R$ (denoted $T
\sqsubseteq S$).

\item $S$ is {\em consistent} with respect to $\cal J$ iff $\cal R$ $\; wlp(\Phi({\cal J}))({\cal R}) \, \Rightarrow \, wlp(S)({\cal R}) \;$ holds for all $X$-predicates.

\end{enumerate}

\end{definition}

\noindent
Note that $\sqsubseteq$ defines a partial order on operations.
There exists an equivalent characterization of transition consistency
that avoids the quantification over all state predicates \cite{ab-rev}. See
\cite{iwsds} for more details.

\section{Fundamentals of Object Oriented Data Modelling} \label{fundamentals}

In the following assume to be given a type system $\bbbt$ as described e.g. in Section \ref{types}. Basically such a type system consists of some {\em basic types}\/ such as $BOOL$, $\bbbn$, $\bbbz$, $STRING$, etc., {\em type constructors}\/ (parameterized types) for record, finite sets, lists, etc. and a {\em subtyping}\/ relation. Moreover, assume that (mutually) {\em recursive types}\/, i.e. types defined by (a system of) domain equations, exist in $\bbbt$. As an alternative to our definition of $\bbbt$ in Section \ref{types} we may restrict $\bbbt$ being one of the type systems  defined in \cite{type1}. In addition we suppose the existence of an abstract identifier type $ID$ in $\bbbt$ without any non-trivial supertype. Arbitrary {\em types}\/ can then be defined by nesting. A type $T$ without occurrence of $ID$ will be called a {\em value-type}\/.

Now let $N_P$, $N_T$, $N_C$, $N_R$, $N_F$, $N_M$ and $V$ denote
arbitrary pairwise disjoint, denumerable sets representing parameter-, type-, class-, reference-, function-, method- and variable-names
respectively.

\subsection{The Concept of a Class} \label{classes}

The OODM in \cite{icdt} distinguishes between values grouped into types and objects grouped into classes. The extent of classes varies over time, whereas types are immutable. Relationships between classes are represented by references together with referential constraints on the object identifiers involved. Moreover, each class is accompanied by a collection of methods defined by deterministic guarded commands \cite{nelson,ab-rev,iwsds}.

Each object in a class consists of an identifier, a collection of values and references to objects in other classes. Identifiers can be represented using the unique identifier type $ID$. Values and references can be combined into a representation type, where each occurence of $ID$ denotes references to some other classes. Therefore, we may define the structure of a class using parameterized types.

\begin{definition} \label{structure-expression}

\begin{enumerate}

\item Let $t$ be a value type with parameters $\alpha_1 , \ldots , \alpha_n$. For distinct reference names $r_1 , \ldots , r_n \in N_R$ and class names $C_1 , \ldots , C_n \in N_C$ the expression derived from $t$ by replacing each $\alpha_i$ in $t$ by $r_i : C_i$ for $i = 1 , \ldots , n$ is called a {\em structure expression}.

\item A {\em class}\/ consists of a class name $C \in N_C$, a structure expression $S$, a set of class names $D_1 , \ldots , D_m \in N_C$ (in the following called the set of {\em superclasses}\/), a set of static constraints ${\cal I}_1 , \ldots , {\cal I}_k $ and a set of transition constraints ${\cal J}_1 , \ldots , {\cal J}_l $. We call $r_i$ the {\em reference}\/ named $r_i$ from class $C$ to class $C_i$. The type derived from $S$ by replacing each reference $r_i : C_i$ by the type $ID$ is called the {\em representation type} $T_C$ of the class $C$.

\item A {\em schema} $\cal S$ is a finite collection of classes $C_1 , \ldots , C_n$ closed under references and superclasses together with a collection of static constraints ${\cal I}_1 , \ldots , {\cal I}_n $ and a collection of transition constraints ${\cal J}_1 , \ldots , {\cal J}_m $.

\item An {\em instance} $\cal D$ of a schema $\cal S$ assigns to each class $C$ a value ${\cal D} (C)$ of type $PFUN(ID,T_C)$ such that all implicit and explicit constraints on $\cal S$ are satisfied.

\end{enumerate}

\end{definition}

\noindent
Here we dispense with giving a concrete syntax for constraints and methods. On the representation level (see Section \ref{schema-rep}) we may use deterministic guarded commands for methods and first-order formulae for constraints. Distinguished classes of static constraints will be introduced in Section \ref{constraints}. Subclasses inherit the methods of their superclasses, but overriding is allowed as long as the new method is a specialization of all its corresponding methods in its superclasses.

\subsection{The Representation of a Schema} \label{schema-rep}

We now associate with each schema $\cal S$ a state space $X$ such that each class $C$ in $\cal S$ is represented by a state variable $x_C :: PFUN(ID,T_C)$ in $X$ called the {\em class type} of $C$. $PFUN(\alpha,\beta)$ is the type constructor for partial function from $\alpha$ to $\beta$ with finite domain. Moreover, $C$ gives rise to {\em referential
constraints} defined by the structure $S$ and {\em class inclusion constraints} defined by the set of superclasses of $C$. All other constraints on $\cal S$ and $C$ are directly translatable in constraints on $X$. Methods on $C$ are $Y$-operations on $X$ with $Y = \{ x_C \}$. Note that due to identifiers being only an internal concept, only value-defined operations, i.e. all input- and
output-types are value types, are accessible to the user. Let us now formally
describe the form of structurally defined inclusion and referential
constraints.

\begin{definition} \label{iic} \label{ric}

Let $C$, $C^\prime$ be classes with representation types $T_C$ and $T_C^\prime$
respectively and let $o : T_C \times ID \rightarrow BOOL$ be a function.

\begin{enumerate}

\item If $T_C$ be a subtype of $T_C^\prime$ via $f : T_C \rightarrow
T_C^\prime$, a {\em class inclusion constraint} on $C$ and $C^\prime$ is a
constraint in the form
\begin{eqnarray*}
&& \forall i :: ID . \, \forall v :: T_C . \: member(Pair(i,v),x_C) = true \; \Rightarrow
\end{eqnarray*}
\begin{equation}
\hspace*{35pt} member(Pair(i,f(v)),x_{C^\prime}) = true \enspace ,
\end{equation}
\noindent 
where $Pair$ is the constructor of $PAIR(\alpha,\beta)$ and $member$ is a function on finite sets $FSET(\alpha)$, hence also on the subtype $PFUN(\alpha,\beta)$.

In the general case a {\em class inclusion constraint} on $C$ and $C^\prime$ has the form
\begin{eqnarray*}
&& \hspace*{-15pt} \forall i :: ID . \: member(i,dom(x_C)) = true \; \Rightarrow member(i,dom(x_{C^\prime})) = true \enspace .
\end{eqnarray*}

\item A {\em referential constraint} on $C$ and $C^\prime$ is a constraint in the form
\begin{eqnarray*} 
&& \forall i,j :: ID . \, \forall v :: T_C . \: member(Pair(i,v),x_C) = true \, \wedge
\end{eqnarray*}
\begin{equation}
\hspace*{35pt} o(v,j) = true \; \Rightarrow \; member(j,dom(x_{C^\prime})) = true \enspace .
\end{equation}

\end{enumerate}

\end{definition}

\noindent
It is easy to see that each class $D$ in the set of superclasses of $C$ gives rise to an inclusion constraint. Moreover, each reference $r : E$ occurring in the structure expression $S$ of $C$ gives rise to a referential constraint with the function $o$ determined by the type underlying $S$. Then $o(v,j) = true$ means that the identifier $j$ occurs within $v$ at a place corresponding to the reference.

\subsection{Value Representability} \label{value-rep}

Let us first concentrate on primitive update methods, i.e. insertion, deletion and update of a single object on a classes $C$. In contrast to the relational datamodel such update operations can not always be derived in the object-oriented case, because the abstract identifiers have to be hidden from the user. However, in \cite{rostock,icdt} it has been shown that for {\em value-representable} classes these operations are uniquely determined by the schema and consistent with respect to the implicit referential and inclusion constraints.

\begin{definition} \label{def-valuerep}

A class $C$ in a schema $\cal S$ with representation type $T_C$ is called {\em value-representable} iff there exists a proper value type $V_C$ such that for all instances $\cal D$ of $\cal S$ there is a function $c: T_C \rightarrow V_C$ such that for $\cal D$

\begin{enumerate}

\item the condition \ $\forall i,j :: ID . \, \forall v,w :: T_C . \; member(Pair(i,v),x_C) = true \wedge$\\
\indent $member(Pair(j,w),x_C) = true \; \wedge \; c(v) = c(w) \; \Rightarrow \; i = j$ \ holds and

\item for each pair ($V_C^\prime,c^\prime$) consisting of a proper value type $V_C^\prime$ and a function $c^\prime: T_C \rightarrow V_C^\prime$ such that property (i) is satisfied there exists a function $c^\prime{}^\prime: V_C \rightarrow V_C^\prime$ that is unique on $c(codom_{\cal D}(x_C))$ with $c^\prime = c^\prime{}^\prime \circ c$.

\end{enumerate}

\noindent
If only the first property holds, $C$ is called {\em value-identifiable}.

\end{definition}

\begin{theorem} \label{icdt-theorem}

\ Let $C$ be a class in a schema $\cal S$. Then there exist unique canonical update operations on $C$ iff $C$ and all its superclasses are value-representable.

\end{theorem}

\noindent
For details and proofs see \cite{icdt}.

\subsection{An Example}

Let us now finalize the presentation of the datamodel by a simple example.

\begin{example} \label{bsp-class}

Assume the existence of a value type PERSON defined elsewhere. A class $C$ named {\sc PersonC} may be defined
as follows. Some details such as the definition of the method named ``exists'' are omitted, but we remark that the described insert-method is in fact the canonical one \cite{icdt}.\\

\noindent
{\sc PersonC} ==\\
\indent {\tt Structure} \ PAIR( PERSON , spouse : {\sc PersonC})\\
\indent {\tt Constraints} \ $\forall$ I,J :: ID . $\forall$ V :: $T_C$ . \, member(Pair(I,V),$x_C$) = true $\wedge$\\
\hspace*{20pt} member(Pair(J,V),$x_C$) = true  $\Rightarrow$  I = J\\
\indent {\tt Methods} \\
\indent \hspace*{10pt} insert( P :: $V_C$ = PAIR(PERSON,$V_C$) ) == I $\leftarrow$ insert$^\prime$(P)\\
\indent ({\sl\tt hidden}) \\
\hspace*{15pt} I :: ID $\leftarrow$ insert$^\prime$( P :: $\overline{V_C}$ = PAIR(PERSON,UNION($\overline{V_C}$,ID)) ) ==\\
\hspace*{20pt} B :: BOOL $\mid$ \, ( \, B $\leftarrow$ exists(P,$x_C$ ) \ ;\\
\hspace*{25pt} B = true  $\rightarrow$\\
\hspace*{30pt} ( \, I :: ID $\mid$ \, ( member(I,dom($x_C$)) = false  $\rightarrow$\\
\hspace*{45pt} P$^\prime$$^\prime$ :: $T_C$ $\mid$ \\
\hspace*{55pt} ( \ $\exists$ P$^\prime$ :: $T_C$ . P$^\prime$ = P  $\rightarrow$  P$^\prime$$^\prime$ := P \ $\crossbox$ \\
\hspace*{60pt} ( \ J :: ID $\mid$ \, J $\leftarrow$ insert$^\prime$( substitute(P,I,second(P))) \ ; \\
\hspace*{65pt} P$^\prime$$^\prime$ := Pair(first(P),J) \, )) \ ;\\
\hspace*{35pt} $x_C$ := union($x_C$,single(Pair(I,P$^\prime$$^\prime$)))))\\
\hspace*{25pt} $\crossbox$ \ skip \\
{\tt End} \ {\sc PersonC} \qed

\end{example}

\section{Enforcing Static Integrity} \label{enforcement}

An alternative to consistency verification is the computation of methods that enforce all constraints of a schema. We now address this problem first for static constraints and generalize Theorem \ref{icdt-theorem}. Our approach starts with a formalization of the integrity enforcement problem focussing on GCSs. We show that GCSs always exist and are unique (up to semantic equivalence). On this formal basis we are able to describe certain compatibility results and outline the structure of GCSs with respect to basic update operations and distinguished classes of static constraints.

\subsection{The Problem} \label{stat-problem}

Suppose now to be given an update operation $S$ and a static constraint $\cal
I$. Assume that $S$ is an $X$-operation, whereas $\cal I$ is defined on $Y$
with $X \subseteq Y$. The idea is to construct a ``new'' $Y$-operation
$S_{\cal I}$ that is consistent with respect to $\cal I$ and can be used to
replace $S$. Roughly speaking this means that the effect of $S_{\cal I}$ on
the state variables in $X$ should not be different from the effect of $S$.
Formally this is expressed by the specialization relation introduced in
Definition \ref{cons}. Clearly, if any there will be more than one such
specialization. Hence the idea to distinguish one of them as the ``greatest'',
i.e. all others should specialize it.

Before giving now the definition of a GCS let us first remark
that for any predicate transformer $f$ the {\em conjugate predicate
transformer}\/ $f^*$ is defined by $f^*({\cal R}) \, = \, \neg f( \neg {\cal
R})$. Hence the following definition of a {\em greatest consistent
specialization}\/: 

\begin{definition} \label{def-gcs}

Let $X \subseteq Y$ be state spaces, $S$ an $X$-operation and $\cal I$ a static integrity constraint on $Y$. A $Y$-operation $S_{\cal I}$ is a {\em Greatest Consistent Specialization}\/ (GCS) of $S$ with respect to $\cal I$ iff 

\begin{enumerate}

\item $wlp(S)({\cal R}) \; \Rightarrow \; wlp(S_{\cal I})({\cal R}) \;$ holds on $Y$ for all formulae $\cal R$ with $fr({\cal R}) \subseteq X$,

\item $wp(S(true) \; \Rightarrow \; wp(S)_{\cal I})(true) \;$ holds on
$Y$, 

\item ${\cal I} \; \Rightarrow \; wlp(S_{\cal I})({\cal I}) \enspace$ holds on $Y$ and

\item for each $Y$-operation $T$ satisfying properties (i) -- (iii) (instead
of $S_{\cal I}$) we have

\begin{enumerate}

\item $wlp(S_{\cal I})({\cal R}) \; \Rightarrow \; wlp(T)({\cal R}) \;$ for all formulae $\cal R$ with $fr({\cal R}) \subseteq X$ and

\item $wp(S_{\cal I})(true) \; \Rightarrow \; wp(T)(true) \enspace
.$

\end{enumerate}

\end{enumerate}

\end{definition}

\noindent
Note that properties (i) and (ii) require $S_{\cal I}$ to be a
specialization of $S$. Property (iii)
requires $S_{\cal I}$ to be consistent with respect to the constraint $\cal
I$. Finally, property (iv) states that each consistent specialization $T$ of
$S$ with $T \, \sqsubseteq \, S$ also specializes $S_{\cal I}$. 

Based on the formal definition of a GCS we can now raise the following questions:

\begin{itemize}

\item Does such a GCS always exist? If it does, is it uniquely determined by $S$ and $\cal I$ (up to semantic equivalence)?

\item Is the GCS $S_{\cal I}$ of a deterministic operation $S$ itself deterministic? If not, how to achieve a deterministic consistent operation?

\item Does a GCS ${( S_{{\cal I}_1} )}_{{\cal I}_2}$ (provided it exists) with respect to more than one integrity constraint depend on the order of enforcement? Is it sufficient to take ${( S_{{\cal I}_1} )}_{{\cal I}_2}$ in order to enforce integrity with respect to ${\cal I}_1 \wedge {\cal I}_2$\/?

\item What is the relation between integrity enforcement and inheritance, i.e. is the GCS $\; T_{\cal I}$ of a specialization $T$ of $S$ a specialization of the GCS $S_{\cal I}$ of $S$\/?

\item How does a GCS look like (if it exists)?

\end{itemize}

\noindent
Partial results for these questions will be discussed in the next subsections.

\subsection{Greatest Consistent Specializations} \label{stat-gcs}

Let us first address the existence problem. Based on the axiomatic
semantics via predicate transformers we can show that a GCS always exists and
is uniquely determined up to semantic equivalence. First, however, we need
some general properties concerning the specialization order $\sqsubseteq$.

\begin{lemma} \label{lemma-supremum}

Let $\cal T$ be a set of $X$-operations. Then there exists the least upper
bound $S_0 \; = \; \bigsqcup\limits_{S \in {\cal T}} \, S$ with respect to
$\sqsubseteq$. $S_0$ is uniquely determined (up to semantic equivalence) and
satisfies

\begin{enumerate}

\item \begin{equation} \label{4}
wlp(S_0)({\cal R}) \; \Leftrightarrow \; \bigwedge_{S \in {\cal T}} \, wlp(S)({\cal R}) \enspace \mbox{and}
\end{equation}

\item \begin{equation} \label{5}
wp(S_0)({\cal R}) \; \Leftrightarrow \; \bigwedge_{S \in {\cal T}} \,
wp(S)({\cal R})  \end{equation}

\end{enumerate}

\noindent
for all formulae $\cal R$ with $fr({\cal R}) \subseteq X$.

\end{lemma}

\begin{proof}

Let $S_0$ be defined (up to semantic equivalence) by (\ref{4}) and
(\ref{5}). Then the universal conjunctivity and the pairing condition are
trivially satisfied. It follows that $S_0$ is an $X$-operation.

Let $T \in {\cal T}$ and $\cal R$ be an arbitrary formula with $fr({\cal R})
\subseteq X$. Then we have:

\begin{itemize}

\item \[ \bigwedge\limits_{S \in {\cal T}} \; wlp(S)({\cal R}) \; \Rightarrow
\; wlp(T)({\cal R}) \enspace \mbox{and} \]

\item \[ \bigwedge\limits_{S \in {\cal T}} \; wp(S)({\cal R}) \; \Rightarrow
\; wp(T)({\cal R}) \enspace . \]

\end{itemize}

\noindent
Thus, $S_0$ is an upper bound of $\cal T$. If $T_0$ is any upper bound of
$\cal T$, we get

\begin{itemize}

\item \[ wlp(T_0)({\cal R}) \; \Rightarrow
\; wlp(T)({\cal R}) \enspace \mbox{and} \]

\item \[ wp(T_0)({\cal R}) \; \Rightarrow
\; wp(T)({\cal R}) \]

\end{itemize}

\noindent
for all $T \in {\cal T}$, hence also

\begin{itemize}

\item \[ wlp(T_0)({\cal R}) \; \Rightarrow
\; \bigwedge\limits_{S \in {\cal T}} \; wlp(S)({\cal R}) \enspace \mbox{and} \]

\item \[ wp(T_0)({\cal R}) \; \Rightarrow
\; \bigwedge\limits_{S \in {\cal T}} \; wp(S)({\cal R}) \enspace . \]

\end{itemize}

\noindent
It follows that $S_0 \sqsubseteq T_0$, i.e. $S_0$ is the least upper
bound. \qed

\end{proof}

\noindent
Note that for ${\cal T} = \emptyset$ the least upper bound is $fail$. Now we
are prepared to present our result concerning the unique existence of a GCS.

\begin{theorem} \label{existence-theorem}

Let $S$ be an $X$-operation, $X \subseteq Y$ and $\cal I$ a static integrity constraint on $Y$. Then there exists a greatest consistent specialization $S_{\cal I}$ of $S$ with respect to $\cal I$. Moreover, $S_{\cal I}$ is uniquely determined (up to semantic equivalence) by $S$ and $\cal I$.

\end{theorem}

\begin{proof}

Let $\cal T$ be the set of $Y$-operations $T$ satisfying (in place of
$S_{\cal I}$ the properties (i) -- (iii) of Definition \ref{def-gcs} and let
$S_{\cal I} \; = \; \bigsqcup\limits_{T \in {\cal T}} \; T$. By definition of
a least upper bound $S_{\cal I}$ satisfies properties (i), (ii) and (iv).
Property (iii) follows from Lemma \ref{lemma-supremum}(i). \qed

\end{proof}

\noindent
Although Theorem \ref{existence-theorem} states that there is always a (unique) solution of the integrity enforcement problem, it does not help us in constructing a GCS, since its proof is non-constructive. Another general problem is that there are usually more than just one static integrity constraint. If we successively build GCSs, can we guarantee that the final result will be independent of the order of constraints? Is the final result the same, if we simply take the conjunction of all constraints? We address these two problems next.

\begin{theorem} \label{commutativity-theorem}

Let ${\cal I}_1$ and ${\cal I}_2$ be static constraints on $Y_1$ and $Y_2$ respectively. If for any operation $S$ the GCS with respect to ${\cal I}_i$ is denoted by $S_{{\cal I}_i}$ ($i = 1,2$), then for any $X$-command with $X \subseteq Y_1 \cap Y_2$ the GCSs ${( S_{{\cal I}_1} )}_{{\cal I}_2}$ and ${( S_{{\cal I}_2} )}_{{\cal I}_1}$ are semantically equivalent.

\end{theorem}

\begin{proof}

For symmetric reasons it is sufficient to show 
\[ {( S_{{\cal I}_1} )}_{{\cal
I}_2} \; \sqsubseteq \; {( S_{{\cal I}_2} )}_{{\cal
I}_1} \enspace . \]

\noindent
We have $\; {\cal I}_2 \; \Rightarrow \; wlp({( S_{{\cal I}_1} )}_{{\cal
I}_2})({{\cal I}_2}) \enspace $. Because of the transitivity of the
implication ${( S_{{\cal I}_1} )}_{{\cal
I}_2}$ then satisfies properties (i) -- (iii) with respect to $S$ and ${\cal
I}_2$, hence by property (iv) we get ${( S_{{\cal I}_1} )}_{{\cal
I}_2} \; \sqsubseteq \; S_{{\cal I}_2} \enspace $. We have

\[ {\cal I}_1 \; \Rightarrow \; wlp(S_{{\cal I}_1})({{\cal I}_1})
\; \Rightarrow \; wlp({( S_{{\cal I}_1} )}_{{\cal I}_2})({{\cal I}_1})
\enspace . \]

\noindent
The first implication is the consistency of $S_{{\cal I}_1}$ with respect
to ${\cal I}_1$, the second implication follows from property (i) for ${(
S_{{\cal I}_1} )}_{{\cal I}_2}$ with ${\cal R} = {\cal I}_1$.

Thus, ${( S_{{\cal I}_1} )}_{{\cal I}_2}$ satisfies properties (i) --(iii)
with respect to $S_{{\cal I}_2}$ and ${\cal I}_1$, i.e. 

\[ {( S_{{\cal I}_1} )}_{{\cal
I}_2} \; \sqsubseteq \; {( S_{{\cal I}_2} )}_{{\cal
I}_1} \enspace \mbox{by property (iv).} \] \qed

\end{proof}

\begin{theorem} \label{conjunctivity-theorem}

Let ${\cal I}_1$ and ${\cal I}_2$ be static constraints on $Y_1$ and $Y_2$ respectively. If for any operation $S$ the GCS with respect to ${\cal I}_i$ is denoted by $S_{{\cal I}_i}$ ($i = 1,2$), then for any $X$-command with $X \subseteq Y_1 \cap Y_2$ the GCSs ${( S_{{\cal I}_1} )}_{{\cal I}_2}$ and $S_{( {\cal I}_1 \wedge {\cal I}_2 )}$ coincide on initial states satisfying ${\cal I}_1 \wedge {\cal I}_2$, i.e., ${\cal I}_1 \wedge {\cal I}_2 \, \rightarrow \, {( S_{{\cal I}_1} )}_{{\cal I}_2}$ and ${\cal I}_1 \wedge {\cal I}_2 \, \rightarrow \, S_{( {\cal I}_1 \wedge {\cal I}_2 )}$ are semantically equivalent.

\end{theorem}

\begin{proof}

From the transitivity of the implication and Definition \ref{def-gcs} it
follows that

\[ {( S_{{\cal I}_1} )}_{{\cal I}_2} \; \sqsubseteq \; S_{{\cal I}_1 \wedge
{\cal I}_2} \enspace \mbox{holds.} \]

\noindent
Then also

\[ {\cal I}_1 \wedge
{\cal I}_2 \, \rightarrow \, {( S_{{\cal I}_1} )}_{{\cal I}_2} \; \sqsubseteq
\; {\cal I}_1 \wedge
{\cal I}_2 \, \rightarrow \, S_{{\cal I}_1 \wedge {\cal I}_2} \enspace
\mbox{holds.} \]

\noindent
We have to show the converse. Let 

\[ \bar{S}_{{\cal I}_1} \; = \; {\cal I}_1 \wedge
{\cal I}_2 \, \rightarrow \, S_{{\cal I}_1 \wedge {\cal I}_2} \; \crossbox \;
S_{{\cal I}_1} \enspace . \]

Then we get $wlp(S)({\cal R}) \Rightarrow wlp(\bar{S}_{{\cal I}_1})({\cal
R})$ and $wp(S)({\cal R}) \Rightarrow wp(\bar{S}_{{\cal I}_1})({\cal
R})$ for all formulae $\cal R$ with $fr({\cal R}) \subseteq X$.

Moreover, ${\cal I}_1 \Rightarrow wlp(\bar{S}_{{\cal I}_1})({\cal
I}_1)$ holds, hence by Definition \ref{def-gcs} it follows
that
$\bar{S}_{{\cal I}_1} \sqsubseteq S_{{\cal I}_1} \enspace .$

If we define 

\[ \bar{S}_{{\cal I}_1,{\cal I}_2} \; = \; {\cal I}_2 \, \rightarrow \,
\bar{S}_{{\cal I}_1} \; \crossbox \; {( S_{{\cal I}_1} )}_{{\cal I}_2} \enspace
, \]

\noindent
then by analogous arguments we derive $\bar{S}_{{\cal I}_1,{\cal I}_2} \;
\sqsubseteq \; {( S_{{\cal I}_1} )}_{{\cal I}_2}$. In particular we conclude

\[ {\cal I}_1 \wedge
{\cal I}_2 \, \rightarrow \, \bar{S}_{{\cal I}_1,{\cal I}_2} \;
\sqsubseteq \; {\cal I}_1 \wedge
{\cal I}_2 \, \rightarrow \, {( S_{{\cal I}_1} )}_{{\cal I}_2} \enspace , \]

but ${\cal I}_1 \wedge
{\cal I}_2 \, \rightarrow \, \bar{S}_{{\cal I}_1,{\cal I}_2}$ is semantically
equivalent to ${\cal I}_1 \wedge
{\cal I}_2 \, \rightarrow \, \bar{S}_{{\cal I}_1}$ and this to ${\cal I}_1 \wedge
{\cal I}_2 \, \rightarrow \, {( S_{{\cal I}_1} )}_{{\cal I}_2}$. Hence the
theorem. \qed

\end{proof}

\noindent
In Section \ref{classes} we required methods on subclasses that
override inherited methods to be specializations. Since we regard methods as
operations on some state space defined by the schema, the problem occurs,
whether the GCS of a specialized operation $T$ of $S$ remains to be a
specialization of the GCS of $S$. Fortunately this is also true.

\begin{theorem} \label{inheritance-theorem}

Let $S_{\cal I}$ be the GCS of the $X$-operation $S$ with respect to
the static integrity constraint $\cal I$ defined on $Y$ with $X \subseteq Y$.
Let $T$ be a $Z$-operation that specializes $S$. If $\cal I$ is regarded as a
constraint on $Y \cup Z$, then the GCS $T_{\cal I}$ of $T$ with respect to
$\cal I$ is a specialization of $S_{\cal I}$.

\end{theorem}

\begin{proof}

From the transitivity of the implication and the consistency of $T_{\cal I}$
with respect to $\cal I$ it follows that $T_{\cal I}$ satisfies properties
(i) -- (iii) of Definition \ref{def-gcs}, hence $T_{\cal I} \sqsubseteq
S_{\cal I}$. \qed

\end{proof}

\noindent
In Section \ref{classes} methods were introduced as deterministic guarded commands. Hence the question whether this property is preserved under GCS construction. Unfortunately this is not true as the following example shows.

\begin{example} \label{bsp-deterministic}

Let $x$, $y$ and $z$ be state variables, all of type $FSETS(T)$, where
$FSETS(\alpha)$ is the finite set constructor (see e.g. \cite{iwsds}) and $T$
is any value type. Let $X = \{ y \}$ and $Y = \{ x,y,z \}$. Then we define an
$X$-operation $S$ by
\begin{eqnarray*}
&& S ( t :: T ) \;== \; \; y^\prime :: FSET(T) \, \mid \\
&& \hspace*{15pt} y =
Union(y^\prime,Single(t)) \wedge member(t,y^\prime) = false \; \rightarrow \;
y := y^\prime
\end{eqnarray*}

\noindent
and a static constraint $\cal I$ on $Y$ by

\[ x = Union(y,z) \; \wedge \; \forall t :: T . member(t,y) = true
\Rightarrow member(t,z) = false \enspace . \]

\noindent
Then the GCS $S_{\cal I}$ has the form
\begin{eqnarray*}
&& S_{\cal I} ( t :: T ) \; == \; \; {\cal I} \; \rightarrow S(t) \; ;\\
&& \hspace*{20pt} ( \, z := Union(z,Single(t) \; \Box\\
&& \hspace*{25pt} x^\prime �� FSET(T) \, \mid \, x =
Union(x^\prime,Single(t)) \wedge member(t,x^\prime) = false \;
\rightarrow\\
&& \hspace*{55pt} x \; := \; x^\prime \; ) \; \crossbox \; S(t)
\enspace .
\end{eqnarray*}

\noindent
We omit the formal proof of the properties of Definition \ref{def-gcs}. \qed

\end{example}

\noindent
A general approach to remove non-determinism is {\em operational
refinement} as defined in \cite{iwsds}. However, operational refinement
allows to ``complete'' a specification of an operation $S$ whenever $S$ is
undefined are never terminating. In this paper we do not regard completion via
refinement. Therefore, we regard the notion of specialization instead.
Due to \cite[Proposition 4.1]{iwsds} it is easy to see that whenever $S$
is consistent with respect to a static constraint $\cal I$, then each
specialization $T$ of $S$ does so, too. 

Hence a
deterministic specialization of $S_{\cal I}$ is still a consistent
specialization of $S$ with respect to $\cal I$. The
next theorem states that we can choose a maximal one.

\begin{theorem} \label{refinement-theorem2}

Let $S_{\cal I}$ be the GCS of a deterministic operation $S$ with respect
to the static constraint $\cal I$ and let $T$ be some deterministic
specialization of $S_{\cal I}$. Then $T$ specializes $S$. Moreover, if
$T^\prime$ is any deterministic specialization of $S$ that is consistent with
respect to $\cal I$, then $T^\prime$ also specializes some deterministic
specialization $T$ of $S_{\cal I}$.

\end{theorem}

\begin{proof}

The first statement is trivial, since $\sqsubseteq$ is a partial order.

If $T^\prime$ is a deterministic specialization of $S$ consistent with
respect to $\cal I$, then according to Definition \ref{def-gcs} $T^\prime$
must be a specialization of $S_{\cal I}$, hence the second statement. \qed

\end{proof}

\section{Enforcing Static Integrity in the OODM} \label{oodm-integrity}

Let us now apply the results of Section \ref{stat-gcs} to the OODM presented in Section \ref{fundamentals}. In this section we restrict ourselves to the basic update operations of Theorem \ref{icdt-theorem} and describe the structure of their GCSs with respect to distinguished classes of static constraints. Moreover, we discuss whether the general problem of GCS construction could be reduced to these basic operations. Unfortunately this is not true.

\subsection{Distinguished Classes of Static Constraints} \label{constraints}

Let us now introduce some kinds of explicit static constraints are generalizations of constraints known from the relational
model, e.g. functional and key constraints, general inclusion
and exclusion constraints, multi-valued dependencies and path constraints.

\begin{definition} \label{explicit}

\ Let $C, C_1, C_2$ be classes in a schema $\cal S$ and let $c^i : T_C \rightarrow T_i$ ($ i = 1,2,3$) and $c_i : T_{C_i} \rightarrow T$ ($i = 1,2$) be functions.

\begin{enumerate}

\item A {\em functional constraint} on $C$ is a constraint of the form
\begin{eqnarray*}
&& \hspace*{-20pt} \forall i,i^\prime :: ID . \, \forall v,v^\prime :: T_C . \; c^1(v) = c^1(v^\prime) \, \wedge \, member(Pair(i,v),x_C) = true
\end{eqnarray*}
\begin{equation}
\hspace*{20pt} \wedge \, member(Pair(i^\prime,v^\prime),x_C) = true \, \Rightarrow \, c^2(v) = c^2(v^\prime) \enspace .
\end{equation}

\noindent
A functional constraint is called a {\em value constraint} iff neither $T_1$ nor $T_2$ contains $ID$.

\item A {\em uniqueness constraint} on $C$ is a constraint of the form
\begin{eqnarray*}
&& \hspace*{-20pt} \forall i,i^\prime :: ID . \, \forall v,v^\prime :: T_C . \; c^1(v) = c^1(v^\prime) \, \wedge \, member(Pair(i,v),x_C) = true
\end{eqnarray*}
\begin{equation}
\hspace*{20pt} \wedge \, member(Pair(i^\prime,v^\prime),x_C) = true \, \Rightarrow \, i = i^\prime \enspace .
\end{equation}

\noindent
A uniqueness constraint on $C$ is called {\em trivial} iff $T_C = T_1$ and $c^1 = id$ hold.

\item A {\em general inclusion constraint} on $C_1$ and $C_2$ is a constraint of the form
\begin{eqnarray*}
&& \hspace*{-20pt} \forall t :: T . \, \exists i_1 :: ID , v_1 :: T_{C_1} . \, member(Pair(i_1,v_1),x_{C_1}) = true \, \wedge \, c_1(v_1) = t
\end{eqnarray*}
\begin{equation}
\hspace*{-10pt} \Rightarrow \; \exists i_2 :: ID , v_2 :: T_{C_2} . \, member(Pair(i_2,v_2),x_{C_2}) = true \, \wedge \, c_2 (v_2) = t .
\end{equation}

\item An {\em exclusion constraint} on $C_1$, $C_2$ is a constraint of the form 
\begin{eqnarray*}
&& \hspace*{-20pt} \forall i_1,i_2 :: ID . \, \forall v_1 :: T_{C_1} . \, \forall v_2 :: T_{C_2} . \, member(Pair(i_1,v_1),x_{C_1}) = true
\end{eqnarray*}
\begin{equation}
\wedge \, member(Pair(i_2,v_2),x_{C_2}) = true \; \Rightarrow \; c_1(v_1) \neq c_2(v_2) \enspace .
\end{equation}

\item An {\em object generating constraint} on $C$ is a constraint of the form
\begin{eqnarray*}
&& \hspace*{-20pt} \forall i_1,i_2 :: ID . \, \forall v_1,v_2 :: T_C . \; member(Pair(i_1,v_1),x_C) = true \, \wedge \\
&& member(Pair(i_2,v_2),x_C) = true \, \wedge \, c^1(v_1) = c^1(v_2) \; \Rightarrow\\
&& \hspace*{20pt} \exists i :: ID , v :: T_C . \, member(Pair(i,v),x_C) = true \, \wedge
\end{eqnarray*}
\begin{equation}
\hspace*{40pt} c^1(v) = c^1(v_1) \, \wedge \, c^2(v) = c^2(v_1) \, \wedge \, c^3(v) = c^3(v_2) \enspace .
\end{equation}

\end{enumerate}

\end{definition}

\noindent
Note that the definition of uniqueness constraints is a generalization of the key concept and object generating constraints are a straightforward generalization of multi-valued dependencies in the
relational model \cite{key,tha88}. The following definition extends these
constraints to path constraints.

\begin{definition} \label{path}

\begin{enumerate}

\item Let $C_1 , \ldots , C_n$be classes in a schema $\cal S$ with representation types $T_{C_1} , \ldots , T_{C_n}$ and let referential constraints on $C_{i-1} , C_i$ be defined via $o_i : T_{C_{i-1}} \times ID \rightarrow BOOL$. 
Then $C_1 , \ldots , C_n$ define a {\em path} in $\cal S$ and the corresponding {\em path expression} is given by
\begin{eqnarray*}
&& member(Pair(i_1,v_1),x_{C_1}) = true \wedge o_2(v_1,i_2) = true \wedge \\
&& \hspace*{20pt} member(Pair(i_2,v_2),x_{C_2}) = true \wedge \ldots \wedge o_n(v_{n-1},i_n) = true \wedge
\end{eqnarray*}
\begin{equation}
\hspace*{40pt} member(Pair(i_n,v_n),x_{C_n}) = true \enspace .
\end{equation}

\item Let $C$, $C^\prime$ be classes in a schema $\cal S$ and let $\cal P$ be a \{ (general) inclusion $\mid$ exclusion $\mid$ functional $\mid$ uniqueness $\mid$ object generating \} constraint on $C$, $C^\prime$ or $C$ respectively. If $C_1 , \ldots , C_n$ and $C_1^\prime , \ldots , C_m^\prime$ are paths in $\cal S$ with $C_n = C$ and $C_m^\prime = C^\prime$, then replacing the corresponding path expressions for $member(Pair(i,v),x_C) = true$ and $member(Pair(i^\prime,v^\prime),x_{C^\prime}) = true$ respectively in $\cal P$ defines a {\em path constraint} ${\cal P}^\prime$ on $C_1$ and $C_1^\prime$. We assume all free variables in ${\cal P}^\prime$ other than $x_C$ and $x_{C^\prime}$ to be universally quantified. More precisely we call ${\cal P}^\prime$ a \{ {\em (general) path inclusion $\mid$ path exclusion $\mid$ path functional $\mid$ path uniqueness $\mid$ path object generating} \} {\em constraint}.

\end{enumerate}

\end{definition}

\subsection{Transforming Static Constraints into Primitive Operations}

Let us now try to generalize the result of theorem \ref{icdt-theorem} with respect to explicit static constraints. Let $\cal S$ be some schema and let $\cal I$ be an explicit static constraint on $\cal S$. We want to derive again insert-, delete- and update-operations for each class $C$ in $\cal S$ such that these are consistent with respect to $\cal I$. Based on the Conjunctivity Theorem \ref{conjunctivity-theorem} we only approach the problem separately for the classes of constraints introduced in the previous subsection.

Moreover, we apply a specific kind of operational refinement in order to reduce the non-determinism of the resulting GCS. Whenever an arbitrary value of some proper value type is required, then we extend the input-type. However, this can not be applied to reduce the non-determinism arising from choice operations. In general, there exists a {\em choice normal form} for the GCS such that its components are the maximal deterministic operational refinements of the GCS that exist by Theorem \ref{refinement-theorem2}. 

In the following we restrict ourselves to the case of a single explicit constraint in addition to the one (trivial) uniqueness constraint that is required to assure value-representability and that has been used in \cite{icdt} to construct {\em canonical update operations}. Then we look at an example with more than one constraint. We illustrate that although Theorem \ref{conjunctivity-theorem} holds, the structure of $S_{({\cal I}_1 \wedge {\cal I}_2)}$ may be not at all obvious.

\subsubsection{General (Path) Inclusion Constraints.}

Let $\cal I$ be a general inclusion constraint on $C_1$, $C_2$ defined via $c_i : T_{C_i} \rightarrow T$ ($i = 1,2$). Then each insertion into $C_1$ requires an additional insertion into $C_2$ whereas a deletion on $C_2$ requires a deletion on $C_1$. Update on one of the $C_i$ requires an additional update on the other class.

Let us first concentrate on the insert-operation on $C_1$ (for an insert on $C_2$ there is nothing to do). Insertion into $C_1$ requires an input-value of type $V_{C_1}$; an additional insert on $C_2$ then requires an input-value of type $V_{C_2}$. However, these input-values are not independent, because the corresponding values of type $T_{C_1}$ and $T_{C_2}$ must satisfy the general inclusion constraint. Therefore we first show that the constraint can be ``lifted'' to a constraint on the value-representation types. Note that this is similar to the handling of IsA-constraints \cite[Lemma 29]{icdt}.

\begin{lemma} \label{inclusion-type-lemma}

Let $C_1$, $C_2$ be classes, $c_i : T_{C_i} \rightarrow T$ functions and let
$V_{C_i}$ be the value-representation type of $C_i$ ($i = 1,2$). Then there
exist functions $f_i : V_{C_i} \rightarrow T$ such that for all database
instances $\cal D$

\begin{equation}
f_1(d_1^{\cal D}(v_1)) = f_2(d_2^{\cal D}(v_2)) \; \Leftrightarrow \; c_1(v_1)
= c_2(v_2) \end{equation}

\noindent
for all $v_i \in codom_{\cal D}(x_{C_i})$ ($i = 1,2$) holds. Here $d_i^{\cal D} : T_{C_i} \rightarrow V_{C_i}$ denotes the function used in the uniqueness constraint on $C_i$ with respect to $\cal D$.

\end{lemma}

\begin{proof}

Due to Definition \ref{def-valuerep} we may define $f_i \; = \; c_i \circ (
d_i^{\cal D} )^{-1}$ on $c_i(codom_{\cal D}(x_{C_i}))$ ($i = 1,2$).

Then we have to show that this definition is independent of the instance $\cal
D$. Suppose ${\cal D}_1$, ${\cal D}_2$ are two different instances. Then
there exists a permutation $\pi$ on $ID$ such that $d_i^{{\cal D}_2} \; = \;
d_i^{{\cal D}_1} \circ \pi$, where $\pi$ is extended to $T_{C_i}$. Then

\[ c_i \circ ( d_i^{{\cal D}_2} )^{-1} \; = \; c_i \circ \pi^{-1} \circ (
d_i^{{\cal D}_1} )^{-1} \; = \; \pi^{-1} \circ c_i \circ (
d_i^{{\cal D}_1} )^{-1} \enspace , \]

\noindent
since $c_i$ permutes with $\pi^{-1}$. Then the stated equality follows. \qed

\end{proof}

\noindent
Now let $V_{C_1,C_2}$ be a subtype of $V_{C_1} \times V_{C_2}$ defined via the
equality $f_1(v_1) = f_2(v_2)$, where $v_i :: V_{C_i}$ are the components of a
value and $f_i$ are the functions of Lemma \ref{inclusion-type-lemma}. We omit
the details. Then we can define the new insert-operation on $C_1$ by
$\; {(insert_{C_1})}_{\cal I} ( V :: V_{C_1,C_2} ) \; == $

\begin{equation} \label{17}
\hspace*{25pt}  \hspace*{25pt} insert_{C_1} (first(V)) \; ; \; insert_{C_2} (second(V)) \enspace .
\end{equation}

\noindent
Now we are able to generalize Theorem \ref{icdt-theorem} with respect to general inclusion constraint.

\begin{theorem} \label{inclusion-gcs-theorem}

Let $\cal I$ be a general inclusion constraint on $C_1$, $C_2$ defined
via $c_i : T_{C_i} \rightarrow T$ and let $S_{\cal I}$ be the insert-operation
of (\ref{17}). Suppose that $C_1$ is not referenced by $C_2$. Then $S_{\cal I}$
is the GCS of the canonical insert-operation of Theorem \ref{icdt-theorem} with
respect to $\cal I$.

\end{theorem}

\begin{proof}

We use the abbreviations $S_i = insert_{C_i} ( V_i :: V_{C_i} )$ ($i=1,2$).
Then

\[ wlp(S_{\cal I})({\cal R}) \; \equiv \; \{ V_1 / first(V) \} . wlp(S_1) (
\{ V_2 / second(V) \} . wlp(S_2) ({\cal R}) \enspace . \]

\noindent
Since $S_i$ is total and always terminating, we have $ wlp(S_i) = wp(S_i)$.
Since $C_1$ is not referenced by $C_2$, we know that $S_2$ is a $\{ x_{C_2}
\}$-operation. Therefore, $wlp(S_2)({\cal R})$ is a logical combination of
$\cal R$ without any substitution, hence $wlp(S_1)({\cal R}) \Rightarrow
wlp(S_{\cal I})({\cal R})$. This proves (i) and (ii).

In particular $wlp(S_{\cal I})({\cal I}) \; \equiv$
\begin{eqnarray*}
&& \{ \, x_{C_1} / Union(x_{C_1},Single(Pair(I_1,V_1))) \, ,\\
&& \hspace*{35pt} x_{C_2} /
Union(x_{C_2},Single(Pair(I_2,V_2))) \, \} . {\cal I}
\end{eqnarray*}

\noindent
with $I_1 , I_2 :: ID$ and $V_i :: T_{C_i}$ with $c_1(V_1) = f_1(first(V))$
and $c_2(V_2) = f_2(first(V))$, where $f_i$ are the functions of Lemma
\ref{inclusion-type-lemma}. Then property (iii) follows immediately. We omit
the proof of (iv). \qed

\end{proof}

\noindent
Note there there is no need to require $C_1 \neq C_2$.
Delete- and update-operations can be defined analogously to (\ref{17}). Then a result analogous to Theorem \ref{inclusion-gcs-theorem} holds. We omit the details here.
The generalization to path constraints is also straightforward.

\subsubsection{(Path) Functional and Uniqueness Constraints.}

Now let $\cal I$ be a functional constraint on $C$ defined via $c^1 : T_C
\rightarrow T_1$ and $c^2 : T_C \rightarrow T_2$. In this case nothing is
required for the delete operation whereas for inserts (and updates) we have to
add a postcondition. Moreover, let $c^{\cal D} : T_C \rightarrow V_C$ denote
the function associated with the value-representability of $C$ and the
database instance $\cal D$ and let all other notations be as before. Let us
again concentrate on the insert-operation. Let $insert_C^\prime$ denote the
{\em quasi-canonical insert}\/ on $C$ \cite{icdt}. Then we define
\begin{eqnarray*}
&& {( insert_C )}_{\cal I} ( V :: V_C ) \; ==\\
&& \hspace*{15pt}
I :: ID \; \mid \; I \, \leftarrow \, insert_C^\prime (V) \; ;\\
&& \hspace*{15pt}
V^\prime :: T_C \; \mid \; member(Pair(I,V^\prime),x_C) = true \;
\rightarrow\\
&& \hspace*{20pt} ( \; \forall J :: ID , W :: T_C . \; ( \,
member(Pair(J,W),x_C) = true\\
&& \hspace*{23pt} \wedge \, c^1(W) = c^1(V^\prime) \; \Rightarrow \; c^2(W) =
c^2(V^\prime) \, ) \; \; \rightarrow
\end{eqnarray*}
\begin{equation} \label{18}
\hspace*{15pt} skip 
\end{equation}

\noindent
Note that in this case there is no change of input-type.

\begin{theorem} \label{functional-gcs-theorem}

Let $\cal I$ be a functional constraint on the class $C$ defined via $c^1 : T_C
\rightarrow T_1$ and $c^2 : T_C \rightarrow T_2$ and let $S_{\cal I}$ be the
insert-operation of (\ref{18}). Then $S_{\cal I}$ is the GCS of the canonical
insert-operation on $C$ defined by Theorem \ref{icdt-theorem} with respect to
$\cal I$.

\end{theorem}

\begin{proof}

The proof is analogous to the one of Theorem \ref{inclusion-gcs-theorem}. \qed

\end{proof}

\noindent
For delete- and update-operations an analogous result holds. We omit the
details. The generalization to path constraints is also straightforward.

A uniqueness constraint defined via $c^1 : T_C \rightarrow T_1$ is equivalent
to a functional constraint defined via $c^1$ and $c^2 = id : T_C \rightarrow
T_C$ plus the trivial uniqueness constraint. Since trivial uniqueness
constraints are already enforced by the canonical update operations, there
is no need to handle separately arbitrary uniqueness constraints.

\subsubsection{(Path) Exclusion Constraints.}

The handling of exclusion constraints is analogous to the handling of
inclusion constraints. This means that an insert (update) on one class may
cause a delete on the other, whereas delete-operations remain unchanged.

We concentrate on the insert-operation. Let $\cal I$ be an exclusion
constraint on $C_1$ and $C_2$ defined via $c_i : T_{C_i} \rightarrow T$ ($i =
1,2$). Let $f_i : V_{C_i} \rightarrow T$ denote the functions from Lemma
\ref{inclusion-type-lemma}. Then we define a new insert-operation on $C_1$ by
\begin{eqnarray*}
&& {( insert_{C_1} )}_{\cal I} ( V :: V_{C_1} ) ==\\
&& \hspace*{15pt} insert_{C_1} (V) \; ;\\
&& \hspace*{15pt} \mu S . \; (( I :: ID \; \mid \, V^\prime :: T_{C_2} \,
\mid \, member(Pair(I,V^\prime),x_{C_2}) = true\\
&& \hspace*{25pt} \wedge c^2(V^\prime) = f_1(V) \; \rightarrow \;
delete_{C_2}(V^\prime) \; ; \; S \; )
\end{eqnarray*}

\begin{equation} \label{19}
\hspace{15pt} \crossbox \; skip \; ) \enspace .
\end{equation}

\begin{theorem} \label{exclusion-gcs-theorem}

Let $\cal I$ be an exclusion constraint on the classes $C_1$ and $C_2$ defined
via $c_i : T_{C_i} \rightarrow T$ ($i = 1,2$) and let
$S_{\cal I}$ be the insert-operation of (\ref{19}). Then $S_{\cal I}$ is the
GCS of the canonical insert-operation on $C_1$ defined by Theorem
\ref{icdt-theorem} with respect to $\cal I$.

\end{theorem}

\begin{proof}

The proof is analogous to the one of Theorem \ref{inclusion-gcs-theorem}. \qed

\end{proof}

\noindent
For delete- and update-operations an analogous result holds. We omit the
details. The generalization to path constraints is also straightforward.

\subsubsection{(Path) Object Generating Constraints.}

Let $\cal I$ be an object generating constraint on a class $C$ defined via
the functions $c^i : T_C \rightarrow T_i$ ($i = 1,2,3$). Then integrity
enforcement requires to add additional inserts (deletes, updates) to each
insert- (delete-, update-) operation. Let us illustrate the new
insert-operation. The handling of delete and update-operations is analogous.
As in the case of inclusion constraints we need a preliminary lemma.

\begin{lemma} \label{generating-type-lemma}

Let $c^i : T_C \rightarrow T_i$ be functions ($i = 1,2,3$) such that $c^1
\times c^2 \times c^3$ defines a uniqueness constraint on the class $C$. Then
there exist functions $f_i : V_C \rightarrow T_i$ such that $c^i = f_i \circ
c^{\cal D}$ holds for all instances $\cal D$, where $c^{\cal D} : T_C
\rightarrow V_C$ corresponds to the value-representability of $C$.

\end{lemma}

\begin{proof}

Since $c^1 \times c^2 \times c^3$ defines a uniqueness constraint on $C$, it
follows from Definition \ref{def-valuerep} that there exists some $f : V_C
\rightarrow T_1 \times T_2 \times T_3$ with $c^1 \times c^2 \times c^3 = f
\circ c^{\cal D}$. Then $f_i = \pi_i \circ f$, where $\pi_i$ is the
projection to $T_i$ ($i = 1,2,3$), satisfy the required property. \qed

\end{proof}

\noindent
Then we define a new insert-operation on $C$ as follows:
\begin{eqnarray*}
&& {( insert_C )}_{\cal I} ( V :: V_C ) \; == \\ 
&& \hspace*{15pt} \exists I^\prime :: ID , V^\prime :: T_C . \,
member(Pair(I^\prime,V^\prime),x_C) = true \\
&& \hspace*{50pt} \wedge \, c^1(V^\prime) = f_1(V)
\; \rightarrow\\ 
&& \hspace*{25pt} ( \, ( \, V^{\prime\prime} :: V_C \, \mid \,
f_1(V^{\prime\prime}) = f_1(V) \, \wedge \, f_2(V^{\prime\prime}) = f_2(V)
\\
&& \hspace*{40pt} \wedge \, f_3(V^{\prime\prime}) = c^3(V^\prime) \;
\rightarrow \; insert_C(V^{\prime\prime}) \, ) \; ;\\
&& \hspace*{25pt} \, \, ( \, V^{\prime\prime\prime} :: V_C \, \mid \,
f_1(V^{\prime\prime\prime}) = f_1(V) \, \wedge \,
f_2(V^{\prime\prime\prime}) = c^2(V^\prime) \, \wedge \\ 
&& \hspace*{40pt} f_3(V^{\prime\prime\prime}) = f_3(V) \; \rightarrow
\; insert_C(V^{\prime\prime\prime}) \, ) \, )\; ;\\
&& \hspace*{25pt} \crossbox \; skip \; ) \; ;
\end{eqnarray*}

\begin{equation} \label{20} 
\hspace*{15pt} insert_C(V) 
\end{equation}

\begin{theorem} \label{generating-gcs-theorem}

Let $\cal I$ be an object generating constraint on a class $C$ defined via
the functions $c^i : T_C \rightarrow T_i$ ($i = 1,2,3$) such that $c^1
\times c^2 \times c^3$ defines a uniqueness constraint on the class $C$ and let
$S_{\cal I}$ be the insert-operation of (\ref{20}). Then $S_{\cal I}$ is the
GCS of the canonical insert-operation on $C$ with respect to $\cal I$.

\end{theorem}

\begin{proof}

The proof is analogous to the one of Theorem \ref{inclusion-gcs-theorem}. \qed

\end{proof}

\noindent
For delete- and update-operations an analogous result holds. We omit the
details. The generalization to path constraints is also straightforward.

\begin{theorem} \label{theorem-explicit-constraints}

\ Let $\cal S$ be a schema such that each class $C$ in $\cal S$ is
value representable. Suppose all explicit constraints in $\cal S$ are general
inclusion constraints, exclusion constraints, functional constraints,
uniqueness constraints, object generating constraints and path constraints.
Then there exist generic update methods $insert_C$, $delete_C$ and $update_C$
for each class $C$ in $\cal S$ that are consistent with respect to all
implicit and explicit static constraints on $\cal S$.

\end{theorem}

\begin{proof}

The result has been shown above in the Theorems
\ref{inclusion-gcs-theorem}--\ref{generating-gcs-theorem} for a single explicit
constraint. Then the general result follows from Theorem
\ref{conjunctivity-theorem}. \qed

\end{proof}

\subsection{Transforming Static Constraints into Transactions}

Let us now consider the case of arbitrary methods which can be used to
model transactions. We concentrate on the question whether it is possible to
achieve general consistent methods as combinations of consistent primitive
operations as e.g. given by Theorem \ref{theorem-explicit-constraints}. Regard
the following simple example:

\begin{example} \label{bsp-account} \

\noindent
{\sc AccountClass} ==\\
\indent {\tt Structure} TRIPLE(PERSON,NAT,NAT)\\
{\tt End} {\sc AccountClass}\\

\noindent
{\tt Constraints} \\
\indent $Pair(I,V) \in \mbox{\sc AccountClass} \, \Rightarrow \, second(V) + third(V) \geq 0$\\
\indent $Pair(I,V) \in \mbox{\sc AccountClass} \, \wedge \, Pair(I^\prime,V^\prime) \in \mbox{\sc AccountClass} \, \wedge $\\
\hspace*{35pt} $first(V) = first(V^\prime) \, \Rightarrow \, I = I^\prime$\\

The second component gives the account of a person and the third component gives his/her credit limit. Let
\begin{eqnarray*}
&& transfer (P_1 :: PERSON , P_2 :: PERSON , T :: NAT) \; ==\\
&& \hspace*{20pt} I_1,I_2 :: ID , N_1,N_2,M_1,M_2 :: NAT \, \mid \\
&& \hspace*{60pt} Pair(I_1,Triple(P_1,N_1,M_1)) \in \mbox{\sc AccountClass} \wedge \\
&& \hspace*{60pt} Pair(I_2,Triple(P_2,N_2,M_2)) \in \mbox{\sc AccountClass} \; \rightarrow\\
&& \hspace*{40pt} update_{AccountClass} (P_1,Triple(P_1,N_1-T,M_1)) \, ; \\
&& \hspace*{40pt} update_{AccountClass} (P_2,Triple(P_2,N_2+T,M_2))
\end{eqnarray*}

\noindent
In this case the precondition to be added is simply the weakest precondition, i.e. $N_1 + M_1 - T \geq 0$. Now regard the operation
\[ S = transfer(P_1,P_2,T_1) \, ; \, transfer(P_2,P_1,T_2) \enspace . \]
\noindent
The precondition to be added to $S$ in order to enforce the first constraint simply is $N_1 + M_1 - T_1 + T_2 \geq 0 \wedge N_2 + M_2 - T_2 + T_1 \geq 0$, which is trivially satisfied if $T_1 = T_2$. However, for large values of $T_1 = T_2$ this condition is weaker then adding three precondition separately. \qed

\end{example}

\begin{theorem}

\ Let $S$ be a method and let $S_1 \ldots S_n$ be canonical update
operations on a schema $\cal S$ occurring within $S$. Let $S^\prime$ result
from $S$ by replacing each $S_i$ by its GCS ${(S_i)}_{\cal I}$ with respect to
some static constraint $\cal I$. Then $S_{\cal I}$ and $S^\prime$ are in
general not semantically equivalent.

\end{theorem}

\begin{proof}

\ A counterexample has been given in Example \ref{bsp-account}. \qed

\end{proof}

\noindent
As a consequence of this theorem it is  even not sufficient to know
explicitly the GCS of basic update operations with respect to a single
constraint. Although Theorem \ref{conjunctivity-theorem} allows the GCS with
respect to more than one constraint to be built successively, we have
seen in Theorems \ref{inclusion-gcs-theorem}--\ref{generating-gcs-theorem}
that the GCS with respect to one constraint is no longer a basic update
operation. Let us illustrate this open problem by a simple example.

\begin{example} \label{bsp-inclusio-exclusion}

\ Let $C_1$, $C_2$, $C_3$ be classes and $c_i : T_{C_i} \rightarrow T$ ($i =
1,2,3$) be functions and suppose there are defined

\begin{itemize}

\item a general inclusion constraint ${\cal I}_1$ on $C_1$ and $C_2$ via
$c_1$ and $c_2$,

\item a general inclusion constraint ${\cal I}_2$ on $C_1$ and $C_3$ via
$c_1$ and $c_3$ and

\item an exclusion constraint ${\cal I}_3$ on $C_2$ and $C_3$ via
$c_2$ and $c_3$.

\end{itemize}

\noindent
Clearly, the GCS of the insert-operation on $C_1$ with respect to ${\cal I}_1
\wedge {\cal I}_2 \wedge {\cal I}_3$ is $fail$, which is hard to build
successively. \qed

\end{example}

\section{Enforcing Transition Integrity} \label{dynamic}

In Section \ref{enforcement} we discussed integrity enforcement in a general framework with respect to static constraints. Let us now try to generalize the results for transition constraints. Thus, let $S$ be an $X$-operation and $\cal J$ a transition constraint on $Y$ with $X \subseteq Y$. The idea is again to construct a ``new'' $Y$-operation $S_{\cal J}$ that is consistent with respect to $\cal J$ and specializes $S$. Again this leads to the idea to construct a {\em Greatest Consistent Specialization} of $S$ with respect to $\cal J$. The difference to the case of static constraints is the use of a different proof obligation for consistency according to Definition \ref{cons}.

\subsection{GCSs with Respect to Transition Constraints} \label{dyn-gcs}

We start giving a formal definition of a {\em Greatest Consistent Specialization}\/ (GCS) of an operation $S$ with respect to a transition constraint $\cal J$.

\begin{definition} \label{def-gcs-dyn}

Let $X \subseteq Y$ be state spaces, $S$ an $X$-operation and $\cal J$ a transition integrity constraint on $Y$. A $Y$-operation $S_{\cal J}$ is a {\em Greatest Consistent Specialization}\/ (GCS) of $S$ with respect to $\cal J$ iff 

\begin{enumerate}

\item $wlp(S)({\cal R}) \; \Rightarrow \; wlp(S_{\cal J})({\cal R}) \;$ holds on $Y$ for all formulae $\cal R$ with $fr({\cal R}) \subseteq X$,

\item $wp(S)(true) \; \Rightarrow \; wp(S_{\cal J})(true) \;$ holds on
$Y$, 

\item $wlp(\Phi({\cal J}))({\cal R}) \; \Rightarrow \; wlp(S_{\cal J})({\cal R}) \enspace$ holds on $Y$ for all formulae $\cal R$ with $fr({\cal R}) \subseteq Y$ and

\item for each $Y$-operation $T$ satisfying properties (i) -- (iv) (instead of $S_{\cal J}$) we have

\begin{enumerate}

\item $wlp(S_{\cal J})({\cal R}) \; \Rightarrow \; wlp(T)({\cal R}) \;$
for
all formulae $\cal R$ with $fr({\cal R}) \subseteq X$ and

\item $wp(S_{\cal J})(true) \; \Rightarrow \; wp(T)(true) \enspace .$

\end{enumerate}

\end{enumerate}

\end{definition}

\noindent
Note that properties (i), (ii) and (iii) say that $S_{\cal J} \, \sqsubseteq
\, S$, where $\sqsubseteq$ is the specialization order of Definition
\ref{nelson-order}. Property (iv) requires $S_{\cal J}$ to be consistent with
respect to the constraint $\cal J$. Finally, property (v) states that each
consistent specialization $T$ of $S$ with $T \, \sqsubseteq \, S$ also
specializes $S_{\cal J}$. 

Based on this formal definition of a GCS we can now raise the same questions as in the static case. Before we state the result on the (unique) existence of GCSs, let us first examine the relation between static and transition constraints. Suppose $\cal I$ is a static constraint on $Y$, then we may regard $\cal I$ also as a transition constraint. Let ${\cal I}^\prime$ result from $\cal I$ by replacing each state variable $x_i$ occurring freely in $\cal I$ by $x_i^\prime$. Then $\cal I \, \Rightarrow \, I^\prime$ defines the {\em corresponding transition constraint} denoted as ${\cal J}_{\cal I}$. Then we know that consistency with respect to $\cal I$ is equivalent to consistency with respect to ${\cal J}_{\cal I}$. This implies the following result:

\begin{theorem} \label{gcs-stat-dyn}

Let $S$ be an $X$-operation and $\cal I$ a static constraint on $Y$ with $X \subseteq Y$. If $S_{\cal I}$ and $S_{{\cal J}_{\cal I}}$ are the GCSs of $S$ with respect to $\cal I$ and the transition constraint ${\cal J}_{\cal I}$ respectively, then these two GCSs are semantically equivalent.

\end{theorem}

\begin{proof}

This follows directly from Definitions \ref{def-gcs} and \ref{def-gcs-dyn}. Using the equivalence of consistency proof obligations with respect to $\cal I$ and ${\cal J}_{\cal I}$ implies the two definitions to coincide. \qed

\end{proof}

\noindent
Next, we are able to proof the (unique) existence of a GCS also for transition constraints. As in the static case the proof will be non-constructive, hence does not help to construct a GCS.

\begin{theorem} \label{existence-theorem-dyn}

Let $S$ be an $X$-operation, $X \subseteq Y$ and $\cal J$ a transition integrity constraint on $Y$. Then there exists a greatest consistent specialization $S_{\cal J}$ of $S$ with respect to $\cal J$. Moreover, $S_{\cal J}$ is uniquely determined (up to semantic equivalence) by $S$ and $\cal J$.

\end{theorem}

\begin{proof}

The proof is analogous to the one of Theorem \ref{existence-theorem}. \qed

\end{proof}

\subsection{Compatibility Results} \label{dyn-compatibility}

Let us now address the compatibility problems with respect to the conjunction of constraints, inheritance and refinement. Note that due to Theorem \ref{gcs-stat-dyn} some of the results in Section \ref{stat-gcs} occur as special cases of the results here.

\begin{theorem} \label{commutativity-theorem-dyn}

Let ${\cal J}_1$ and ${\cal J}_2$ be transition constraints on $Y_1$ and $Y_2$ respectively. If for any operation $S$ the GCS with respect to ${\cal J}_i$ is denoted by $S_{{\cal J}_i}$ ($i = 1,2$), then for any $X$-command $S$ with $X \subseteq Y_1 \cap Y_2$ the GCSs ${( S_{{\cal J}_1} )}_{{\cal J}_2}$ and ${( S_{{\cal J}_2} )}_{{\cal J}_1}$ are semantically equivalent.

\end{theorem}

\begin{proof}

The proof is analogous to Theorem \ref{commutativity-theorem}. \qed

\end{proof}

\begin{theorem} \label{inheritance-theorem-dyn}

Let $S_{\cal J}$ be the GCS of the $X$-operation $S$ with respect to the transition constraint $\cal J$ defined on $Y$ with $X \subseteq Y$. Let $T$ be a $Z$-operation that specializes $S$. If $\cal J$ is regarded as a constraint on $Y \cup Z$, then the GCS $T_{\cal J}$ of $T$ with respect to $\cal J$ is a specialization of $S_{\cal J}$.

\end{theorem}

\begin{proof}

The proof is analogous to the one of Theorem \ref{inheritance-theorem}. \qed

\end{proof}

\begin{theorem} \label{deterministic-theorem}

The GCS $S_{\cal J}$ of a deterministic $X$-operation $S$ with respect to a transition constraint $\cal J$ is in general non-deterministic.

\end{theorem}

\begin{proof}

This follows from Theorem \ref{gcs-stat-dyn}, since determinism is not even preserved by GCSs with respect to static constraints as shown by the counter-example in Example \ref{bsp-deterministic}. \qed

\end{proof}

\noindent
Hence the problem remains to remove the non-determinism. Due to
\cite[Proposition 4.2]{iwsds} it is easy to see that whenever $S$ is
consistent with respect to a transition constraint $\cal J$, then each
specialization $T$ of $S$ does so, too.

\begin{theorem} \label{refinement-theorem2-dyn}

Let $S_{\cal J}$ be the GCS of a deterministic operation $S$ with respect to the transition constraint $\cal J$ and let $T$ be some deterministic operational refinement of $S_{\cal J}$. Then $T$ specializes $S$. Moreover, if $T^\prime$ is any deterministic specialization of $S$ that is consistent with respect to $\cal J$, then $T^\prime$ also specializes some deterministic operational refinement $T$ of $S_{\cal J}$.

\end{theorem}

\begin{proof}

The proof is analogous to Theorem \ref{refinement-theorem2}.
\qed

\end{proof}

\section{Conclusion} \label{open}

In this paper we addressed the problem of integrity enforcement in object-oriented databases. First we introduced a formally defined object-oriented datamodel (OODM) that includes inclusion and referential constraints implicitly in a schema and allows in particular explicit static and transition constraints to be defined. We gave formally defined general proof obligations for static and transition consistency. Using a general purpose theorem prover to prove these formulae gives a verification based approach to consistency.

However, the verification approach does not help in writing consistent methods. Hence the idea to replace each update operation (methods in the OODM) by a {\em Greatest Consistent Specialization}\/ (GCS). We show that such GCSs always exist and are uniquely determined by the operation and the constraints up to semantic equivalence. Moreover, they are compatible with the conjunction of constraints, inheritance and refinement.
%Unfortunately, a GCS in general is non-deterministic, but a suitable maximal deterministic 
%branch can be selected via refinement.

An unsolved open problem is the general structure of a GCS including the problem of its computation. One idea is to exploit the structure of a constraint that must involve constructor- and selector-expressions on state vaiables (classes in the OODM). However, this idea is still two vague to be discussed in this paper. Another open problem concerns the generalization to arbitrary dynamic constraints. Lipeck has shown in \cite{lipeck} that dynamic constraints expressed in some generalized propositional temporal logic give rise to transition graphs. It should be possible to derive a suitable proof obligation in the predicate transformer calculus also for such constraints. Then the idea of GCS construction should carry over even to this class of constraints that comprises static and transition constraints. 

For the case of the OODM we achieve more specific results for a wide class of static constraints that occur as generalizations of kinds of constraints known from the relational model. We show that integrity enforcement for primitive update operations is possible. Moreover, part of the non-determinism can be removed in a canonical way by extension of the required input-type. In general, however, this is not sufficient, since it is not possible to construct the GCS as a combination of the GCSs of primitive operations.

\begin{thebibliography}{12}
\parskip4.5pt

\bibitem{abiteboul} S.~Abiteboul: {\it Towards a deductive
object-oriented database language}, Data \& Knowledge Engineering, vol. 5,
1990, pp. 263 -- 287

\bibitem{iql} S.~Abiteboul, P. Kanellakis: {\it Object Identity
as a Query Language Primitive}, in Proc. SIGMOD, Portland Oregon, 1989,
pp. 159 -- 173

\bibitem{type1} A.~Albano, A.~Dearle, G.~Ghelli, C.~Marlin, R.~Morrison, R.~Orsini, D.~Stemple: 
{\it A Framework for Comparing Type Systems for Database Programming Languages}, in Type Systems and 
Database Programming Languages, University of St. Andrews, Dept. of Mathematical and Computational Sciences, 
Research Report CS/90/3, 1990

\bibitem{manifesto} M.~Atkinson, F.~Bancilhon, D.~DeWitt, K.~Dittrich,
D.~Maier, S.~Zdonik: {\it The Object-Oriented Database System Manifesto},
Proc. 1st DOOD, Kyoto 1989

\bibitem{key} S. Al Fedaghi, B. Thalheim: {\it Fundamentals of databases - The
key concept}, submitted for publication, 1990

\bibitem{beeri2} C.~Beeri: {\it Formal Models for Object-Oriented 
Databases}, Proc. 1st DOOD 1989, pp. 370 -- 395

\bibitem{beeri} C.~Beeri: {\it A formal approach to object-oriented
databases}, Data and Knowledge Engineering, vol. 5 (4), 1990, pp. 353 -- 382

\bibitem{bk} C.~Beeri, Y.~Kornatzky: {\it Algebraic Optimization of Object-Oriented Query Languages},
in S.~Abiteboul, P.~C.~Kanellakis (Eds.): Proc. ICDT '90, Springer LNCS 470, pp. 72 -- 88

\bibitem{dij} E. W. Dijkstra, C. S. Scholten: {\it Predicate Calculus and
Program Semantics}, Springer-Verlag, 1989

\bibitem{lipeck2} H.-D. Ehrich, M.~Gogolla, U.~Lipeck: {\it
Algebraische Spezifikation abstrakter Datentypen}, Teubner-Verlag, 1989

\bibitem{ehrich} H.-D.~Ehrich, A.~Sernadas: {\it Fundamental Object
Concepts and Constructors}, in G.~Saake, A.~Sernadas (Eds.): Information
Systems -- Correctness and Reusability, TU Braunschweig, Informatik Berichte
91-03, 1991

\bibitem{ehma} H. Ehrig, B. Mahr: {\it Fundamentals of Algebraic
Specification}, vol.1, Springer 1985

\bibitem{tanca} P.~Fraternali, S.~Paraboschi, L.~Tanca: {\it Automatic
Rule Generation for Constraint Enforcement in Active Databases}, in
U.~Lipeck, B.~Thalheim (Eds.):  Proc. 4th Int. Workshop on Foundations of
Models and Languages for Data and Objects ``MODELLING DATABASE DYNAMICS'',
Volkse (Germany), October 19-22, 1992, in this issue

\bibitem{heuer} A.~Heuer: {\it Objektorientierte Datenbanksysteme}, Addison
Wesley, 1992

\bibitem{oid} S. Khoshafian, G. Copeland: {\it Object Identity}, 
Proc. 1st Int. Conf. on OOPSLA, Portland, Oregon, 1986

\bibitem{lipeck} U.~W.~Lipeck: {\it Dynamische Integrit\"at von Datenbanken}\/ (in German), Springer IFB 209, 1987

\bibitem{nelson} G.~Nelson: {\it A Generalization of Dijkstra's
Calculus}, ACM TOPLAS, vol. 11 (4), October 1989, pp. 517 -- 561

\bibitem{troll} G. Saake, R. Jungclaus: {\it Specification
of Database Applications in the TROLL Language}, in D.~Harper,
M.~Norrie (Eds.): Proc. Int. Workshop on the Specification of Database
Systems, Glasgow, 1991

\bibitem{ab-rev} K.-D.~Schewe, J.~W.~Schmidt, I.~Wetzel, N.~Bidoit, D.~Castelli, C.~Meghini: {\it Abstract Machines Revisited}, FIDE Technical Report 1991/11, February 1991

\bibitem{iwsds} K.-D.~Schewe, I.~Wetzel, J.~W.~Schmidt: {\it Towards
a Structured Specification Language for Database Applications}, in D.~Harper,
M.~Norrie (Eds.): Proc. Int. Workshop on the Specification of Database
Systems, Springer WICS, 1991, pp. 255 -- 274

\bibitem{rostock}
K.-D.~Schewe, B.~Thalheim, I.~Wetzel, J.~W.~Schmidt: {\it Extensible Safe Object-Oriented Design of Database Applications}, University of Rostock, Report CS - 09 - 91, September 1991 

\bibitem{icdt} K.-D.~Schewe, J.~W.~Schmidt, I.~Wetzel: {\it Identification,
Genericity and Consistency in Object-Oriented Databases}, in J.~Biskup,
R.~Hull (Eds.): Proc. ICDT '92, Springer LNCS 646, 1992, pp. 341 -- 356

\bibitem{stacs} K.-D.~Schewe: {\it Class Semantics in Object
Oriented Databases}, submitted 1992

\bibitem{tha88} B.~Thalheim: {\it
Dependencies in Relational Databases}, Teubner Leipzig, 1991

\bibitem{jan} J.~Van~den~Bussche, Dirk~Van~Gucht: {\it A Hierarchy of Faithful
Set Creation in Pure OODBs}, in J.~Biskup,
R.~Hull (Eds.): Proc. ICDT '92, Springer LNCS 646, 1992, pp. 326 -- 340

\end{thebibliography}

\end{document}
