\documentstyle[11pt,a4,fleqn]{report}

%%%%%%%%%%%%%%%%%%%% Ingrid's specs %%%%%%%%%%%%%%%%%%%

\newfont{\bs}{cmbxsl10 scaled 1200}
\newfont{\bss}{cmbxsl10 scaled 1000}

\newcommand{\brl}{\{}
\newcommand{\brr}{\}}

\newcommand{\gen}{$_{\mbox {\bss gen}}$}
\newcommand{\rep}{$_{rep}\;$}
\newcommand{\con}{$_{con}$}
\newcommand{\sel}{$_{sel}$}
\newcommand{\fun}{$_{fun}$}
\newcommand{\class}{$_{class}$}

\newcommand{\constructors}{\tt constructors}
\newcommand{\selectors}{\tt selectors}
\newcommand{\functions}{\tt functions}
\newcommand{\basedOn}{\tt basedOn}
\newcommand{\subtypeOf}{\tt subtypeOf}
\newcommand{\type}{\tt type}
\newcommand{\eend}{\tt end}
\newcommand{\axioms}{\tt axioms}

\newcommand{\pr}{$\,^\prime$}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newtheorem{definition}{Definition} 
\newtheorem{theorem}[definition]{Theorem}
\newtheorem{proposition}[definition]{Proposition} 
\newtheorem{corollary}[definition]{Corollary}
\newtheorem{lemma}[definition]{Lemma}
\newtheorem{example}{Example}
\newtheorem{algorithm}[definition]{Algorithm}
\newtheorem{proof}{Proof.}
\newtheorem{problem}{Problem.}

\renewcommand{\theproof}{}
\renewcommand{\theproblem}{}

\renewcommand{\labelenumi}{(\roman{enumi})}
\mathindent0.5cm
\newcommand{\crossbox}{ \Box \hspace*{-9pt} \times}
\newcommand{\disunion}{\stackrel{\cdot}{\cup}}
\newcommand{\qed}{\hspace*{\fill} $\Box$}

\renewcommand{\thefootnote}{\fnsymbol{footnote}}

\title{\Huge\bf Foundations of Object Oriented Database Concepts\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$^1$,\\ \Large Bernhard Thalheim$^2$,\\ \Large Ingrid Wetzel$^1$}

\date{$^1$ \ University of Hamburg, Dept. of Computer Science,\\Vogt-K\"olln-Str. 30, D-W-2000 Hamburg 54, FRG \\[1ex] $^2$ \ University of Rostock, Dept. of Computer Science,\\Albert-Einstein-Str. 21, D-O-2500 Rostock, FRG}

\begin{document}

\maketitle
\renewcommand{\thefootnote}{\arabic{footnote}}

\begin{abstract}

It is claimed that object oriented databases (OODBs) overcome many of the limitations of the relational model. However, the formal foundation of OODB concepts is still an open problem. Even worse, for relational databases a commonly accepted datamodel existed very early on whereas for OODBs the unification of concepts is outstanding.

Our research in Hamburg and Rostock is directed towards a formally founded object oriented datamodel (OODM) and to contribute to the development of a uniform mathematical theory of OODBs. This report contains the results of our first investigations on the OODM.

A clear distinction between {\em objects}\/ and {\em values}\/ turns out to be essential in the OODM. {\em Types}\/ and {\em Classes}\/ are used to structure values and objects repectively. Then the problem of unique object identification occurs. We show that this problem can be be solved for classes with extents that are completely representable by values. Such classes are called {\em value-representable}\/. The finiteness of a database and the existence of finitely representable {\em rational tree types}\/ are sufficient to decide value-representability.

Another advantage of the relational approach is the existence of structurally determined {\em canonical update operations}\/. We show that this property can be carried over to object-oriented datamodels iff classes are value-representable. Moreover, in this case {\em database consistency}\/ with respect to implicitly specified referential and inclusion constraints will be automatically preserved.

This result can be generalized with respect to distinguished classes of explicitly stated static constraints. We 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. 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.

From an engineering point of view an algorithm is required to generate these consistent operations. We address this construction problem by the specification of generators for them. These generators will be based on the possibility to represent syntactic components of the language as values within the language itself, which is known to form the basis of {\em linguistic reflection}\/. Moreover, the generators involve a single generic proof of correctness hence relieve the user of the burden to write basic update operations and to assure their consistency.

\end{abstract}

\tableofcontents

\chapter{Introduction}

The shortcomings of the relational database approach encouraged much research aimed at achieving more appropriate data models. It has been claimed that the {\em object-oriented approach} will
be the key technology for future database systems and languages \cite{oo-manifesto}. Several
systems \cite{galileo,albano1,albano,o2,quest,exodus,vision,napier,iris,orion,gemstone,florian} arose from these efforts.
However, in contrast to research in the relational area there is no common
formal agreement on what constitutes an object-oriented database \cite{beeri2,beeri,beeripods}.

The basic question ``What is an object?'' seems to be trivial, but already here the variety of answers is large. In object oriented programming the notion of an {\em object}\/ was intended as a generalization of the abstract data type concept with the additional feature of {\em inheritance}\/. In this sense object orientation involves the isolation of data in semi-independent modules in order to promote high software development productivity. The development of object oriented databases regarded an object also as a basic unit of persistent data, a view that is heavily influenced by existing semantic datamodels (SDMs) \cite{ifo,sdm,hull-king,taxis,telos,sam}. Thus, object oriented databases are composed of independent objects but must also provide for the maintenance of inter-object consistency, a demand that is to some degree in dissonance with the basic style of object orientation.

A view that is common in OODB research is that objects are abstractions of real world entities and should have an identity \cite{oo-manifesto}. This leads to a distinction between {\em values}\/ and {\em objects}\/ \cite{beeri2,beeri}. A value is
identified by itself whereas an object has an identity independent of its
value. This object identity is usually encoded by object identifiers \cite{abiteboul,iql,oid}. Abstracting from the pure physical level the identifier of an object can be regarded as being immutable during the object's lifetime. Identifiers ease the sharing and update of data. However, such abstract identifiers do not relieve us from the task to provide unique identification mechanisms for objects. In object oriented programming object names are sufficient. Retrieving mass data by name is senseless.

In most approaches to OODBs an object is coupled with a value of some fixed structure. To our point of view this contradicts already the goal of objects being abstractions of reality. In real situations an object has several and also changing aspects that should be captured by the object model.

\begin{quote}

Therefore, in our object model each {\em object}\/ $o$ consists of a unique identifier $id$, a set
of (type-, value-)pairs $( T_i , v_i )$, a set of (reference-, object-)pairs $(
ref_j , o_j )$ and a set of methods $meth_k$.

\end{quote}

\noindent
Types are used to structure values. Classes serve as structuring primitive for objects having
the same structure and behaviour. It is obvious that the multiple aspects view of an object allows them to be simultaneously members of more than one class and to change class memberships.

In our model a class structure 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 static and dynamic constraints. 

\section{The Identification Problem}

One important concept of object-oriented databases is {\em object identity}\/. Following \cite{abiteboul,bk} the immutable identity of an object can be encoded by the concept of abstract object-identifiers. The advantages of this approach are that sharing, mutability of values and cyclic structures can be represented easily \cite{ohori}. On the other hand, system provided identifiers can not be used for object identification, since this would lead to a database of identifiers \cite{lockemann}. Hence the user can only access objects in the database via values. Object identifiers do not have a meaning
for the user and should be hidden from the user.

We study whether equality of identifiers can be derived from the
equality of values. In the literature the notion of ``deep'' equality has
been introduced for objects with equal values and references to
objects that are also ``deeply'' equal. This recursive definition becomes
interesting in the case of cyclic references.

Therefore, we introduce {\em functional constraints}\/ on classes, in particular
{\em uniqueness constraints}\/, which express equality on identifiers as a consequence
of the equality of some values or references. On this basis we can
address the following problem how to characterize those classes that are completely representable
(and hence also identifiable) by values.
We show that the finiteness of a database and the existence of finitely representable recursive types are sufficient to decide {\em value-representability}\/.

\section{Generic Update Operations}

The success of the relational data model is due certainly to the existence of
simple query and update-languages. Preserving the advantages of the relational in OODBs is a serious goal.

The generic querying of objects has been approached in \cite{abiteboul,bk}. While querying is per se a set-oriented operation, i.e. it is not necessary to select just one single object, and hence does not raise any specific problems with object identifiers, things change completely in case of updates. If an object with a given value is to be updated (or deleted), this is only defined unambigously, if there does not exist another object with the same value. If more than one object exists with the same value or more generally with the same value and the same references to other objects, then the user has to decide, whether an update- or delete-operation is applied to {\em all} these objects, to only {\em one} of these objects selected non-deterministically or to {\em none} of them, i.e. to reject the operation.
However, it is not possible to specify a priori such an operation that works in the same way for all objects in all situations. The same applies to insert-operations. Hence the problem, in which cases operations for the insertion, deletion and update of objects can be defined generically.

Some authors \cite{saake} have chosen the solution to abandon generic operations. Others \cite{albano1,albano,o2} use identifying values to represent object identity, thus embody a strict concept of surrogate keys to avoid the problem. Our approach is different from both solutions in that we use the concept of hidden abstract identifiers, but at the same time formally characterize those classes for which unique generic operations for the insertion, deletion and update of single objects can be derived automatically. It turns out that these are exactly the value-representable ones.

It can be shown that generators for these generic update operations can be specified for any value-representable class of a schema. The generators can be used to increase the productivity of system developers while enhancing the quality of the implemented systems.

\section{The Consistency Problem}

One of the primary benefits that database systems offer is automatic 
enforcement of database integrity.  
One type of integrity is maintained through automatic concurrency control 
and recovery mechanisms; allmost all commercial systems provide 
this. Another one is the automatic enforcement of user-specified integrity 
constraints. Most commercial database systems, especially 
relational database management systems enforce only a bare minimum of 
constraints, largely because of the performance overhead associated with 
updates. 
A database system should be designed to automatically take methods specified 
by the user or generated by the system upon checking integrity constraints 
upon occurrence of certain database operations.

The {\em maintenance problem}\/ is the problem how to ensure the database 
satisfies its constraints after certain actions. 
There are at present two approaches to this maintenance problem. 
The first one, more classical is the modification of methods in accordance 
to the specified integrity constaints. 
The second approach uses generation mechanisms for the specified events. Upon 
occurrence of certain database events like update operations the management 
component is activated 
for integrity maintenance. The first research direction did not succeed 
because of some limitations within the approach. The second one is at present one 
of the most active database research areas. One of our objectives is to show that the first approach can be extended to object-oriented 
databases using stronger mathematical fundamentals.

Accuracy is an obviously important and desirable feature of any database. 
To this end, {\em integrity constraints}\/, conditions that 
data must satisfy before a database is updated, are commonly employed as 
a means of helping to maintain consistency.  
In relational databases the specification and enforcement 
of integrity constraints has a long tradition \cite{tha88}, whereas in 
OODBs the integrity problem has only recently drawn attention \cite{tanca,volkse}. 

In object oriented databases, integrity maintenance can be based 
on two different approaches. The first one uses blind update operations. In 
this case, any update is allowed and the system organizes the maintenance. 
The second approach is based on 
methods rewriting. This approach is more effective. Assuming a 
consistent database state  the modified method can not lead to an 
inconsistent state. 
In contrast to the relational model 
the fundamental concepts of {\em object identity}\/ \cite{oid} 
and {\em inheritance}\/ imply inevitably the existence of {\em inclusion}\/ 
and {\em referential constraints}\/ that are specified with each OODB schema. 
Integrity with respect to these constraints must be preserved by all 
database updates, especially by basic {\em insert-}\/, {\em delete-}\/ 
and {\em update-}\/operations. As usual in OODBs 
such operations are modeled by {\em methods}\/. Due to the main 
result in \cite{icdt} such operations are only uniquely determined 
by the schema in the case of {\em value-representable}\/ classes. We shall 
outline these methods and draw specific attention to the type 
of the required input-value.
 
In relational databases distinguished classes of static 
integrity constraints have been discussed such as {\em inclusion}\/, {\em exclusion}\/, 
{\em functional}\/, {\em key}\/ and {\em multi-valued dependencies}\/. 
All these constraints can be generalized to the object oriented case. 
Then the result on the existence of integrity preserving methods can 
be generalized to capture also these constraints. We shall also describe 
the resulting methods.

\section{The Organization of the Paper}

In Chapter \ref{model} we introduce the OODM. We start first motivating
the concepts and give a short review on some theoretical aspects underlying the
model. Then we describe in detail the structural and the behavioural parts of
the OODM.

Chapter \ref{identification} handles the identification problem. We
introduce the notion of value-represen\-ta\-bi\-li\-ty and show results on the
decidability.

The genericity problem will be approached in Chapter \ref{genericity}. We show the relationship between value-representability and the unique existence of generic update operations. Finally we describe an algorithmic approach to generate such operations using linguistic reflection.

The consistency problem is dealt with in Chapter \ref{enforcement}. We outline an operational approach based on greatest consistent specializations and describe them for the case of distinguished classes of static integrity constraints.

We summarize our results and describe some open problems in Chapter \ref{schluss}.

\section*{Acknowledgement}

We would like to thank Catriel Beeri for stimulating discussions concerning object identification. We also want to thank David Stemple who contributed to the engineering aspects concerning genericity in the OODM. He convinced us on the benefits of linguistic reflection. Thanks also to Kasimierz Subieta for questioning the theme from a programming point of view.

\chapter{An Object Oriented Datamodel} \label{model}

In this chapter we present the formal object oriented datamodel (OODM) of \cite{rostock,icdt,volkse}. We observe that an object in the real world always has an identity. Therefore, abstract (i.e. system-provided) object identifiers are introduced to capture identity. However, neither the real world object that was the basis of the abstraction nor the abstract identifier can be used for the identification of an object.

In contrast to existing object oriented datamodels \cite{abiteboul,iql,galileo,albano1,albano,oo-manifesto,o2,exodus,vision,iris,orion,gemstone,ohori,saake,schekscholl} an object is not coupled with a unique type. In contrast, we observe that real world objects can have different aspects that may change over time. Therefore, a primary decision was taken to let an object be associated with more than one type and to let these types even change during the object's lifetime. The same applies to references to other objects.

Classes are used to abstract from individual objects providing mutable collections of a given structure and behaviour, where the latter is modelled via methods.

We start with a motivation, where we explain the general notion of an object and illustrate by using examples the notions of {\em type}\/, {\em class}\/ and {\em method}\/. Throughout this section a preliminary informal syntax will be used.

Then we give a brief outline of some theoretical background underlying the OODM. This comprises an algebraic framework for type and method specifications that stems from the specification language SAMT \cite{iwsds,stacs} together will formally defined consistency notions.

The heart of the chapter is formed by Sections \ref{fundamentals} and \ref{behaviour}, where we introduce formally the structural and the behavioural part of the OODM.

\section{Motivation} \label{motivation}

Relational approaches to data modelling are called value-oriented since in 
these models real world entities are completely represented by their values.
In the object-oriented approach we distinguish between objects and values.
Values can be gouped into types. In general, a type may be regarded as an
immutable set of values of a uniform structure together with operations
defined on such values. Subtyping is used to relate values in different types.

Whereas values are encoded by themselves \cite{beeri2,beeri}, objects have to be
encoded by object identifiers regardless of the content, location or
addressability \cite{oid}. In our approach to OODBs each object $o$ consists of a unique identifier $id$, a set
of (type-, value-)pairs $( T_i , v_i )$, a set of (reference-, object-)pairs $(
ref_j , o_j )$ and a set of methods $meth_k$. We assume all identifiers $id$ to belong to unique given set $ID$. 

Types represent immutable sets of values. They can be defined algebraically similar to
\cite{bk,ehrich1,ehma}. Type constructors can be defined analogously by parameterized types. These can be used to build complex types by nesting and recursive types. We assume that the set $ID$ of possible object identifiers is also a type. Then an instantiation of a parameterized type defines a structure
that represents a combination of values and references, where references are expressed by the occurrence of a value of type $ID$.

Objects can be grouped into
classes with some structure built from values and references. Furthermore, we may associate
methods and constraints with each class. This means of structure building involves implicit {\em referential
constraints}\/. Inheritance on classes is given by IsA-relations, i.e. by set inclusion on object identifiers. Moreover we introduce subtyping and formalize this by the definition of a continuous function from a subtype to a supertype. The relation between subtyping and inheritance is given by an {\em inclusion constraint}\/ on classes.

\subsection{The Class Concept as a Structural Primitive} \label{classes-informal}

The class concept provides the grouping of objects having
the same structure which uniformly combines aspects of object values and references. Moreover, generic operations on objects such as object creation, deletion and update of its values and references are associated with classes provided these operations can be defined unambigously. Objects can belong to different classes, which guarantees each object of our abstract object model to be captured by the collection of possible classes.
As for values
that are only defined via types, objects can only be defined via classes.
Thus, a design consists of {\em type}\/ 
and {\em class definitions}.

\subsubsection{Type Definitions.}

Assume the existence of {\em basic types}\/ $STRING$, $NAT$, $INT$ and $BOOL$ 
with the usual operations on them. Additionally, there exist a basic type $ID$ that will be used to model object identifiers and a trivial type $\bot$ with only one element and no operations.

In this paper we only use fixed type constructors, the {\em tagged tuple}\/ constructor denoted
by ($\cdot$), the {\em finite set}\/ constructor denoted by $\{ \cdot \}$ and the {\em union}\/ constructor denoted $\cup$. We use concatenation on tuple types denoted by the $\circ$-operator.

Types and type constructors in general are defined by nesting of these constructors. These types can be organized in a {\em subtype}\/ hierarchy with the subtype relation defined as usual. $\bot$ is a supertype of every type.

As a last structuring feature recursive type definitions are allowed. They only occur as input-types for generated update methods, where {\em rational tree}\/ values are required \cite{life}.

\begin{example} {\rm \label{bsp-type-informal}

The set and the tuple type constructors are both used in the declaration for PERSONNAME:

\begin{tabbing}
xxxxx\=PERSONNAMEE a \= a = \= ( \= SecondName, \= :, \= \{STIRNG\} \=\kill
\>$PERSONNAME$ \> = \> ( \> FirstName \>: \>$STRING$,\\
\>\>\>\>SecondName\> :\> $STRING$,\\
\>\>\>\> Titles \>:\> \{$STRING$\}\>)
\end{tabbing}

The definition for a type PERSON uses the type PERSONNAME and a type ADDRESS 
defined elsewhere:

\begin{tabbing}
xxxxx\=PERSONNAMEE a \= = a \= ( \= PersonIdentityNo, \= :, \= PERSONNAME, 
\=\kill
\>$PERSON$ \> = \> ( \> PersonIdentityNo \>: \>$NAT$,\\
\>\>\>\>Name\> :\> $PERSONNAME$,\\
\>\>\>\> Address \>:\> $ADDRESS$ \> )
\end{tabbing}

The following example defines {\em STUDENT} as a subtype of {\em PERSON}:

\begin{tabbing}
xxxxx\=PERSONNAMEE a \= = a \= ( \= Faculty, \=  :, \= NAT, \=\kill
\>$STUDENT$ \> = \>\>$PERSON$ $\circ$ ( StudNo : $NAT$, Faculty : $NAT$ ) \hspace{1.0cm}\qed
\end{tabbing}

} \end{example}

\subsubsection{Class Definitions.}

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 type constructors.

\begin{itemize}

\item Let $t$ be a type constructor with parameters $\alpha_1 , \ldots , \alpha_n$ such that $ID$ does not occur in $t$. For distinct reference names $r_1 , \ldots , r_n$ and class names $C_1 , \ldots , C_n$ 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$, a structure expression $S$, a set of class names $D_1 , \ldots , D_m$ (in the following called the set of {\em superclasses}\/) and a set of methods. 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 constraints ${\cal I}_1 , \ldots , {\cal I}_n $.

\end{itemize}

\begin{example} {\rm \label{bsp-schema-informal}

Let the types $PERSON$ and $STUDENT$ be as in Example \ref{bsp-type-informal}. In addition assume a type $PROFESSOR$ defined as elsewhere as another subtype of $PERSON$. Then the following is a simple schema for a university application. For the moment methods are omitted.\\

\noindent
{\tt Schema} \ University\\
\indent {\tt Class} \ {\sc PersonC}\\
\indent \indent {\tt Structure} \ $PERSON$\\
\indent \indent {\tt Methods} \ $\ldots$\\[0.8ex]
\indent {\tt Class} \ {\sc MarriedPersonC}\\
\indent \indent {\tt IsA} \ {\sc PersonC}\\
\indent \indent {\tt Structure} \ $PERSON \circ$ (Spouse : {\sc MarriedPersonC})\\[0.8ex]
\indent {\tt Class} \ {\sc StudentC}\\
\indent \indent {\tt IsA} \ {\sc PersonC}\\
\indent \indent {\tt Structure} \ $STUDENT \circ$ (Supervisor : {\sc ProfessorC})\\[0.8ex]
\indent {\tt Class} \ {\sc ProfessorC}\\
\indent \indent {\tt IsA} \ {\sc PersonC}\\
\indent \indent {\tt Structure} \ $PROFESSOR$\\[0.8ex]
\indent {\tt Constraint} \ Unique({\sc PersonC},$PERSON$)\\[0.8ex]
\indent {\tt Constraint} \ EXCL({\sc StudentC},{\sc ProfessorC}) \qed

} \end{example}

\noindent
The notation Unique($C$,$T$) means that values of type $T$ do not occur twice in the class $C$. EXCL($C_1$,$C_2$) states that the classes $C_1$ and $C_2$ are disjoint.

At each time, $C$ is given by a finite set of objects. More precisely, $C$ is a set of pairs $(i,v)$, where $i$ is of type $ID$ and $v$ is of type $T_C$ such that identifiers are unique in this set. This defines an {\em instance} $\cal D$ of a schema $\cal S$.

Moreover, $C$ gives rise to {\em referential
constraints}\/ defined by the structure $S$ and {\em IsA constraints}\/ defined by the set of superclasses of $C$, i.e.

\begin{itemize}

\item whenever an identifier $j :: ID$ occurs in $v$ and this occurrence corresponds to the reference $r_k : C_k$, then there must exist an object in $C_k$ with identifier $j$ ({\em referential integrity}\/), and 

\item for each superclass $D_k$ there exist an object with identifier $i$ (and some value $w :: T_{D_k}$ in $D_k$) ({\em inclusion integrity}\/). Moreover, if $T_C$ is a subtype of $T_{D_k}$, there $v$ must correspond to $w$.

\end{itemize}

\noindent
Note, that we do not require classes to be disjoint nor that IsA relations require a subtype relation on the corresponding representation types.

\subsection{Methods as a Basis for Behaviour Modeling} \label{methods-informal}

Methods in general can be described operationally with the usual control constructs. Assignments are only allowed on the class $C$ or on a selective expression on $C$. Therefore, we dispense with introducing a specific method language here.

Let us now concentrate on basic 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{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.

Value-representability of all classes in a schema is implied, if we define a trivial {\em uniqueness constraint}\/ for each class. Such a constraint requires the values of type $T_C$ in the class extension $C$ to be unique, which is similar to a (trivial) key definition in the relational case.

\begin{example} {\rm  \label{bsp-method-informal}

Let us describe the insert-method for the class {\sc PersonC} of Example \ref{bsp-schema-informal}.\\

\noindent
insert$_{PersonC}$ (in: $P$ :: $PERSON$, out: I :: $ID$) \ = \\
\indent IF \ $\exists \; O \in$ {\sc PersonC} . value($O$) = $P$\\
\indent THEN \ $I$ := ident($O$)\\
\indent ELSE \ $I$ := NewId  ; \\
\indent \indent {\sc PersonC} := {\sc PersonC} $\cup$ \{ ( $I$,$P$)\}\\
\indent ENDIF\\

\noindent
For the insert on the class {\sc MarriedPersonC} we need a more complex input type $V$ recursively defined as

\[ V = PERSON \circ \mbox{(} V \cup ID \mbox{)} \]

\noindent
For each $P :: V$ let $f(P) :: PERSON$ be the projection onto $PERSON$ corresponding to the subtype relation between $V$ and $PERSON$. Then we have\\

\noindent
insert$_{MarriedPersonC}$ (in: $P$ :: $V$, out: $I$ :: $ID$) \ = \\
\indent $I$ := insert$_{PersonC}(f(P))$ ; \\
\indent IF \ $\forall \; O \in \mbox{\sc MarriedPersonC}$ . ident($O$) $\neq$ $I$\\
\indent THEN \ $P^\prime$ := substitute($I$,$P$,Spouse(P)) ; \\
\indent \indent \indent IF \ $P^\prime :: ID$\\
\indent \indent \indent THEN \ $J$ := $P^\prime$\\
\indent \indent \indent ELSE \ $J$ := insert$_{MarriedPersonC}$($P^\prime$)\\
\indent \indent \indent ENDIF \ ; \\
\indent \indent {\sc MarriedPersonC} := {\sc MarriedPersonC} $\cup$ \{ ($I$,$f(P) \circ \mbox{(} J \mbox{)}$)\}\\
\indent ENDIF\\

\noindent
We used the global method NewId to denote the selection of a new identifier. The expression substitute($I$,$P$,$T$) denotes the result of replacing the value $I$ for $P$ in the expression $T$. \qed

} \end{example} 

\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 the 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. This is related to algebraic specifications \cite{ehrich1,ehma}. 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} {\rm \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} {\rm \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. See \cite{stacs} for a completely mathematical treatment of types. 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,ab-rev,vdm,nelson}:

\begin{definition} {\rm \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} {\rm \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{The Structural Approach} \label{fundamentals}

In the following assume to be given a type system $\cal T$ as described e.g. in Section \ref{types}. Basically such a type system consists of some {\em basic types}\/ such as $BOOL$, $NATURAL$, $INTEGER$, $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 $\cal T$. As an alternative to our definition of $\cal T$ in Section \ref{types} we may restrict $\cal T$ being one of the type systems  defined in \cite{galileo,type1,cardelli,quest,napier,adabtpl,dbpl,florian}. In addition we suppose the existence of an abstract identifier type $ID$ in $\cal T$ 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} {\rm \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}\/) and a set of static constraints ${\cal I}_1 , \ldots , {\cal I}_k $. 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 (structural) {\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 $.

\item An {\em instance} $\cal D$ of a structural 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. Distinguished classes of static constraints will be introduced in Section \ref{constraints}. 

\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$. $PFUN(ID,T_C)$ is called the {\em class type}\/ of $C$. $PFUN(\alpha,\beta)$ is the type constructor for partial function from $\alpha$ to $\beta$ with finite domain\footnote{In fact, we need a more sophisticated semantics for objects and classes as exemplified by the algebraic approach of the IS-CORE group \cite{ehrich} or by the evolving algebra approach \cite{gottlob}.}. 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$. Let us now formally describe the form of structurally defined inclusion and referential constraints.

\begin{definition} {\rm \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.

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

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

Assume the existence of a value type PERSON defined elsewhere. A class $C$ named {\sc PersonC} may be defined
as follows.\\

\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\\
{\tt End} \ {\sc PersonC} \qed

} \end{example} 

\subsection{Static Integrity 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 \cite{volkse,adc}.

\begin{definition} {\rm \label{explicit} \label{constraint}

\ 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{tha88}. The following definition extends these constraints to path constraints.

\begin{definition} {\rm \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} 

\section{The Behavioural Approach} \label{behaviour}

So far, only static aspects have been considered. A structural schema is simply a collection of data structures called classes. Let us now turn to adding dynamics to this picture. As required in the object oriented approach operations will be associated with classes. This gives us the notion of a method.

We shall distinguish between visible and hidden methods to emphasize those methods that can be invoked by the user and others. This is not intended to define an interface of a class, since for the moment all methods of a class including the hidden ones can be accessed by other methods. The justification for such a weak hiding concept is due to two reasons.

\begin{itemize}

\item Visible methods serve as a means to specify (nested) transactions. In order to build sequences of database instances we only regard these transactions assuming a linear invocation order on them.

\item Hidden methods can be used to handle identifiers. Since these identifiers do not have any meaning for the user, they must not occur within the input or output of a transaction.

\end{itemize}

\noindent
In general methods describe possible sequences of database instances. In order to restrict this set of possible sequences to legal ones dynamic integrity constraints are used. In general some temporal logic is required to express such constraints \cite{lipeck}. In order to avoid this we restrict the OODM to allow only transition constraints to be specified.

In a second part we shall have a short look on queries and views.

\subsection{Methods, Transactions and Transition Constraints}

Let us now address the formalization of the notions {\em method}\/, {\em class}\/ and {\em transition constraint}\/ and then generalize the notion of {\em schema}\/.

\begin{definition} {\rm \label{def-method}

Let $T_1 , \ldots , T_n , T_1^\prime , \ldots , T_m^\prime \in N_T$ such that there exist types in $\cal T$ with these names. Let $M \in N_M$ and $\iota_1 , \ldots , \iota_n , o_1 , \ldots , o_m \in V$.

\begin{enumerate}

\item A {\em method signature}\/ consists of a method name $M$, a set of input-parameter / input-type pairs $\iota_i :: T_i$ and a set of output-parameter / output-type pairs $o_j :: T_j^\prime$. We write

\[ o_1 :: T_1^\prime , \ldots , o_m :: T_m^\prime \; \leftarrow \; M ( \iota_1 :: T_1 , \ldots , \iota_n :: T_n ) \; . \]

\item Let $C$ be some class as in Definition \ref{structure-expression}. A {\em method}\/ $M$ on $C$ consists of a method signature with name $M$ and a body that is represented as a guarded command on $X = \{ x_C \}$.

\item A method $M$ on a class $C$ with signature $o_1 :: T_1^\prime , \ldots
, o_m :: T_m^\prime \; \leftarrow \; M ( \iota_1 :: T_1 , \ldots , \iota_n ::
T_n )$ is called {\em value-defined}\/ iff all $T_i$ ($i = 1 \ldots n$) and
$T_j^\prime$ ($j = 1 , \ldots , m$) are proper value types.

\end{enumerate}

} \end{definition}

\noindent
On the representation level (see Section \ref{schema-rep}) we use guarded commands for methods. As mentioned above the OODM distinguishes between transactions, i.e. methods visible to the user, and hidden methods. We require each transaction to be value-defined. 

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. Overriding becomes mandatory in the case of multiple inheritance with name conflicts. A method that overrides a hidden method on some superclass must also be hidden.

\begin{definition} {\rm \label{method-spec}

Let $C$ be a class as in Definition \ref{structure-expression} with superclasses $D_1 , \ldots , D_k$. A {\em method specification}\/ on $C$ consists of two sets of methods ${\cal S} = \{ M_1 , \ldots , M_n \}$ (called {\em transactions}\/) and ${\cal H} = \{ M_1^\prime , \ldots , M_m^\prime \}$ (called {\em hidden methods}\/) such that the following properties hold:

\begin{enumerate}

\item Each $M_i$ ($i = 1 , \ldots , n$) is value-defined.

\item For each transaction $M^l$ on some superclass $D_l$ there exists some $i \in \{ 1, \ldots ,n \}$ such that $M_i$ specializes $M^l$.

\item For each hidden method $M^l$ on some superclass $D_l$ there exists some $j \in \{ 1, \ldots ,m \}$ such that $M_j^\prime$ specializes $M^l$.

\end{enumerate}

} \end{definition}

\noindent
Let us briefly discuss what specialization means for the input- and output-types. Sometimes it is required that the input-type for an overriding method should be a subtype of the original one (covariance rule), sometimes the opposite (contravariance rule) is required. The first rule applies e.g. if we want to override an insert method. In this case the inherited method has no effect on the subclass, but simply calls the ``old'' method. The second rule applies if input-types reuired on the superclass can be omitted on the subclass. Both rules are captured by the formal notion of specialization. We omit the details \cite{iwsds}.

\begin{example} {\rm \label{bsp-method}

Let us now describe methods on the class {\sc PersonC} introduced in Example \ref{bsp-class}. 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
{\tt Methods} \\
\indent \hspace*{10pt} insert( P :: $V_C$ = PAIR(PERSON,$V_C$) ) == I $\leftarrow$ insert$^\prime$(P)\\
({\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 \qed

} \end{example}

\noindent
The dynamic part of a schema also requires transition constraints to be specified.

\begin{definition} {\rm

Let $C$ be a class as in Definition \ref{structure-expression}. A {\em transition constraint}\/ on $C$ is a first-order formula $\cal R$ with $fr({\cal R}) \subseteq \{ x_C , x_C^\prime \}$, where $x_C^\prime$ represents the value of $x_C$ after performing some operation.

} \end{definition}

\noindent
Now we are prepared to generalize the definition of classes, schemata and instances.

\begin{definition} {\rm \label{class}

\begin{enumerate}

\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$ (called the set of {\em superclasses}\/), a set of static constraints ${\cal I}_1 , \ldots , {\cal I}_k $, a set of transition constraints ${\cal J}_1 , \ldots , {\cal J}_l $ and a method specification (${\cal S} = \{ M_1 , \ldots , M_n \}$ , ${\cal H} = \{ M_1^\prime , \ldots , M_{n^\prime}^\prime \}$) on $C$. 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, superclasses and method call 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}_l $.

\item An {\em instance} $\cal D$ of a structural 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}

\subsection{Queries and Views}

Roughly speaking the querying of a database is an operation on the database without changing its state. The emphasis of a query is on the output. While such a general view of queries can be subsumed by transactions, hence by methods in the OODM, query languages are in particular intended to be declarative in order to support an ad-hoc querying of a database without the need to write new transactions \cite{oo-manifesto}.

Querying a relational database can be expressed by terms in relational algebra. This view can be easily generalized to the OODM that is built upon a sophisticated extensible type system $\cal T$. Each type is algebraically specified and hence gives rise to an algebra -- to be more precise: a G-algebra \cite{stacs}. Therefore, terms over such types occur naturally. Moreover, type specifications are based on other type specifications via constructors, selectors and functions. Hence, $\cal T$ allows arbitrary terms involving more than one class variable $x_C$ to be built. Then a {\em query}\/ turns out be be represented by term $t$ over some type $T$ such that the free variables of $t$ are all class variables. This approach is in accordance with the algebraic approach in \cite{bk} and with so called {\em universal traversal combinators}\/ \cite{traversal}.

In relational algebra a {\em view}\/ may be regarded simply as a stored query (or derived relation). We shall try to generalize also this view to the OODM.

However, things change dramatically, when object identifiers come into
play \cite{beeripods}, since now we have to distinguish between queries that
result in values and those that result in (collections of) objects. Therefore
we distinguish in the OODM between value queries and general access expressions.

A {\em value query}\/ on a schema $\cal S$ can then be represented by a term $t$ of some value type $T$ with $fr(t) \subseteq \{ x_C \mid C \in {\cal S} \}$. Ad-hoc querying of a database should then be restricted to value queries. This is no loss of generality, because for any type $T$ in $\cal T$ involving identifiers there exists a corresponding type $T^\prime$ allowing multiple occurrences. Take e.g. a class $C$. If we want to get all the objects in that class no matter whether they have the same values or not, the corresponding term of type $T = PFUN(ID,T_C)$ would be $x_C$. This is not a value query, but if $T_C$ is a value type, we may take $T^\prime = BAG(T_C)$ and the natural projection given by the subtype functions 

\[ PFUN(\alpha,\beta) \rightarrow FSET(PAIR(\alpha,\beta)) \rightarrow BAG(PAIR(\alpha,\beta)) \rightarrow BAG(\beta) \; . \]

\noindent
In Section \ref{value-rep} we shall see how to generalize this to be case where $T_C$ is arbitrary. We then have to replace $T_C$ by the value-representation type $V_C$ provided this exists.

In the case of arbitrary access expressions another problem occurs \cite{beeripods}. So far, we can only build terms $t$ that involve identifiers already existing in the database. Thus, such queries are called {\em object preserving}\/. If we want the result of a query to represent ``new'' objects, i.e. if we want to have {\em object generating queries}\/, we have to apply a mechanism to create new object identifiers. This can be achieved by {\em object creating functions}\/ on the type $ID$ with arity $ID \times \ldots \times ID \rightarrow ID$ \cite{ilog,kifer}.

The idea that a view is a stored query then carries over easily. However, the structure of a view should be compatible with the structure of the schema, i.e. each view may be regarded as a derived class. Summarizing, we get the following formal definition.

\begin{definition} {\rm \label{query-view}

Let ${\cal S} = \{ C_1 , \ldots , C_n \} $ be some schema.

\begin{enumerate}

\item A {\em value query}\/ on $\cal S$ is a term $t$ over some proper value type $T$ with\\
$fr(t) \subseteq \{ x_{C_1} , \ldots , x_{C_n} \} $.

\item An {\em access expression}\/ on $\cal S$ is a term $t$ over some proper type $T$ with\\
$fr(t) \subseteq \{ x_{C_1} , \ldots , x_{C_n} \} $.

\item A {\em view}\/ on $\cal S$ consists of a view name $v \in N_C$ such that there is no class $C \in {\cal S}$ with this name, a structure expression $S(v)$ containing references to classes in $\cal S$ or to views on $\cal S$ and a defining access expression $t(v)$ of type $PFUN(ID,T_v)$, where $T_v$ is the representation type corresponding to $S(v)$.

\end{enumerate}

} \end{definition}

\noindent
Let us now finalize this chapter with a simple example of a view in the OODM.

\begin{example} {\rm \label{bsp-view}

Take again the class {\sc PersonC} of Example \ref{bsp-class}. Let $Age$ be some selector on the type $PERSON$ and let the function $filter$ be defined on $FSET(\alpha)$ with arity $FSET(\alpha) \times FUN(\alpha,BOOL) \rightarrow FSET(\alpha)$ (see also \cite{bk}). Then the following defines the subset of {\sc PersonC} of all old persons.\\

\noindent
{\tt View} \ {\sc OldPersonV} \ ==\\
\indent {\tt Structure} \ $PAIR ( PERSON, spouse : \mbox{\sc PersonC} )\\
\indent {\tt Definition} \ $filter(\mbox{\sc PersonC},Lambda[X](greater(Age(First(Second(X))),60)))\\
{\tt End} \ {\sc OldPersonV} \qed

} \end{example}

\chapter{Object Identification and Value-Representation} \label{identification}

This chapter is devoted to the identification problem in object oriented databases. Roughly speaking databases are considered to contain persistent mass data. From an object oriented point of view a database may be considered as a huge collection of objects of arbitrary complex structure. Hence the problem to uniquely identify and retrieve objects in such collections.

Each object in a database is an abstraction of a real world object that has a unique {\em identity}\/. The representation of such objects in the OODM uses an abstract identifier $I$ of type $ID$ to encode this identity. Such an identifier may be considered as being immutable. However, from a systems oriented view permutations or collapses of identifiers without changing anything else should not affect the behaviour of the database.

For the user the abstract identifier of an object which may be e.g. a physical address has no meaning. Therefore, a different access to the identification problem is required. We show that the unique identification of an object in a class leads to the notions of {\em value-identifiability}\/ and {\em value-representability}\/. We discuss the identification problem in Section \ref{value-rep} under the assumption that the only explicit constraints are uniqueness constraints. Then we analyse the weaker concept of {\em weak value-representability}\/ that can be used to capture also objects that do not exists for there own, but depend on other objects. This is related to {\em weak entities}\/ in entity-relationship models \cite{herm}.

\section{On the Notion of Value-Representability} \label{value-rep}

According to our definitions two objects in a class $C$ are identical iff they have the same identifier. By the use of constraints, especially uniqueness constraints, we could restrict this notion of equality.

The goal of this section is the characterization of those classes, the objects in which are completely representable by values, i.e. we could drop the object identifiers and replace references by values of the referred object. We shall see in Section \ref{generic} that in case of value-representable classes we are able to preserve an important advantage of relational databases, i.e. the existence of structurally determined update operations.

\begin{definition} {\rm \label{value-repr} \label{def-valuerep}

\ Let $C$ be a class in a schema $\cal S$ with representation type $T_C$.

\begin{enumerate}

\item $C$ is called {\em value-identifiable} iff there exists a proper value type $I_C$ such that for all instances $\cal D$ of $\cal S$ there is a function $c: T_C \rightarrow I_C$ such that the uniqueness constraint on $C$ defined by $c$ holds for $\cal D$.

\item $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 uniqueness constraint on $C$ defined by $c$ holds and

\item for each uniqueness constraint on $C$ defined by some function $c^\prime: T_C \rightarrow V_C^\prime$ with proper value type $V_C^\prime$ there exists a function $c^\prime{}^\prime: V_C \rightarrow V_C^\prime$ that is unique on $c(codom_{\cal D}(C))$ with $c^\prime = c^\prime{}^\prime \circ c$.

\end{enumerate}

\end{enumerate}

} \end{definition} 

\noindent
It is easy to see that each value-representable class $C$ is also value-identifiable. Moreover, the {\em value-representation type} $V_C$ in Definition \ref{value-repr} is unique up to isomorphism.

\begin{theorem}

\ Let $C$ be a class in a schema $\cal S$. Then $C$ is value-representable iff $C$ is value-identifiable and $C_i$ is value-representable for all references $r_i : C_i$ in the structure expression $S$.

\end{theorem}

\begin{proof} {\rm 

This follows directly from the definitions. \qed

} \end{proof} 

\subsection{Value-Representability in the Case of Acyclic Reference Graphs} \label{vrep-simple}

Since value-representability is defined by the existence of a certain proper value type, it is hard to decide, whether an arbitrary class is value-representable or not. In case of simple classes the problem is easier, since we only have to deal with uniqueness and value constraints. In this case it is helpful to analyse the reference structure of the class. Hence the following graph-theoretic definitions.

\begin{definition} {\rm  \label{ref-graph}

The {\em reference graph} of a class $C$ in a schema $\cal S$ is the smallest labelled graph $G_{rep} = (V,E,l)$ satisfying:

\begin{enumerate}

\item There exists a vertex $v_C \in V$ with $l(v_C) = \{ t , C \}$, where $t$ is the top-level type in the structure expression $S$ of $C$.

\item For each proper occurrence of a type $t \neq ID$ in $T_C$ there exists a unique vertex $v_t \in V$ with $l(v_t) = \{ t \}$.

\item For each reference $r_i : C_i$ in the structure expression $S$ of $C$ the reference graph $G_{ref}^i$ is a subgraph of $G_{ref}$.

\item For each vertex $v_t$ or $v_C$ corresponding to $t ( x_1 , \ldots , x_n )$ in $S$ there exist unique edges $e_t^{(i)}$ from $v_t$ or $v_C$ respectively to $v_{t_i}$ in case $x_i$ is the type $t_i$ or to $v_{C_i}$ in case $x_i$ is the reference $r_i : C_i$. In the first case $l(e_t^{(i)}) = \{ S_i \}$, where $S_i$ is the corresponding selector name; in the latter case the label is $\{ S_i , r_i \}$.

\end{enumerate}

} \end{definition} 

\begin{definition} {\rm \label{id-graph}

\ Let ${\cal S} = \{ C_1 , \ldots , C_n \}$ be a schema. Let ${\cal S}^\prime = \{ C_1^\prime , \ldots , C_n^\prime \}$ be another schema such that for all $i$ either $T_{C_i}^\prime = T_{C_i}$ holds or there exists a uniqueness constraint on $C_i$ defined by some $c_i: T_{C_i} \rightarrow T_{C_i^\prime}$. Then an {\em identification graph} $G_{id}$ of the class $C_i$ is obtained from the reference graph of $C_i^\prime$ by changing each label $C_j^\prime$ to $C_j$.

} \end{definition} 

\begin{example} {\rm \label{bsp-graph}

\ Let {\sc MarriedPersonC} be defined as in Example \ref{bsp-class}. Then the reference graph and the identification graph with respect to the uniqueness constraint of this class are shown in Figure \ref{fig-graph}. \qed

\begin{figure}
\begin{center}
\setlength{\unitlength}{1cm}

\begin{picture}(14.5,5)
\thicklines

\put(3.0,0.5){\circle{0.5}}
\put(3.0,2.5){\circle{0.5}}
\put(3.0,2.25){\vector(0,-1){1.5}}
\put(4.25,2.5){\oval(1,1)[r]}
\put(4.25,3){\vector(-2,-1){1}}
\put(4.25,2){\line(-2,1){1}}
\put(0,3.5){\{ PAIR , {\sc MarriedPersonC} \} }
\put(0.3,0.45){\{ PERSON \} }
\put(1.5,1.5){\{ first \} }
\put(3.5,1.5){\{ second , spouse \} }

\put(11,0.5){\circle{0.5}}
\put(11,2.5){\circle{0.5}}
\put(11,2.25){\vector(0,-1){1.5}}
\put(12.25,2.5){\oval(1,1)[r]}
\put(12.25,3){\vector(-2,-1){1}}
\put(12.25,2){\line(-2,1){1}}
\put(7.25,3.5){\{ PAIR , {\sc MarriedPersonC} \} }
\put(9.05,0.45){\{ NAT \} }
\put(9.35,1.5){\{ first \} }
\put(11.5,1.5){\{ second , spouse \} }

\end{picture}
\caption{\label{fig-graph} The reference graph and identification graph of class {\sc MarriedPersonC}}
\end{center}
\end{figure}

} \end{example} 

\begin{theorem} \label{graph-char}

\ Let $C$ be a class in a schema $\cal S$ with acyclic reference graph $G_{ref}$ such that there exist uniqueness constraints for $C$ and each $C_i$ such that $C_i$ occurs as a label in $G_{ref}$. Then $C$ is value-representable.

\end{theorem}

\begin{proof} {\rm 

\ We use induction on the maximum length of a path in $G_{ref}$. If there are no references in the structure expression $S$ of $C$ the type $T_C$ is a proper value type. Since there exists a uniqueness constraint on $C$, the identity function $id$ on $T_C$ also defines a uniqueness constraint. Hence $V_C = T_C$ satisfies the requirements of Definition \ref{value-repr}.

If there are references $r_i : C_i$ in the structure expression $S$ of $C$, then the induction hypothesis holds for each such $C_i$, because $G_{ref}$ is acyclic. Let $V_C$ result from $S$ by replacing each $r_i : C_i$ by $V_{C_i}$. Then $V_C$ satisfies the requirements of Definition \ref{value-repr}. \qed

} \end{proof} 

\begin{theorem}

\ Let $C$ be a class in a schema $\cal S$ such that there exist an acyclic identification graph $G_{id}$ and uniqueness constraints for $C$ and each $C_i$ occuring as a label in $G_{id}$. Then $C$ is value-identifiable.

\end{theorem}

\begin{proof} {\rm 

\ The proof is analogous to that of Theorem \ref{graph-char}. \qed

} \end{proof} 

\begin{theorem} \label{simple-char}

\ Let $C$ be a class with acyclic reference graph in a schema $\cal S$. Then the value-representability of $C$ is decidable.

\end{theorem}

\begin{proof} {\rm 

\ So far the only explicit constraints in our model are uniqueness constraints. According to Definition \ref{constraint} equality of identifiers occurs only as a positive literal in such constraints. Therefore, it is impossible to derive a uniqueness constraint for a class $C$ that has not one a priori. Theorem \ref{graph-char} implies that value-representability can be decided by checking the existence of uniqueness constraints in the class definitions. \qed

} \end{proof} 

\begin{theorem}

\ Let $C$ be a class in a schema $\cal S$ such that there exist an acyclic identification graph. Then the value-identifiability of $C$ is decidable.

\end{theorem}

\begin{proof} {\rm 

\ The proof is analogous to that of Theorem \ref{simple-char}. \qed

} \end{proof} 

\subsection{Computation of Value Representation Types}

We want to address the more general case where cyclic references may occur in the schema ${\cal S} = \{ C_1 , \ldots , C_n \}$. In this case a simple induction argument as in the proof of Theorem \ref{graph-char} is not applicable. So we take another approach. We define algorithms to compute types $V_C$ and $I_C$ that turn out to be proper value types under certain conditions. In the next subsection we then show that these types are the value representation type and the value identification type required by Definition \ref{value-repr}.

\begin{algorithm} {\rm \label{alg-vc}

Let $G(C_i) = T_{C_i}$ provided there exists a uniqueness constraint on $C_i$, otherwise let $G(C_i)$ be undefined. If $ID$ occurs in some $G(C_i)$ corresponding to $r_j : C_j$ ($j \neq i$), we write $ID_j$.

Then iterate as long as possible using the following rules: 

\begin{enumerate}

\item If $G(C_j)$ is a proper value type and $ID_j$ occurs in some $G(C_i)$ ($j \neq i$), then replace this corresponding $ID_j$ in $G(C_i)$ by $G(C_j)$.

\item If $ID_i$ occurs in some $G(C_i)$, then let $G(C_i)$ be recursively defined by $G(C_i) == S_i$, where $S_i$ is the result of replacing $ID_i$ in $G(C_i)$ by the type name $G(C_i)$.

\end{enumerate}

\noindent
This iteration terminates, since there exists only a finite collection of classes. If these rules are no longer applicable, replace each remaining occurrence of $ID_j$ in $G(C_i)$ by the type name $G(C_j)$ provided $G(C_j)$ is defined. \qed

} \end{algorithm} 

\noindent
Note that the the algorithm computes (mutually) recursive types.
Now we give a sufficient condition for the result of Algorithm \ref{alg-vc} to be a proper value type.

\begin{lemma} \label{lemma-vc}

\ Let $C$ be a class in a schema $\cal S$ such that there exists a uniqueness constraint for all classes $C_i$ occurring as a label in the reference graph $G_{ref}$ of $C$. Let $V_C$ be the type $G(C)$ computed by Algorithm \ref{alg-vc}. Then $V_C$ is a proper value type.

\end{lemma}

\begin{proof} {\rm 

\ Suppose $V_C$ were not a proper value type. Then there exists at least one occurrence of $ID$ in $V_C$. This corresponds to a class $C_i$ without uniqueness constraint occurring as a label in $G_{ref}$, hence contradicts the assumption of the lemma. \qed

} \end{proof} 

\begin{algorithm} {\rm \label{alg-ic} 

Let $F(C_i) = T_i$ provided there exists a uniqueness constraint on $C_i$ defined by $c_i: T_{C_i} \rightarrow T_i$, otherwise let $F(C_i)$ be undefined. If $ID$ occurs in some $F(C_i)$ corresponding to $r_j : C_j$ ($j \neq i$), we write $ID_j$.

Then iterate as long as possible using the following rules: 

\begin{enumerate}

\item If $F(C_j)$ is a proper value type and $ID_j$ occurs in some $F(C_i)$ ($j \neq i$), then replace this corresponding $ID_j$ in $F(C_i)$ by $F(C_j)$.

\item If $ID_i$ occurs in some $F(C_i)$, then let $F(C_i)$ be recursively defined by $F(C_i) == S_i$, where $S_i$ is the result of replacing $ID_i$ in $F(C_i)$ by the type name $F(C_i)$.

\end{enumerate}

\noindent
This iteration terminates, since there exists only a finite collection of classes. If these rules are no longer applicable, replace each remaining occurrence of $ID_j$ in $F(C_i)$ by the type name $F(C_j)$ provided $F(C_j)$ is defined. \qed

} \end{algorithm} 

\begin{lemma} \label{lemma-ic}

\ Let $C$ be a class in a schema $\cal S$ such that there exists a uniqueness constraint for all classes $C_i$ occurring as a label in some identification graph $G_{id}$ of $C$. Let $I_C$ be the type $F(C)$ computed by Algorithm \ref{alg-ic} with respect to the uniqueness constraints used in the definition of $G_{id}$. Then $I_C$ is a proper value type.

\end{lemma}

\begin{proof} {\rm 

The proof is analogous to that of Lemma \ref{lemma-vc}. \qed

} \end{proof} 

\subsection{The Finiteness Property} \label{finiteness}

Let us now address the general case. The basic idea is that there is always only a finite number of objects in a database. Assuming the database being consistent with respect to inclusion and referential constraints yields that there can not exist infinite cyclic references. This will be expressed by the {\em finiteness property}.
We show that this property implies the decidability of value-representability provided the type system allows recursive types to be defined in such a way that all their values are finitely representable, i.e. representable as rational trees. Note that the type specifications introduced in Section \ref{types} satisfy this property.

\begin{definition} {\rm \label{cycle}

\ Let $C$ be a class in a schema $\cal S$ and let $g_{k,l}$ denote a path in $G_{ref}$ from $v_{C_k}$ to $v_{C_l}$ provided there is a reference $r_l : C_l$ in the structure expression of $C_k$. Then a {\em cycle} in $G_{ref}$ is a sequence $g_{0,1} \cdots g_{n-1,n}$ with $C_0 = C_n$ and $C_k \neq C_l$ otherwise.

} \end{definition} 

\noindent
Note that we use paths instead of edges, because the edges in $G_{ref}$ do not always correspond to references.
According to our definition of a class there exists a referential constraint on $C_k$, $C_l$ defined by $o_{k,l} : T_{C_k} \times ID \rightarrow BOOL$ corresponding to $g_{k,l}$. Therefore, to each cycle there exists a corresponding sequence of functions $o_{0,1} \cdots o_{n-1,n}$. This can be used as follows to define a function $cyc: ID \times ID \rightarrow BOOL$ corresponding to a cycle in $G_{ref}$.

\begin{definition} {\rm \label{cycle-rel}

\ Let $C$ be a class in a schema $\cal S$ and let $g_{0,1} \cdots g_{n-1,n}$ be a cycle in $G_{ref}$. The corresponding {\em cycle relation} $cyc: ID \times ID \rightarrow BOOL$ is defined by $cyc(i,j) = true$ iff there exists a sequence $i = i_0 , i_1 , \ldots , i_n = j$ ($n \neq 0$) such that $( i_l , v_l ) \in C_l$ and $o_{l,l+1} ( i_{l+1} , v_l ) = true$ for all $l = 0 , \ldots , n-1$.

} \end{definition} 

\noindent
Given a cycle relation $cyc$, let $cyc^m$ the $m$-th power of $cyc$.

\begin{lemma} \label{fin-ass}

\ Let $C$ be a class in a schema $\cal S$. Then $C$ satisfies the finiteness property, i.e. for each instance $\cal D$ of $\cal S$ and for each cycle in $G_{ref}$ the corresponding cycle relation $cyc$ satisfies

\[ \forall i \in dom(C) . \, \exists n . \, \forall j \in dom(C) . \, \exists m < n . \; ( \, cyc^n(i,j) = true \, \Rightarrow \, cyc^m(i,j) = true \, ) \; . \]

\end{lemma}

\begin{proof} {\rm 

Suppose the finiteness property were not satisfied. Then there exist an instance $\cal D$, a cycle relation $cyc$ and an object identifier $i_0$ such that

\[ \forall n . \, \exists j \in dom(C) . \, \forall m < n . \; ( \, cyc^n(i_0,j) = true \, \wedge \, cyc^m(i_0,j) = false \, ) \]

\noindent
holds. Let such a $j$ corresponding to $n > 0$ be $i_n$. Then the elements $i_0 , i_1 , i_2 , \ldots$ are pairwise distinct. Hence there would be infinitely many objects in $\cal D$ contradicting the finiteness of a database. \qed

} \end{proof} 

\begin{lemma} \label{lemma2-vc}

\ Let $\cal D$ be an instance of schema ${\cal S} = \{ C_1 , \ldots , C_n \}$. Then $\cal D$ satisfies at each stage of Algorithm \ref{alg-vc} uniqueness constraints for all $i = 1 , \ldots , n$ defined by some $c_i : T_{C_i} \rightarrow G(C_i)$.

\end{lemma}

\begin{proof} {\rm 

It is sufficient to show that whenever a rule is applied replacing $G(C_i)$ by $G(C_i)^\prime$, then $G(C_i)^\prime$ also defines a uniqueness constraint on $C_i$.

Suppose that $Pair(i,v) \in C_i$ holds in $\cal D$. Since it is possible to apply a rule to $G(C_i)$, there exists at least one value $j :: ID$ occurring in $c_i(v)$. Replacing $ID_j$ in $G(C_i)$ corresponds to replacing $j$ by some value $v_j :: G(C_j)$. Because of the finiteness property such a value must exist. Moreover, due to the uniqueness constraint defined by $c_j$ the function $f : G(C_i) \rightarrow G(C_i)^\prime$ representing this replacement must be injective on $c_i(codom_{\cal D}(C_i))$. Hence, $c_i^\prime = f \circ c_i$ defines a uniqueness constraint on $C_i$. \qed

} \end{proof} 

\begin{lemma} \label{lemma2-ic}

\ Let $\cal D$ be an instance of schema ${\cal S} = \{ C_1 , \ldots , C_n \}$. Then $\cal D$ satisfies at each stage of Algorithm \ref{alg-ic} uniqueness constraints for all $i = 1 , \ldots , n$ defined by some $c_i^\prime : T_{C_i} \rightarrow F(C_i)$.

\end{lemma}

\begin{proof} {\rm 

The proof is analogous to the proof of Lemma \ref{lemma2-vc}. \qed

} \end{proof} 

\begin{lemma} \label{lemma-vc-ic}

Let $\cal D$ be an instance of schema ${\cal S} = \{ C_1 , \ldots , C_n \}$. Then at each stage of the algorithms \ref{alg-vc} and \ref{alg-ic} for all $i = 1 , \ldots , n$ there exists a function $\bar{c}_i : G(C_i) \rightarrow F(C_i)$ that is unique on $c_i(codom_{\cal D}(C_i))$ with $c_i^\prime = \bar{c}_i \circ c_i$.

\end{lemma}

\begin{proof} {\rm 

As in the proof of Lemma \ref{lemma2-vc} it is sufficient to show that the required property is preserved by the application of a rule from Algorithm \ref{alg-vc} or \ref{alg-ic}. Therefore, let $\bar{c}_i$ satisfy the required property and let $g : G(C_i) \rightarrow G(C_i)^\prime$ and $f : F(C_i) \rightarrow F(C_i)^\prime$ be functions corresponding to the application of a rule to $G(C_i)$ and $F(C_i)$ respectively. Such functions were constructed in the proofs of Lemma \ref{lemma2-vc} and Lemma \ref{lemma2-ic} respectively. 

Then $f \circ \bar{c}_i$ satisfies the required property with respect to the application of $f$. In the case of applying $g$ we know that $g$ is injective on $c_i(codom_{\cal D}(C_i))$. Let $h : G(C_i)^\prime \rightarrow G(C_i)$ be any continuation of $g^{-1} : g(c_i(codom_{\cal D}(C_i))) \rightarrow G(C_i)$. Then $\bar{c}_i \circ h$ satisfies the required property. \qed

} \end{proof} 

\begin{theorem} \label{vc-theorem}

\ Let $C$ be a class in a schema $\cal S$ such that there exists a uniqueness constraint for all classes $C_i$ occurring as a label in the reference graph $G_{ref}$ of $C$. Let $V_C$ be the type $G(C)$ computed by Algorithm \ref{alg-vc}. Then $C$ is value-representable with value representation type $V_C$.

\end{theorem}

\begin{proof} {\rm 

\ $V_C$ is a proper value type by Lemma \ref{lemma-vc}. From Lemma \ref{lemma2-vc} it follows that if $\cal D$ is an instance of $\cal S$, then there exists a function $c : T_C \rightarrow V_C$ such that the uniqueness constraint defined by $c$ holds for $\cal D$. 

If $V_C^\prime$ is another proper value type and $\cal D$ satisfies a uniqueness constraint defined by $c^\prime : T_C \rightarrow V_C^\prime$, then $V_C^\prime$ is some value-identification type $I_C$. Hence by Lemma \ref{lemma-vc-ic} there exists a function $c^\prime{}^\prime : V_C \rightarrow V_C^\prime$ that is unique on $c(codom_{\cal D}(C))$ with $c^\prime = c^\prime{}^\prime \circ c$. This proves the Theorem. \qed

} \end{proof}

\begin{corollary} 

\ Let $\cal S$ be a schema such that all classes $C$ in $\cal S$ are value-identifiable. The all classes $C$ in $\cal S$ are also value-representable. \qed

\end{corollary} 

\begin{theorem} \label{ic-theorem}

\ Let $C$ be a class in a schema $\cal S$ such that there exists a uniqueness constraint for all classes $C_i$ occurring as a label in some identification graph $G_{id}$ of $C$. Let $I_C$ be the type $F(C)$ computed by Algorithm \ref{alg-ic} with respect to the uniqueness constraints used in the definition of $G_{id}$. Then $C$ is value-identifiable with value identification type $I_C$.

\end{theorem}

\begin{proof} {\rm 

The proof is analogous to that of Theorem \ref{vc-theorem}. \qed

} \end{proof} 

\begin{theorem} \label{fin-theorem}

\ Let $C$ be a class in a schema $\cal S$. Then the value-representability and the value-identifiability of $C$ are decidable.

\end{theorem}

\begin{proof} {\rm 

The proof is analogous to that of Theorem \ref{simple-char}. \qed

} \end{proof} 

\section{Weak Value-Representability}

Let us now ask whether there exist also weaker identification mechanisms
other than value-representability. In several papers, e.g. \cite{ohori} a
navigational approach on the basis of the reference structure has been
favoured. This leads to dependent classes similar to ``weak entities'' in the
entity-relationship model \cite{herm}. We shall show that such an approach
requires at least a value-identifiable ``entrance'' of some path and the hard
restriction on references to be representable by surjective functions.

\begin{definition} {\rm \label{wv-ident}

\ Let $\cal S$ be some schema.

\begin{enumerate}

\item If $r$ is a reference from class $C$ to $D$ in $\cal S$ and $o : T_C
\times ID \rightarrow BOOL$ is the function of Definition \ref{ric} expressing
the corresponding referential constraint, then $r$ satisfies the {\em
(SF)-condition}\/ iff

\begin{enumerate}

\item $o(v,i) = true \wedge o(v,j) = true \; \Rightarrow \; i = j$ and

\item $member(j,dom(x_D)) = true \; \Rightarrow \; \exists v :: T_C . \, member(v,codom(x_C)) = true \wedge o(v,j) = true$

\end{enumerate}

\noindent
hold for all $i,j :: ID , v :: T_C$.

\item An {\em (SF)-chain}\/ from class $D$ to $C$ in $\cal S$ is a sequence of classes $D = C_0 , \ldots , C_n = C$ together with references $r_i$ ($i = 1 , \ldots , n$) from $C_{i-1}$ to $C_i$ such that each $r_i$ satisfies the (SF)-condition.

\item A class $C$ in $\cal S$ is called {\em weakly value-identifiable}\/ iff there exists a value-identifiable class $D$ and an (SF)-chain from $D$ to $C$.

\end{enumerate}

} \end{definition}

\noindent
The notation (SF)-condition has been chosen to emphasize that such a reference represents a surjective function. It is easy to see taking $n = 0$ that each value-identifiable class is also weakly value-identifiable.

\begin{lemma} \label{wv-lemma1}

If $C$ is a weakly value-identifiable class in a schema $\cal S$, then there exists a proper value type $I_C$ such that for each instance $\cal D$ of $\cal S$ there exists a function $c : ID \rightarrow I_C$ such that $c$ is injective on $dom_{\cal D}(C)$.

\end{lemma}

\noindent
Call $I_C$ a {\em weak value-identification type}\/ of the class $C$.

\begin{proof} {\rm 

\ Let $D = C_0 , \ldots , C_n = C$ be an (SF)-chain from the value-identifiable class $D$ to $C$ with corresponding references $r_i$ ($i = 1 , \ldots , n$). Since $r_i$ satisfies the (SF)-condition, there exists a function $c_i : ID \rightarrow ID$ such that $j \in dom_{\cal D}(C_i) \Rightarrow (c_i(j),v) \in x_{C_{i-1}}$ for some $v$ with $o_i(v,j) = true$ (just take some inverse image of $j$ under the surjective reference function). Since $r_i$ defines a function, $c_i$ is clearly injective.

If $c^\prime : ID \rightarrow I_D$ is the function defined by the uniqueness constraint on $D$ and $c^\prime{}^\prime : ID \rightarrow ID$ is the concatenation $c_1 \circ \ldots \circ c_n$, then $c = c^\prime \circ c^\prime{}^\prime$ satisfies the required property. \qed

} \end{proof}

\begin{problem}

\ Does the converse of Lemma \ref{wv-lemma1} also hold? 

\end{problem}

\begin{definition} {\rm \label{wv-rep}

A class $C$ in a schema $\cal S$ is called {\em weakly value-representable}\/ iff there exists a proper value type $V_C$ such that for each instance $\cal D$ of $\cal S$ the following properties hold.

\begin{enumerate}

\item There is a function $c : ID \rightarrow V_C$ that is injective on $dom_{\cal D}(C)$.

\item For each proper value type $V_C^\prime$ and each function $c^\prime : ID \rightarrow V_C^\prime$ that is injective on $dom_{\cal D}(C)$ there exists a function $c^\prime{}^\prime : V_C \rightarrow V_C^\prime$ that is unique on $c(dom_{\cal D}(C))$ with $c^\prime = c^\prime{}^\prime \circ c$.

\end{enumerate}

\noindent
We call $V_C$ the {\em weak value-representation type}\/ of the class $C$.

} \end{definition}

\noindent
Note that the weak value-representation type is unique provided it exists. Again it is easy to see that value-representability implies weak value-representability. Moreover, due to Lemma \ref{wv-lemma1} each weakly value-representable class is also weakly value-identifiable. We shall see that also the converse of this fact is true.

\begin{algorithm} {\rm \label{alg-wv}

Let the schema be ${\cal S} = \{ C_1 , \ldots , C_n \}$. Start with $H(C_i) = T_{C_i}$ ($i = 1 , \ldots , n$). If $ID$ occurs in some $H(C_i)$ corresponding to $r_j : C_j$ ($j \neq i$), we write $ID_j$.

Then iterate as long as possible using the following rules: 

\begin{enumerate}

\item If $H(C_j)$ is a proper value type and $ID_j$ occurs in some $H(C_i)$ ($j \neq i$), then replace this corresponding $ID_j$ in $H(C_i)$ by $H(C_j)$.

\item If $ID_i$ occurs in some $H(C_i)$, then let $H(C_i)$ be recursively defined by $H(C_i) == S_i$, where $S_i$ is the result of replacing $ID_i$ in $H(C_i)$ by the type name $H(C_i)$.

\end{enumerate}

\noindent
This iteration terminates, since there exists only a finite collection of classes. If these rules are no longer applicable, replace each remaining occurrence of $ID_j$ in $H(C_i)$ by the type name $H(C_j)$. \qed

} \end{algorithm}

\noindent
This algorithm is similar to the Algorithms \ref{alg-vc} and \ref{alg-ic}. However, we completely ignore uniqueness constraints.

\begin{lemma} \label{wv-lemma2}

\ Let $C$ be a class in a schema $\cal S$ and let $I_C$ be the type $H(C)$
computed by Algorithm \ref{alg-wv}. Then $I_C$ is a proper value type.

\end{lemma}

\begin{proof} {\rm 

The proof is analogous to that of Lemma \ref{lemma-vc}. \qed

} \end{proof}

\begin{lemma} \label{wv-lemma3}

Let $\cal D$ be an instance of the schema ${\cal S} = \{ C_1 , \ldots , C_n \}$. Let $C$, $D$ be classes such that $C$ is weakly value-identifiable, $D$ is value-identifiable and there exists some (SF)-chain from $D$ to $C$. Let $c : ID \rightarrow I_C$ be the function of Lemma \ref{wv-lemma1} corresponding to this chain. Let $c^\prime : ID \rightarrow H(D)$ be a function corresponding to the uniqueness constraint on $D$ and the instance $\cal D$.
Then at each stage of the Algorithm \ref{alg-wv} there exists a function $\bar{c} : H(D) \rightarrow I_C$ that is unique on $c^\prime(dom_{\cal D}(C))$ with $c = \bar{c} \circ c^\prime$.

\end{lemma}

\begin{proof} {\rm 

The proof is analogous to the one of Lemma \ref{lemma2-vc}. \qed

} \end{proof}

\begin{theorem} \label{wv-theorem}

Let $C$ be a weakly value-identifiable class in a schema $\cal S$ and let $V_C$ be the product of all types $H(D)$, where $D$ is the leading value-identifiable class in some maximal (SF)-chain corresponding to $C$ and $H(D)$ is the result of Algorithm \ref{alg-wv}. Then $C$ is weakly value-representable with weak value-representation type $V_C$.

\end{theorem}

\begin{proof} {\rm

\ $V_C$ is a proper value type by Lemma \ref{wv-lemma2}. From Lemmata \ref{lemma2-ic} and \ref{wv-lemma1} it follows that there exists a function $c^\prime : ID \rightarrow V_C$ that is injective on $dom_{\cal D}(C)$.

From Lemma \ref{wv-lemma3} it follows that there exists a function $\bar{c} : V_C \rightarrow I_C$ that is unique on $c^\prime(dom_{\cal D}(C))$ with $c = \bar{c} \circ c^\prime$. This proves the Theorem.\qed

} \end{proof}

\chapter{Genericity} \label{genericity}

The preservation of advantages of relational databases requires the definability of generic operations for querying and for the insertion, deletion and update of single objects.
While querying \cite{abiteboul,bk,heuer,shaw} is per se a set-oriented operation, i.e. it is not necessary to select just one single object, and hence does not raise any specific problems with object identifiers, things change completely in case of updates. If an object with a given value is to be updated (or deleted), this is only defined unambigously, if there does not exist another object with the same value. If more than one object exists with the same value or more generally with the same value and the same references to other objects, then the user has to decide, whether an update- or delete-operation is applied to {\em all} these objects, to only {\em one} of these objects selected non-deterministically or to {\em none} of them, i.e. to reject the operation.
However, it is not possible to specify a priori such an operation that works in the same way for all objects in all situations. The same applies to insert-operations. Hence the problem, in which cases operations for the insertion, deletion and update of objects can be defined generically.

Some authors \cite{saake} have chosen the solution to abandon generic operations. Others \cite{albano1,albano,o2} use identifying values to represent object identity, thus embody a strict concept of surrogate keys to avoid the problem. Our approach is different from both solutions in that we use the concept of hidden abstract identifiers, but at the same time formally characterize those classes for which generic operations for the insertion, deletion and update of single objects can be derived automatically. We show that there is a close connection between {\em value-representability}\/ and the unique existence of generic operations for the insertion, deletion and update of single objects. Furthermore, inclusion and
referential integrity are enforced by these operations. 

In Section \ref{generic} we describe these operations. In Section \ref{generator} we then specify an algorithm to compute generic update methods \cite{generator,rib}. The specification is built on the same theoretical ground as the OODM, hence sets up a specific case of linguistic reflection \cite{reflection}.

\section{Existence and Consistency of Generic Update Operations} \label{generic}

{\em Methods} are used to specify the dynamics of an object-oriented database. Here, we do not want to give a concrete language for methods. In general methods can be specified in the style of Dijkstra focussing on deterministic operations \cite{iwsds}.

In this paper we are only interested in {\em canonical update operations}, i.e. we want to associate with each class $C$ in a schema $\cal S$ {\em methods} for {\em insertion}, {\em deletion}\/ and {\em update}\/ on single objects. These operations should be consistent with respect to the constraints in $\cal S$. Thus, they are sufficient to express the creation, deletion and change of objects including the migration between classes. However, we would like to regard these operations as being ``generic'' in the sense of polymorphic functions, since insert, delete and update should be defined for each class. The problem is that the input-type and the body of these operations require information from the schema. This leads to polymorphism with respect to meta-types. For the purpose of this paper we do not discuss this problem.

\subsection{Canonical Update Operations}

The requirement that object-identifiers have to be hidden from the user imposes the restriction on canonical update operations to be value-defined in the sense that the identifier of a new object has to be chosen by the system whereas all input- and output-data have to be values of proper value types.

We now formally define canonical update operations. For this purpose regard an instance $\cal D$ of a schema $\cal S$ as a set of objects. For each recursively defined type $T$ let $\bar{T}$ denote by replacing each occurrence of a recursive type $T^\prime$ in $T$ by $UNION(T^\prime,ID)$.

\begin{definition} {\rm \label{generic-upd}

Let C be a class in a schema $\cal S$. {\em Canonical update operations} on $C$ are $insert_C$, $delete_C$ and $update_C$ satisfying the following properties:

\begin{enumerate}

\item Their input types are proper value types; their output type is the trivial type $\bot$.

\item In the case of $insert$ applied to an instance $\cal D$ there exists a distinguished object $o :: PAIR(ID,T_C)$ such that

\begin{enumerate}

\item the result is an instance ${\cal D}^\prime$ with $o \in {\cal D}^\prime$ and ${\cal D} \subseteq {\cal D}^\prime$ hold and

\item if $\bar{\cal D}$ is any instance with ${\cal D} \subseteq \bar{\cal D}$ and $o \in \bar{\cal D}$, then ${\cal D}^\prime \subseteq \bar{\cal D}$.

\end{enumerate}

\item In the case of $delete$ applied to an instance $\cal D$ there exists a distinguished object $o :: PAIR(ID,T_C)$ such that

\begin{enumerate}

\item the result is an instance ${\cal D}^\prime$ with $o \not\in {\cal D}^\prime$ and ${\cal D}^\prime \subseteq {\cal D}$ hold and

\item if $\bar{\cal D}$ is any instance with $\bar{\cal D} \subseteq {\cal D}$ and $o \not\in \bar{\cal D}$, then $\bar{\cal D} \subseteq {\cal D}^\prime$.

\end{enumerate}

\item In the case of $update$ applied to an instance ${\cal D} = {\cal D}_1 \disunion {\cal D}_2$, where ${\cal D}_2 = \{ o \}$ if $o \neq o^\prime$ and ${\cal D}_2 = \emptyset$ otherwise there exist distinguished objects $o,o^\prime :: PAIR(ID,T_C)$ with $o = Pair(i,v)$ and $o^\prime = Pair(i,v^\prime)$ such that

\begin{enumerate}

\item the result is an instance ${\cal D}^\prime = {\cal D}_1 \disunion {\cal D}_2^\prime$ with ${\cal D}_2 \cap {\cal D}_2^\prime = \emptyset$,

\item $o \in {\cal D}$, $o^\prime \in {\cal D}^\prime$,

\item if $\bar{\cal D}$ is any instance with ${\cal D}_1 \subseteq \bar{\cal D}$ and $o^\prime \in \bar{\cal D}$, then ${\cal D}^\prime \subseteq \bar{\cal D}$.

\end{enumerate}

\end{enumerate}

\noindent
{\em Quasi-canonical update operations} on $C$ are $insert_C^\prime$, $delete_C^\prime$ and $update_C^\prime$ defined analogously with the only difference of their output type being $ID$ and their input-type being $\bar{T}$ for some value-type $T$.

} \end{definition} 

\noindent
Note that this definition of canonical update operations includes the consistency with respect to the implicit and explicit constraints on $\cal S$. We show that value-representability is sufficient for the existence and uniqueness of such operations. We use a guarded command notation as in \cite{iwsds} for these update operations.

\begin{lemma} \label{lemma28}

\ Let $C$ be a class in a schema $\cal S$ such that there exist quasi-canonical update operations on $C$. Then also canonical update operations exist on $C$.

\end{lemma}

\begin{proof} {\rm 

\ In the case of {\em insert} define $insert_C (V :: V_C) == I \leftarrow insert_C^\prime (V)$, i.e. call the corresponding quasi-canonical operation and ignore its output. The same argument applies to {\em delete} and {\em update}. \qed

} \end{proof} 

\subsection{Existence of Canonical Updates in the Case of Value-Representability}
Our next goal is to reduce the existence problem of quasi-canonical update operations to schemata without IsA relations.

\begin{lemma} \label{lemma29}

Let $C$, $D$ be value-representable classes in a schema $\cal S$ such that $C$ is a subclass of $D$ with subtype function $g : T_C \rightarrow T_D$. Then there exists a function $h : V_C \rightarrow V_D$ such that for each instance $\cal D$ of $\cal S$ with corresponding functions $c : T_C \rightarrow V_C$ and $d : T_D \rightarrow V_D$ we have $h(c(v)) = d(g(v))$ for all $v \in codom_{\cal D}(C)$.

\end{lemma}

\begin{proof} {\rm 

\ By Definition \ref{value-repr} $c$ is injective on $codom_{\cal D}(C)$, hence any continuation $h$ of $d \circ g \circ c^{-1}$ satisfies the required property.

It remains to show that $h$ does not depend on $\cal D$. Suppose ${\cal D}_1$, ${\cal D}_2$ are two instances such that $w = c_1(v_1) = c_2(v_2) \in V_C$, where $c_1 ,d_1, h_1$ correspond to ${\cal D}_1$ and $c_2 ,d_2, h_2$ correspond to ${\cal D}_2$. Then there exists a permutation $\pi$ on $ID$ such that $v_2 = \pi(v_1)$. We may extend $\pi$ to a permutation on any type. Since $ID$ has no non-trivial supertype, $g$ permutes with $\pi$, hence $g(v_2) = \pi(g(v_1))$. From Definition \ref{value-repr} it follows $d_2(g(v_2)) = d_1(g(v_1))$, i.e. $h_2(w) = h_1(w)$. \qed

} \end{proof} 

\noindent
In the following let ${\cal S}_0$ be a schema derived from a schema $\cal S$ by omitting all IsA relations.

\begin{lemma} \label{lemma30}

\ Let $C$ be a value-representable class in $\cal S$ such that all its superclasses $D_1 \ldots D_n$ are also value-representable. Then quasi-canonical update operations exist on $C$ in $\cal S$ iff they exist on $C$ and all $D_i$ in ${\cal S}_0$.

\end{lemma}

\begin{proof} {\rm 

\ By Theorem \ref{vc-theorem} the value-representation type $V_C$ is the result of Algorithm \ref{alg-vc}, hence $V_C$ does not depend on the inclusion constraints of $\cal S$. Then we have
\begin{eqnarray*} 
&& I :: ID \, \leftarrow \, insert_C^\prime(V :: V_C) == \\
&& \hspace*{20pt} I \leftarrow insert_{D_1}^\prime(h_1(V)) ; \ldots ; I \leftarrow insert_{D_n}^\prime(h_n(V)) ; I \leftarrow insert_C^0(V) \; \; \; ,
\end{eqnarray*}
\noindent
where $h_i : V_C \rightarrow V_{D_i}$ is the function of Lemma \ref{lemma29} and $insert_C^0$ denotes a quasi-canonical insert on $C$ in ${\cal S}_0$. Hence in this case the result for the {\em insert} follows by structural induction on the IsA-hierarchy.

If the subtype function $g$ required in Lemma \ref{lemma29} does not exist for some superclass $D$ then simply add $V_D$ to the input type. We omit the details for this case.

The arguments for {\em delete}\/ and {\em update}\/ are analogous. \qed

} \end{proof} 

\noindent
Now assume the existence of a global operation $NewId$ that produces a fresh identifier $I :: ID$.

\begin{lemma} \label{lemma31}

\ Let $C$ be a value-representable class in ${\cal S}_0$. Then there exist unique quasi-canonical update operations on $C$.

\end{lemma}

\begin{proof} {\rm 

\ Let $r_i : C_i$ ($i = 1 \ldots n$) denote the references in the structure expression of $C$. If $V$ be a value of type $\bar{V_C}$, then there exist values $V_{i,j} :: \bar{V_{C_i}}$ ($i = 1 \ldots n , j = 1 \ldots k_i$) occurring in $V$. Let $\bar{V} = \{ V_{i,j} / J_{i,j} \mid i = 1 \ldots n , j = 1 \ldots k_i \} . V$ denote the value of type $T_C$ that results from replacing each $V_{i,j}$ by some $J_{i,j} :: ID$. Moreover, for $I :: ID$ let 
\[ V_{i,j}^{(I)} = \left \{ \begin{array}{ccl}
\{ V / I \} . V_{i,j} && \mbox{if } V \mbox{ occurs in } V_{i,j}\\
V_{i,j} && \mbox{else} \end{array} \right . \]
Then the quasi-canonical insert operation can be defined as follows: 
\begin{eqnarray*}
&& I :: ID \leftarrow insert_C^\prime ( V :: \bar{V_C} ) \, == \\
&& IF \; \exists \, I^\prime :: ID \, , \, V^\prime :: T_C . \; ( Pair(I^\prime,V^\prime) \in C \, \wedge \, c(V^\prime) = V ) \\
&& THEN \; I := I^\prime\\
&& ELSE \; I \leftarrow NewId \: ; \: J_{1,1} \leftarrow insert_{C_1}^\prime (V_{1,1}^{(I)}) \, ; \, \ldots \, ; \, J_{n,k_n} \leftarrow insert_{C_n}^\prime (V_{n,k_n}^{(I)}) \, ; \\
&& \hspace*{45pt} C := C \cup \{ Pair(I,\bar{V}) \}\\
&& FI
\end{eqnarray*} 
\noindent
It remains to show that this operation is indeed quasi-canonical. Apply the operation to some instance $\cal D$. If there already exists some object $o = Pair(I^\prime,V^\prime)$ in $C$ with $c(V^\prime) = V$, the result is ${\cal D}^\prime = {\cal D}$ and the requirements of Definition \ref{generic-upd} are trivially satisfied. Otherwise let the distinguished object be $o = Pair(I,\bar{V})$. If $\bar{\cal D}$ is an instance with ${\cal D} \subseteq \bar{\cal D}$ and $o \in \bar{\cal D}$, we have $J_{i,j} \in dom(C_i)$ for all $i = 1 \ldots n$, $j = 1 \ldots k_i$, since $\bar{\cal D}$ satisfies the referential constraints. Hence $\bar{\cal D}$ contains the distinguished objects corresponding to the involved quasi-canonical operations $insert_{C_i}^\prime$. By induction on the length of call-sequences ${\cal D}_{i,j} \subseteq \bar{\cal D}$ for all $i = 1 \ldots n$, $j = 1 \ldots k_i$, where ${\cal D}_{i,j}$ is the result of $J_{i,j} \leftarrow insert_{C_i}^\prime(V_{i,j}^{(I)})$. Hence ${\cal D}^\prime = \bigcup\limits_{i,j} {\cal D}_{i,j} \, \cup \, \{ o \} \subseteq \bar{\cal D}$. The uniqueness follows from the uniqueness of $V_C$.

The definitions and proofs for {\em delete}\/ and {\em update}\/ are analogous. \qed

} \end{proof} 

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

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

\end{theorem}

\begin{proof} {\rm 

\ By Lemma \ref{lemma28} and Lemma \ref{lemma30} it is sufficient to show the existence of quasi-canonical update operations on $C$ and all its superclasses in the schema ${\cal S}_0$. This follows from Lemma \ref{lemma31}. \qed

} \end{proof} 

\section{A Generator Approach to Achieve Higher-Level Genericity} \label{generator}

Our aim is to generate canonical update methods {\em insert$_C$}, {\em delete$_C$} and {\em update$_C$} for each class $C$ of a database schema. These operations demand the identification of objects without accessing the object identifier, since {\em oid}s are an internal concept and do not have a meaning for the user of a database. Hence the need for {\em value-representability}. Besides this identification problem we also have to cope with the enforcement of implicit integrity constraints. In Section \ref{value-rep} it has been shown that value-representability is a necessary and sufficient condition for the existence of consistent canonical update operations.

These update operations are ``generic'' in the sense, that they are applicable to each class of a schema. Our aim now is to provide an algorithmic solution to the generation of canonical update operations. A natural first idea is to exploit polymorphism as in \cite{quest} for this task. However, canonical consistent updates on a class $C$ require an input-type $V_C$ without any occurrence of $ID$. Such an input-type has to be computed from the schema. Hence the generation of such operations requires meta-information. It has been shown in \cite{base,limits} that the need for meta-information exceeds the capability of polymorphism. Two solutions are then possible:

\begin{itemize}

\item introduce polymorphic meta-types or

\item use linguistic reflection as proposed in \cite{reflection}.

\end{itemize}

\noindent
The first approach is fine as long as we do not care about decidability problems in type checking, however, reflection is more practical.

The basic idea of linguistic reflection is to use representation types such as $SCHEMA_{rep}$, $CLASS_{rep}$ and $TYPE_{rep}$ for the representation of abstract syntax expressions representing schemata, class definitions and type declarations respectively. For each of these, there exists a function $raise$ associating with this syntactic expression a true schema, class or type respectively. Moreover, we need functions $i$ and $v$ with signature $SCHEMA_{rep} \times CLASS_{rep} \rightarrow TYPE_{rep}$. $v({\cal S},{\cal C})$ represents a value-type needed for the insertion of a new object into $raise({\cal C})$. Clearly, this type is also required for updates. $i({\cal S},{\cal C})$ represents a value-type needed for the identification of some object, hence is needed for delete and update-operations.

If $OPER_{rep}({\cal I},{\cal S})$ represents the operations on the schema defined by $\cal S$ (defined  via methods) with input type represented by $\cal I$, then the problem is to define three reflective functions 

\indent
\( insert : \; {\cal S} :: SCHEMA_{rep} \times {\cal C} :: CLASS_{rep} \: \rightarrow \: OPER_{rep}(v({\cal S},{\cal C}),{\cal S}) \) ,\\
\indent
\( delete : \; {\cal S} :: SCHEMA_{rep} \times {\cal C} :: CLASS_{rep} \: \rightarrow \: OPER_{rep}(i({\cal S},{\cal C}),{\cal S}) \) and\\
\indent
\( update : \; {\cal S} :: SCHEMA_{rep} \times {\cal C} :: CLASS_{rep} \: \rightarrow \: OPER_{rep}(i({\cal S},{\cal C}) \times v({\cal S},{\cal C}),{\cal S}) \).\\

\noindent
$OPER_{rep}$ is a type constructor applicable only to representation types. Clearly, we should have $OPER_{rep}(I_{rep},S_{rep}) \, = \, ( OPER(I,S) )_{rep}$, where $OPER$ is again a type constructor and $OPER(I,S)$ is the type of the operations on $S$ with input-type $I$.

\subsection{Basic Assumptions}
Since we are concerned with providing generic update operations we have to discuss the uniqueness and existence of these operations in general. 

Whenever object oriented data models include the principle of hiding identifiers from the user  insert, delete and update operations demand the unique accessibility of objects from ``outside'', i.e. by the user, in a  way different from using the internal identifiers. This is in accordance with the identifier being only an implementation concept \cite{beeri,beeripods}. Otherwise   database management of the  identifiers themselves would be required \cite{lockemann}. The approach of naming objects in a program scope usually applied in object oriented programming languages is to be ruled out in the database context. Therefore we have to require that objects within a class need to be distinguished by values and referenced objects.

Our previous work on these topics \cite{icdt,rostock} gives a characterization of those classes having objects that are completely representable by values, i.e. we can replace references by values of referred objects and identify an object by its values. These classes are called value-representable i.e. it is possible to identify each object by some value of a proper value type (without occurrence of oids). (In the case of cyclic references the finiteness of the database imposes the instances of such a type to be finitely representable).


It is shown that the value-representability of classes is decidable under certain conditions and that a unique value type (serving as input type for canonical update operations) can be derived for any value-representable class. Moreover,  the unique existence of canonical insert, delete and update operations of a class {\sl C} turns out to be guaranteed iff {\sl C} is value-representable.

\subsection{A Framework for Generator Application}
Applying the approach discussed above to practically support  meta polymorphism we need to introduce in our context:
\begin{itemize}
\item
{\em Representation types} for syntactic components of our language capturing meta information, e.g. {\sl Schema$_{rep}$, Class$_{rep}$, Type$_{rep}$} about schemata, class  and type definitions  or representing code to be generated, e.g. {\sl Meth$_{rep}$}. For each of these a function {\sl raise} exists associating with this abstract syntax a true schema, class, type or method respectively.
\item
{\em Generator functions} that are defined  on these representation types and produce again abstract syntax which extends -- after a {\em raise} --  our specification. In particular we need a generator {\sl V\gen} with signature 
{\sl \begin{tabbing} 
xx \= xxxxx \= xx \= xxxx \= xx \= xx \= xx \= xx \= xx \= \kill 
\> V\gen \>:\> Schema\rep $\times$ Class\rep $\rightarrow$ Type\rep
\end{tabbing}}
deriving a value type definition serving as input type in insert and update operations. Moreover, we need at least one generator {\sl I\gen} with the same signature that derives an identification type used in delete and update operations. For the sake of simplicity we neglect {\sl I\gen} and use also {\sl V\gen} for identification.
Canonical update operations are generated by functions {\sl Insert\gen , Delete\gen, Update\gen} with signatures:
{\sl \begin{tabbing} 
xx \= xxxxxxxxx \= xx \= xxxx \= xx \= xx \= xx \= xx \= xx \= \kill 
\> Insert\gen\> : \>Schema\rep $\times$ Class\rep $\rightarrow$ Meth\rep\\
\> Delete\gen\> : \>Schema\rep $\times$ Class\rep $\rightarrow$ Meth\rep\\
\> Update\gen\> : \>Schema\rep $\times$ Class\rep $\rightarrow$ Meth\rep
\end{tabbing}}
\end{itemize}

\subsection{Representations Types}


In this section we present the definition of representation types forming the framework in which  generator functions are defined. Here we make use of general algebraic type specifications as in \cite{iwsds,bk}. However, we distinguish between constructors, selectors and other functions. Axioms are given by conditional equations. A type definition may refer to other type definitions which is indicated by the keyword {\sl basedOn}. 


We concentrate on those representation types that are necessary for defining  {\sl Insert\gen}. Constructions for {\sl Delete\gen} and {\sl Update\gen} can be given analogously. Although needed we omit all details concerning  the representation type for types and the definition of the generator for value-representation types that are needed for input.
The following type definitions provide abstract syntax values for {\em structures, classes, methods} and {\em commands}.  


The type definition for {\sl Structure\rep} uses representations of  types  as defined in \cite{icdt} on top of which structures  are built. The list of reference-name/class-name pairs indicates the references of a class whereby class objects can have a complex structure with references occurring as parameters at any level in nested type constructors. The axiom indicates  that a reference list of a structure has to be  as long as its parameter list whereby {\sl params} is a function on  types returning lists of their parameters. 
{\sl \begin{tabbing}
xx \= xx \= xx \= xxxxxxxxxx \= x  \= xx \= xx\= \kill
\>Structure\rep ==\\
\hspace{0.4 cm}
\>\> \basedOn \\
\>\>\>ClassName\rep, Type\rep, List($\alpha$), Pair($\alpha$,$\beta$), RefName\rep\\ 
\>\> \constructors\\
\>\>\> structure\con \>: \> Type\rep $\times$ List(Pair(RefName\rep,ClassName\rep)) $\rightarrow$ Structure\rep\\
\>\> \selectors\\
xx \= xx \= xx \= xxxxxxxxxxxxxx \= x \= x \= xx \= xx\= \kill
\>\>\> structureType\sel \>:\> Structure\rep $\rightarrow$ Type\rep\\
\>\>\> references\sel \>:\> Structure\rep $\rightarrow$ 
List(Pair(RefName\rep,ClassName\rep))\\
\>\> \axioms\\
\>\>\> With s : Structure\rep . \\
\>\>\>length(params(structureType\sel(s)) $=$ length(references\sel(s))\\
\>\>\eend
\end{tabbing}}
\noindent
The definition of {\sl Class\rep}  can be given in the following way omitting for now user defined methods.
{\sl \begin{tabbing}
xx \= xx \= xx \= xxxxxxx \= x  \= xx \= xx\= \kill

\>Class\rep ==\\
\hspace{0.4 cm}
\>\> \basedOn \\
\>\>\>ClassName\rep, Structure\rep, Fset($\alpha$)\\ 
\>\> \constructors\\
\>\>\> class\con \>:\> ClassName\rep  $\times$  Fset(ClassName\rep) $\times$ Structure\rep  $\rightarrow$ Class\rep\\
\>\> \selectors\\
xx \= xx \= xx \= xxxxxxxxxx \= x \= x \= xx \= xx\= \kill
\>\>\> className\sel \>:\> Class\rep $\rightarrow$ ClassName\rep\\
\>\>\> isA\sel \>:\> Class\rep $\rightarrow$ Fset(ClassName\rep)\\
\>\>\> structure\sel  \>:\> Class\rep $\rightarrow$ Structure\rep\\
\>\> \axioms $\ldots$\\
\>\>\eend
\end{tabbing}}

\noindent
An abstract representation of a method consists of its name, the
declaration of its input and output parameters together with a representation
of its body.
{\sl \begin{tabbing}
xx \= xx \= xxxxxxx \= x  \= xx \= xx\= \kill
Meth\rep =\\
\> \basedOn \\
\>\> MethName\rep, VarName\rep,
Command\rep, Type\rep, Fset($\alpha$), Pair($\alpha,\beta$)\\ 
\> \constructors\\
\>\> meth\con \>: \> MethName\rep $\times$  Fset(Pair(VarName\rep, Type\rep))  $\times$ \\
\>\>\>\> Fset(Pair(VarName\rep, Type\rep)) $\times$  Command\rep $\rightarrow$  Meth\rep\\
\>\selectors\\
xx \= xx \= xxxxxxxxxxx \= x  \= xx \= xx\= \kill
\>\> methName\sel \>:\> Meth\rep $\,\rightarrow$ MethName\rep\\
\>\> input\sel \>:\> Meth\rep $\rightarrow$ Fset(Pair(VarName\rep,Type\rep))\\
\>\> output\sel \>:\> Meth\rep $\rightarrow$ Fset(Pair(VarName\rep,Type\rep))\\
\>\> command\sel \>:\> Meth\rep $\rightarrow$ Command\rep\\
\>\eend
\end{tabbing}}
\noindent
Finally, the representation of commands is inductively defined by:
{\sl \begin{tabbing}
xx \= xx \= xxxxxxx \= x  \= xx \= xx\= \kill
Command\rep ==\\
\hspace{0.4 cm}
\> \basedOn \\
\>\>MethName\rep, VarName\rep,
 List($\alpha$), Pair($\alpha,\beta$), Expr\rep,Pred\rep\\ 
\> \constructors\\
\>\> skip\con \>:\>  $\rightarrow$ Command\rep\\
\>\> call\con \>:\>  MethName\rep  $\times$  List(VarName\rep)
 $\times$  List(VarName\rep) $\rightarrow$ Command\rep\\
\>\> assign\con \>:\> VarName\rep$\times$ Expr\rep $\rightarrow$ Command\rep\\
\>\> seq\con \>:\>  List(command\rep) $\rightarrow$ Command\rep\\
\>\> if\con \>:\>  Pred\rep  $\times$  Command\rep $\times$  Command\rep $\rightarrow$ Command\rep\\
\>\> while\con \>:\> Pred\rep $\times$ Command\rep $\rightarrow$ Command\rep\\

\>\> any\con \>:\> VarName\rep $\times$ Type\rep $\times$ Pred\rep $\times$  Command\rep $\rightarrow$ Command\rep\\
xx \= xx \= xxxxxxxxxx \=x \= xx \= xx\= \kill
\> \selectors $\ldots$\\
\> \axioms $\ldots$ \\
\>\eend
\end{tabbing}}
\noindent
Predicates will have the constructors {\sl true\con, false\con, forall\con, exist\con, not\con, implies\con, eq\con, isIn\con $\ldots$}. We omit  the details.







 

\subsection{Generators for Generic Update Operations}



The generator to be presented produces abstract syntax for {\em insert} operations, i.e. it is defined in terms of {\sl meth\con}. The case of {\em update} and {\em delete} can be handled analogously. Its task is the generation of the appropriate actual parameters for {\sl meth\con} from class and schema representations. The parameters are the operation's name, a list of input parameters, a list of output parameters and a representation of a command forming the body of the insert operation. Omitting other details we   concentrate on parts of the body   managing inclusion constraints, dealing with  references in the acyclic and cyclic case and changing the class extent. For each subtask we will briefly discuss the code  to be produced followed by a discription of the algorithm to produce the actual parameters forming this  code and then present the generator definition together with  its (raised) output. 

\subsubsection{Managing Inclusion Constraints}

In the case of {\sl IsA}-relationships we have to generate calls of insert operations on each of the direct superclasses while providing  appropriate input values for these operations.

Since  class representations capture  {\sl IsA}-information through a set of class names we can produce the insert calls by applying a general {\sl set-reduce} function as defined in \cite{base}. It will return a list of calls which, serving as parameter for a sequence constructor, will lead to a sequence of commands. Roughly speaking {\sl set-reduce} applies a function to each element of a set and accomodates the results by the application of another function.

For generating a call we need the method's name together with a list of input and output variables. Of further interest is the input value.
In parallel to the generation of  insert operations we have to generate functions on the  value types involved. For sake of simplicity we  assume that {\sl IsA}-relationship between classes {\sl C$_1$} and {\sl C$_2$} ({\sl C$_1$ IsA C$_2$}) includes  subtype relationships on their structure types ({\sl T\_C$_1$ subtypeOf T\_C$_2$)}. This is not required in general. {\sl IsA}-relation on classes means inclusion relation on their corresponding sets of oids. If we had no subtype relationship on the value-types we would have to produce a different input type  for a subclass including all values necessary in superclasses. This is easy compared to the case of an existing subtype relation. In Lemma \ref{lemma29} it has been shown that in the case of subtype relationship a subtype function between the value types of sub- and superclasses exists. Thus, a generator for these functions exists.  At this point we omit the definition.  We merely make use of the name of the generated function which we built by  the concatenation instead of applying a name selector to the generator's output. The function taking {\sl V\_C} to {\sl V\_D$_i$} is called {\sl h\_C,D$_i$}. 

Again for simplicity we make the further assumption for the  case of more than one distinct  superclasses. We assume the existence of a common superclass of these superclasses. Otherwise we would run into problems of renaming or having synonyms of identifiers. A technical solution for this problem is indicated in \cite{subieta}. 

{\sl Insert\gen} has input values {\sl C} of type {\sl Class\rep} and {\sl S} of type {\sl Schema\rep}. The insert operation being produced uses variable name {\sl 'v'} for its input value.
{\sl \begin{tabbing}
xx \= xx \= xx \= xx\= xx\= xx\= xx\=\kill
\> seq\con(
\>\> setReduce(\\
\>\>\> isA\sel(C),\\
\>\>\>lambda D.\\
\>\>\>\> call\con(concat('insert\_',D),\\
\>\>\>\>\> singleList(apply\con(concat('h\_', concat(className\rep(C),D)),'v'))\\ 
\>\>\>\>\>singleList(concat('i\_',D))),\\
\>\>\> append,\\ 
\>\>\> nil))\\
\end{tabbing}}
\noindent
If we apply {\sl raise} to the produced output code for superclasses {\sl D$_1$, $\ldots$ D$_n$} the result will be:
{\sl \begin{tabbing}
xx \= xx \= xxxx \= xx\= xx\= xx\= xx\= xx\= xx \= \kill
\>\> i\_${D_1}$ $\leftarrow$ insert\_D$_1$(h\_C,D$_1$(v)); \\
\>\> $\ldots$;\\
\>\> i\_${D_n}$ $\leftarrow$ insert\_D$_n$(h\_C,D$_n$(v)); \\
\end{tabbing}}


\subsubsection{Enforcing Referential Constraints in the Acyclic Case}\label{acyclic}

In this section we handle  classes with an acyclic reference structure. In this case  the insert operation includes calls  with appropriate input values for each class being referred to. The operation has somehow to gather the returned identifiers for producing a value of type {\sl T\_C} which forms a prerequisite for adding the new object to the class extent.

In order to produce the sequence of insert calls for referenced objects we  proceed  in the same way as shown above. We apply {\sl list-reduce} to  the list of references which has to be selected from the structure representation of the class. {\sl list-reduce} is defined analogously to {\sl set-reduce}.

Again we have to provide  input values for which we  assume generated functions doing the job \cite{icdt}. For each reference {\sl r$_i$} to a class {\sl C$_i$} we  have a function {\sl val\_r$_i$} taking an input value of type {\sl V\_C} to the set of all those values of type {\sl V\_C$_i$} that occur at the corresponding place in {\sl v}. These values correspond to existing or new objects in {\sl C$_i$} to which  the future object in {\sl C} will refer to via {\sl r$_i$}.  As we explained above the value type of a class includes for each reference the value type of the class referenced to. Since references can occur in deeply nested type constructors (e.g. we can have lists of sets of referred objects) they are in general multivalued. This requires the call of a  method {\sl insertObjects\_C$_i$} before the final insert. The method {\sl insertObjects\_C$_i$} receives a set of input values for {\sl C$_i$} and returns sets of identifier/input-value pairs. Its definition is given below.

The calling insert operation gathers these sets of identifier-value pairs in a list {\sl l}.\footnote{At this place a list structure is needed which corresponds to the order in which the references are given in the reference list. Referenced classes might have the same structure so that a value alone would not suffice to indicate to which class the object with a value belongs to.} It should be indicated that in the case of  references to {\sl C$_1$, $\ldots$ C$_n$} the list {\sl l} has type {\sl List(Set(Pair(Id, Union(V\_C$_1$, $\ldots$ V\_C$_n$))))} where {\sl Union} means a variadic union type constructor. Since we neglect the representation type for types  we    introduce a function {\sl makeTypeRep}  taking a  type definition and turning it into its representation. 

{\sl \begin{tabbing}
xx \= xx \= xx \= xx\= xx\= xx\= xx\=\kill
\>any\con(\\
\>\>'l',makeTypeRep(List(Set(Pair(Id,Union(V\_C$_1$,$\ldots$V\_C$_n$))))),\\
\>\> eq\con('l','nil'),\\
\>\> seq\con(listReduce(\\
\>\>\> references\sel(structure\sel(C)),\\
\>\>\> lambda D.cons\\
\>\>\>\> (call\con(concat('insertObjects\_',second(D)),\\
\>\>\>\>\> apply\con(concat('val\_', first(D)),v), 'j'),\\ 
\>\>\>\>singleList(assign\con ('l', 'append(Pair(j,l))'))),\\
\>\>\> append,\\ 
\>\>\> nil)))
\end{tabbing}}
\noindent
The generator will produce the following code for references to classes {\sl C$_1$} to {\sl C$_n$}.
{\sl \begin{tabbing}
xx \= xx \= xxxx \= xx\= xx\= xx\= xx\= xx\= xx \= \kill
\>  l : List(Set(Pair(Id,Union(V\_C$_1$,..,V\_C$_n$)))) $\mid$ l = nil $\longrightarrow$\\
\>(j $\leftarrow$ insertObjects\_C$_1$(val\_$r_1$(v)); l := append(Pair(j,l));\\
\> $\;$...;\\
\> $\;$j $\leftarrow$ insertObjects\_C$_n$(val\_$r_n$(v)); l := append(Pair(j,l)));
\end{tabbing}}
\noindent
The called methods {\sl insertObjects\_C$_i$} have the following form:
{\sl \begin{tabbing}
xx \= xx \= xx \= xx\= xx\= xx\= xx\= xx\= xx \= \kill
\> k $\leftarrow$ insertObjects\_C$_i$ (vs : Set(V\_$C_i$))  = \\
\>\> s:Set(Pair(Id,V\_$C_i$) $\mid$ s = empty $\longrightarrow$\\
\>\> (j:Nat $\mid$ j = 1 $\longrightarrow$\\
\>\> (do vs $\neq$ empty\\
\>\>\> v : V\_$C_i$ $\mid$ v $\in$ vs  $\longrightarrow$\\
\>\>\> (id$_{r_i,j}$ $\leftarrow$ insert\_C$_i$(v);\\
\>\>\> s := insert(Pair(id$_{r_i,j}$,v),s);\\
\>\>\> vs := vs - \{v\};\\
\>\>\> j := j+1);\\
\>\> od);\\
\>\> k := s)
\end{tabbing}}

Clearly, there also exists a generator for {\sl insertObjects\_C$_i$}, but for the sake of brevity we omit its description here.
\subsubsection{Changing the Class Extent}
This part deals with adding the new object to the class' extent. According to our data modelling approach we have to insert a pair consisting of an identifier and a value of type {\sl T\_C}. This requires a function {\sl f\_C} on {\sl V\_C} producing a value of type {\sl T\_C}. It is applied to the input value of the insert operation together with the provided list {\sl l} of sets of identifier-/values-pairs  and substitutes ``reference-wise'' values of type {\sl V\_C$_i$} by their related identifiers as provided in list {\sl l}. Generator code and raised generated code are the following:
{\sl \begin{tabbing}
xx \= xx \= xx \= xx\= xx\= xx\= xx\= xx\= xx \= \kill
\>assign\con(name\sel(C), unionExpr\rep(name\sel(C),\\
\>\> singleSet(concat('Pair', concat('i',apply(concat('f\_',name\sel(C)),'Pair(v,l)')))))
\end{tabbing}}

{\sl \begin{tabbing}
xx \= xx \= xx \= xx\= xx\= xx\= xx\= xx\= xx \= \kill
\>C := C $\cup$ \{Pair(i,f\_C(Pair(v,l)))\}
 \end{tabbing}}

\subsubsection{Dealing with Cyclic Reference Structures}
Now we extend our generator to the case of a  cyclic reference structure. In this case the value type {\sl V\_C} will be recursively defined. In general, even mutual recursive definitions are required \cite{icdt}.  Recursive types have to be defined in such a way that all their values are finitely representable, i.e. representable as rational trees. The finiteness of the database which imposes the finiteness of cycles fits perfectly with rational trees as input values.

Let us consider the insert call arising by a cycle on class {\sl C}. To simplify the explanation, we concentrate on single-valued and direct cyclic references first. In this case {\sl val\_r$_c$(v)} is unary, say {\sl \{v$\,^{\prime}$\}}, where {\sl v$\,^{\prime}$} is of type {\sl V\_C}. We need a function {\sl occurs}  defined on two values of type {\sl V\_C}. It checks  the input value whether {\sl v} occurs in {\sl v$\,^{\prime}$} which is true iff the object corresponding to {\sl v$\,^{\prime}$}  refers to the object corresponding to {\sl v}, i.e. the cycle  on class {\sl C} is closed just at this input object. Furthermore, this means that the calls of insertions on {\sl C} will stop with the second occurrence of the rational tree {\sl v} in {\sl v}. It requires the already created identifier to be available on the later applied insert operation. It also serves as indication that the cycle has to be closed at this point and no further insert call on {\sl C} need to follow. This passing on of the identifier is simply managed by substituting the identifier for {\sl v} in {\sl v$\,^{\prime}$} and calling the next inserts on {\sl C} for reducing the cycle with the substituted value. This requires to change {\sl V\_C} by substituting {\sl Union(V\_C,Id)} for {\sl V\_C} in the defining expression of {\sl V\_C}. Let the resulting type be denoted $\overline{\mbox{\sl V\_C}}$.
Here {\sl Union($\alpha,\beta$)} denotes a simple union type.
Consider, that  function {\sl val\_r$_i$} provides only values of type {\sl V\_C}, hence without identifiers. Therefore, if an identifier was substituted in the case of a cycle no  input value will be provided for a further input call and, moreover, the identifier is already part of the value to be inserted.

General cycles are handled analogously. The function {\sl occurs} in this case has to check if v occurs in some value {\sl v$\,^{\prime}$} in the set {\sl val\_r$_c$(v)}. 


However, since substitution of {\sl i} for {\sl v} in {\sl v$\,^{\prime}$} does not change {\sl v$\,^{\prime}$} if {\sl occurs(v,v$\,^{\prime}$) = false}, we only have to replace the parameter {\sl val\_C$_i$} (in the acyclic case) by {\sl substitute(val\_C$_i$(v),(v,i))}. Hence all insert operations may take values of the extended type $\overline{\mbox{\sl V\_C}}$ as input which includes {\sl V\_C}.

\chapter{Integrity Enforcement} \label{enforcement}

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.

Let us now address the integrity enforcement problem with respect to static and transition constraints. In general, verification techniques based on predicate transformers are applicable \cite{iwsds} but 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{static-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. 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.

\section{Enforcing Static Integrity} \label{static-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} {\rm \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) -- (iv) (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} {\rm 

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} {\rm 

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} {\rm 

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} {\rm 

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} {\rm 

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} {\rm \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} {\rm 

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{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 in Lemma \ref{lemma29}.

\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-represen\-ta\-tion 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} {\rm 

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} {\rm 

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} {\rm 

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} {\rm 

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} {\rm 

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} {\rm 

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} {\rm 

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} {\rm \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} {\rm 

\ 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} {\rm \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 $loop$, 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} {\rm \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} {\rm 

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} {\rm 

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} {\rm 

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} {\rm 

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} {\rm 

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} {\rm 

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

} \end{proof}

\noindent
An unsolved 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. 

\chapter{Conclusion} \label{schluss}

In this report we describe results from first investigations in Hamburg and Rostock concerning the formal foundations of object oriented database concepts. For this purpose we introduced a formal object oriented datamodel (OODM) with the following characteristics.

\begin{itemize}

\item Objects are considered to be abstractions of real world entities, hence they have an immutable identity. This identity is encoded by abstract identifiers that are assumed to form some type $ID$. This identifier concept eases the modelling of shared data and cyclic references, however, it does not relieve us from the problem to provide unique identification mechanisms for objects in a database.

\item In our approach there is not only one value of a given type that is associated with an object. In contrast we allow several values of possibly different types to belong to an object, and even this collection of types may change.

\item Types are used to structure values. In our approach general algebraic type specifications are allowed including parameterization, subtyping and mutual recursion.

\item Classes are used to structure objects. At each time a class corresponds to a collection of objects with values of the same type and references to objects in a fixed set of classes. Inheritance is based on IsA relations that express an inclusion at each time of the sets of objects. Moreover, referential integrity is supported.

\item We associate with each class a collection of methods. Methods
are specified by guarded commands, hence the method language is computationally
complete. In order to allow the handling of identifiers that are always hidden
from the user as well as user-accessible transactions a hiding operator on
methods is introduced. Generic update operations, i.e. insert, delete and
update on a class are assumed to be automatically derived whenever this is
possible.

\item We associate static and transition constraints to classes and also to a schema. Certain kinds of such constraints can be obtained by generalizing corresponding constraints in the relational model.

\end{itemize}

\noindent
On this basis of this formal OODM we study the problems of identification, genericity and integrity.

We show that the unique identification of objects in a class requires the class to be value-representable. Assuming that only uniqueness constraints are defined we can show that value-representability is decidable.

An advantage of database systems is to provide generic update operations. We show that the unique existence of such generic operations on some class requires also value-representabi\-li\-ty. However, in this case referential and IsA integrity can be enforced automatically. From an engineering point of view an algorithm is required to generate these consistent operations. We address this construction problem by the specification of generators for them. These generators will be based on the possibility to represent syntactic components of the language as values within the language itself, which is known to form the basis of {\em linguistic reflection}\/. Moreover, the generators involve a single generic proof of correctness hence relieve the user of the burden to write basic update operations and to assure their consistency.

The existence result can be generalized with respect to distinguished classes of explicitly stated static constraints. We 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. 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.

This report is far from giving a complete mathematical foundation of OODB concepts. A lot of problems are still left open and are the matter of current investigations or future research.

\begin{itemize}

\item OODBs have been claimed to support engineering applications without proving this. We believe that our approach to types will allow really complex objects to be defined and that the general notion of object will ease the support of versions. In order to support multiple objects in a class the parameterization seems to be a good idea. We shall work on this idea.

\item In our approach classes are sets. What are other bulk types? Does it make
sense to abstract from classes in this way?

\item In this report we left aside much of the formal semantics which is based on the specification language SAMT. However, there also exist some open problems with this, e.g. a more general approach to transactions without assuming linear order of execution and traces on classes.

\item The problem of updatable views is still open. We work on it.

\item Our approach to genericity only handles the worst case expressed by the
value representation type. We assume that polymorphism will help to generalize
our results to the general case. Moreover, we must integrate communication
aspects at least with respect to the user.

\item So far, we have shown an existence result for greatest consistent specializations that are used to achieve integrity enforcement. We do not know how to find such a GCS in the general case. 

\item The axiomatic semantics used for guarded commands abstracts from an execution model. All results are true for semantic equivalence classes. However, we also need optimization, especially with respect to the derived GCSs.

\item We only presented a formal OODM without looking into methodological aspects such as the characterization of good designs or stepwise refinement approaches.

\end{itemize}

\noindent
We express the hope that others will also contribute to solve outstanding problems in OODB foundation or in the implementation of more sophisticated object oriented database languages on a sound mathematical basis.

\begin{thebibliography}{12} 

\addcontentsline{toc}{chapter}{Bibliography}

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

\bibitem{ifo} S.~Abiteboul, R.~Hull: {\it IFO: A Formal Semantic Database Model}, ACM ToDS, vol. 12 (4), December 1987, pp. 525 -- 565

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

\bibitem{life} H.~A\"{\i}t-Kaci: {\it An Overview of LIFE}, in  J.~W.~Schmidt, A.~A.~Stognij (Eds.): Proc. Next Generation Information 
Systems Technology , Springer LNCS, vol. 504, 1991, pp. 42 -- 58

\bibitem{galileo} A.~Albano, G.~Ghelli, R.~Orsini: 
{\it Types for Databases: The Galileo Experience}, in Type Systems and 
Database Programming Languages, University of St. Andrews, Dept. of Mathematical and Computational Sciences, 
Research Report CS/90/3, 27 -- 37

\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{albano1} A.~Albano, G.~Ghelli, R.~Orsini: {\it Objects and Classes for a Database Programming Language}, FIDE technical report 91/16, 1991

\bibitem{albano} A.~Albano, G.~Ghelli, R.~Orsini: {\it A Relationship Mechanism for a Strongly Typed Object-Oriented Database Programming Language}, in A.~Sernadas (Ed.): {\it Proc. VLDB 91}, Barcelona 1991

\bibitem{oo-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{o2} F.~Bancilhon, G.~Barbedette, V.~Benzaken, C.~Delobel, S.~Gamerman, C.~L{\'e}cluse, P.~Pfeffer, P.~Richard, F.~Velez: {\it The Design and Implementation of O$_2$, an Object-Oriented Database System}, Proc. of the ooDBS II workshop, Bad M{\"u}nster, FRG, September 1988

\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{beeripods} C.~Beeri: {\it New Data Models and Languages - the Challange} in Proc. PODS '92

\bibitem{cardelli} L.~Cardelli, P.~Wegner: {\it On Understanding Types, Data Abstraction and Polymorphism}, ACM Computing Suerveys 17,4, pp 471 -- 522

\bibitem{quest} L.~Cardelli: {\it Typeful Programming}, Digital Systems Research Center Reports 45, DEC 
SRC Palo Alto, May 1989

\bibitem{exodus} M.~Carey, D.~DeWitt, S.~Vandenberg: {\it A Data Model and Query Language for EXODUS}, Proc. ACM SIGMOD 88

\bibitem{vision} M.~Caruso, E.~Sciore: {\it The VISION Object-Oriented Database Management System}, Proc. of the Workshop on Database Programming Languages, Roscoff, France, September 1987

\bibitem{napier} A.~Dearle, R.~Connor, F.~Brown, R.~Morrison: {\it Napier88 - A Database Programming Language?},  in Type Systems and 
Database Programming Languages, University of St. Andrews, Dept. of Mathematical and Computational Sciences, 
Research Report CS/90/3, 10 -- 26

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

\bibitem{ehrich1} 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{adabtpl} L.~Fegaras, T.~Sheard, D.~Stemple: 
{\it The ADABTPL Type System}, in Type Systems and 
Database Programming Languages, University of St. Andrews, Dept. of Mathematical and Computational Sciences, 
Research Report CS/90/3,  45 --  56

\bibitem{traversal} L.~Fegaras, T.~Sheard, D.~Stemple: 
{\it Uniform Traversal Combinators: Definition, Use and Properties}, University of Massachusetts, 1992

\bibitem{iris} D.~Fishman, D.~Beech, H.~Cate, E.~Chow et al.: {\it IRIS: An Object-Oriented Database Management System}, ACM ToIS, vol. 5(1), January 1987

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

\bibitem{gottlob} G.~Gottlob, G.~Kappel, M.~Schrefl: {\it Semantics of Object-Oriented Data Models -- The 
Evolving Algebra Approach}, in J.~W.~Schmidt, A.~A.~Stognij (Eds.): Proc. Next Generation
Information  Systems Technology, Springer LNCS, vol. 504, 1991

\bibitem{sdm} M.~Hammer, D.~McLeod: {\it Database Description with SDM: A Semantic Database Model}, J. ACM, vol. 31 (3), 1984, pp. 351 -- 386

\bibitem{heuer} A.~Heuer, P.~Sander: {\it Classifying Object-Oriented 
Results in a Class/Type Lattice}, in B.~Thalheim et al. (Ed.): {\it 
Proceedings MFDBS 91}, Springer LNCS 495, pp. 14 -- 28

\bibitem{hull-king}
R.~Hull, R.~King: {\it Semantic Database Modeling: Survey, Applications and Research Issues}, ACM Computing Surveys, vol. 19(3), September 1987

\bibitem{ilog} R.~Hull, M.~Yoshikawa: {\it ILOG: Declarative Creation and Manipulation of Object Identifiers}, in Proc. 16th VLDB, Brisbane (Australia), 1990, pp. 455 -- 467

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

\bibitem{kifer} M.~Kifer, J.~Wu: {\it A Logic for Object-Oriented Logic Programming (Maier's O-Logic Revisited)}, in PODS'89, pp. 379 -- 393

\bibitem{orion} W.~Kim, N.~Ballou, J.~Banerjee, H.~T.~Chou, J.~Garza, D.~Woelk: {\it Integrating an Object-Oriented Programming System with a Database System}, in Proc. OOPSLA 1988

\bibitem{lockemann} P.~Lockemann, J.~W.~Schmidt: {\it Datenbankhandbuch}, Springer, 1987

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

\bibitem{gemstone} D.~Maier, J.~Stein, A.~Ottis, A.~Purdy: {\it Development of an Object-Oriented DBMS}, OOPSLA, September 1986

\bibitem{dbpl} F.~Matthes, J.~W.~Schmidt: 
{\it The Type System of DBPL}, in Type Systems and 
Database Programming Languages, University of St. Andrews, Dept. of Mathematical and Computational Sciences, 
Research Report CS/90/3,  38 -- 44

\bibitem{florian} F.~Matthes, J.~W.~Schmidt: {Bulk Types -- Add-On or Built-In?}, in Proc. DBPL III, Nafplion 1991

\bibitem{taxis}  J.~Mylopoulos, P.~A.~Bernstein, H.~K.~T.~Wong: {\it A Language Facility for Designing Interactive Database-Intensive Applications}, ACM ToDS, vol. 5 (2), April 1980, pp. 185 -- 207

\bibitem{telos} J.~Mylopoulos, A.~Borgida, M.~Jarke, M.~Koubarakis: {\it Telos: Representing Knowledge About Information Systems}, ACM ToIS, vol. 8 (4), October 1990 pp. 325 -- 362

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

\bibitem{ohori} A. Ohori: {\it Representing Object Identity in a Pure Functional Language}, Proc. ICDT 90, Springer LNCS, pp. 41 -- 55

\bibitem{saake} G. Saake, R. Jungclaus: {\it Specification of Database Applications in the TROLL Language}, in 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 (an extended version appeared as FIDE technical report 1991/30, October 1991)

\bibitem{vdm}
K.-D.~Schewe, J.~W.~Schmidt, I.~Wetzel: {\it Specification and Refinement in 
an Integrated Database Application Environment}, Proc. VDM 91, 
Noordwijkerhout, October 1991

\bibitem{rostock}
K.-D.~Schewe, B.~Thalheim, I.~Wetzel, J.~W.~Schmidt: {\it Extensible Safe Object-Oriented Design of Database Applications}, University of Rostock, Preprint 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, pp. 341 -- 356

\bibitem{volkse} K.-D.~Schewe, B.~Thalheim, J.~W.~Schmidt, I.~Wetzel: {\it
Integrity Enforcement in Object-Oriented Databases}, in U.~Lipeck (Ed.): Proc.
4th Int. Workshop on Foundations of Models and Languages for Data and Objects
``MODELLING DATABASE DYNAMICS'', Volkse (Germany), October 19-22, 1992

\bibitem{generator} K.-D.~Schewe, J.~W.~Schmidt, D.~Stemple, B.~Thalheim, I.~Wetzel: {\it Generating Methods to Assure Global Integrity}, submitted 1992

\bibitem{rib} K.-D.~Schewe, J.~W.~Schmidt, D.~Stemple, B.~Thalheim, I.~Wetzel: {\it A Reflective Approach to Method Generation in Object Oriented Databases}, University of Rostock, Rostocker Informatik Berichte, no. 13, 1992

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

\bibitem{adc} K.-D.~Schewe, B.~Thalheim, I.~Wetzel: {\it Integrity
Preserving Updates in Object Oriented Databases}, in M.~Orlowska (Ed.) : Proc.
Australian Database Conference, Brisbane, February 1993 (to appear)

\bibitem{schekscholl} M. H. Scholl, H.-J. Schek: {\it A Relational Object Model}, in Proc. ICDT 90, Springer LNCS, pp. 89 -- 105

\bibitem{shaw} G. M. Shaw, S. B. Zdonik: {\it An Object-Oriented Query-Algebra}, IEEE Data Engineering, vol. 12 (3), 1989, pp. 29 -- 36

\bibitem{base} D.~Stemple, T.~Sheard: {\it A Recursive Base for Database Programming Primitives}, in Proceedings of the First International East/West Database Workshop, Kiev, October 1990

\bibitem{limits} D.~Stemple, T.~Sheard: 
{\it Exceeding the Limits of Polymorphism}, in Proc. EDBT '90

\bibitem{reflection} D.~Stemple, T.~Sheard, L.~Fegaras: 
{\it Reflection: A Bridge from Programming to Database Languages}, in Proc. HICSS '92

\bibitem{sam} S. Y. W. Su: {\it SAM$^*$: A Semantic Association Model for Corporate and Scientific-Statistical Databases}, Inf. Sci., vol. 29, 1983, pp. 151 -- 199

\bibitem{subieta} K.~Subieta: {\it A Persistent Object Store for the LOQIS Programming System}, to appear in: International Journal of Microcomputer Applications

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

\bibitem{herm} B.~Thalheim: {\it The Higher-Order Entity-Relationship
Model}, in J.~W.~Schmidt, A.~A.~Stognij (Eds.): Proc. Next Generation
Information  Systems Technology, Springer LNCS, vol. 504, 1991

\end{thebibliography}

\end{document}
