\documentstyle[a4,11pt]{article}

\renewcommand{\labelenumi}{(\roman{enumi})}
\newtheorem{defn}{Definition} 
\newtheorem{thm}{Theorem}
\newtheorem{prop}{Proposition} 
\newtheorem{cor}{Corollary}
\newtheorem{lem}{Lemma} 
\newtheorem{exam}{Example}
\newtheorem{definition}[defn]{Definition}
\newtheorem{algorithm}{Algorithm}

\renewcommand{\thealgorithm}{\Alph{algorithm}}

\title{{\LARGE\bf Extensible Safe Object-Oriented Design of Database Applications}$^*$\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{Klaus--Dieter Schewe, Bernhard Thalheim$^+$\\
Ingrid Wetzel, Joachim W. Schmidt}

\date{\footnotesize Hamburg University, Dept. of Computer Science,\\Schl\"uterstr. 70, D-W-2000 Hamburg 13\\schewe@dbis1.informatik.uni-hamburg.de\\ \ \\
$^+$Rostock University, Dept. of Computer Science,\\A.-Einstein-Str. 21, D-O-2500 Rostock\\thalheim@informatik.uni-rostock.dbp.de\\ \ \\ \today}

\begin{document}

\maketitle

\begin{abstract}

\noindent
The formal foundation of object-oriented databases is still an open problem. 
In this paper a formalization of kernel object-oriented design concepts is achieved by an automatizable transformation into a specification language with a clear mathematical semantics. This approach allows object-oriented design to be {\em extensible}.

The preservation of advantages of relational databases requires the definability of generic operations for the insertion, deletion and update of single objects. It is shown that such generic operations can only be defined for value-representable classes. The possibility to detect value-representability contributes to the {\em safety} for object-oriented design.
  
\end{abstract}

\section{Introduction}

The shortcomings of the relational database approach encouraged much research aimed at achieving more appropriate data models. There has been a tremendous interest in {\em semantic data models} which emphasize on natural mechanisms and constructs for the description of relationships between stored data. In the last decade several models such as SDM \cite{sdm}, TAXIS \cite{taxis}, SAM$^*$ \cite{sam} and IFO \cite{ifo} were proposed primarily as schema design tools. Their usefulness for this task as well as their fundamentals are widely accepted. Similar structuring mechanisms are used by {\em knowledge representation systems} such as KL-ONE \cite{klone}, BACK \cite{back}, TELOS \cite{telos} or CLASSIC \cite{classic} which put additional emphasis on inferences on such structures.

Recently, it has been claimed that the {\em object-oriented approach} to
be the key technology for future database systems and languages. Several
systems such as EXODUS \cite{exodus}, VISION \cite{vision}, IRIS \cite{iris}, Gemstone \cite{gemstone}, ORION
\cite{orion} and O$_2$ \cite{o2} arose from these efforts; current
research in databases often addresses object-orientation, e.g. \cite{albano1}.
However, in contrast to research in the relational area there is no common
formal agreement on what constitutes an object-oriented database \cite{beeri}.

In this paper we outline a safe and extensible way to design an object-oriented database while supporting general design concepts as described in \cite{oo-manifesto}. 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, the handling of such identifiers is itself a database problem \cite{lockemann}, since the user can only access those objects in the database that can be completely described by values. 

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,albano2,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 call such classes {\em value-representable}.
In our approach these classes are accompanied by a collection of generic operations that need not to be specified by the user. Furthermore, inclusion dependency and
referential integrity are enforced by these operations. This justifies the use of the notion ``safety''. 

We introduce a kernel high-level language featuring types and classes together
with separate hierarchies on both. Classes denote sets of objects, and objects
themselves are encoded via an object identifier and values of that object
belonging to a collection of types or referring to other objects.
Recently, the necessity of a separate mechanism for the handling of
relationships was identified \cite{albano2}. We
allow relationships between classes to be represented in the same manner as
classes with references to other classes, which allows in turn the modelling of
higher-order relationships \cite{herm}.

\begin{figure}
\setlength{\unitlength}{0.8cm}
\begin{center}
\begin{picture}(13,7.5)

\thicklines

\large
\put(0,7.0){\makebox(0,0)[l]{Extensibility}}
\put(0,3.5){\makebox(0,0)[l]{Safety}}
\put(0,0.75){\makebox(0,0)[l]{Reification}}
\put(8.75,7.0){\makebox(0,0){\shortstack{Kernel\\language}}}
\put(8.75,3.5){\makebox(0,0)[b]{SAMT}}
\put(6.5,0.75){\makebox(0,0)[r]{DB2}}
\put(8.0,0.75){\makebox(0,0){DBPL}}
\put(9.5,0.75){\makebox(0,0){O$_{2}$}}
\put(11,0.75){\makebox(0,0){$ \cdots $}}

\put(5.5,7.0){\makebox(0,0)[r]{$ \cdots $}}
\put(7,7.0){\makebox(0,0){$ \hookleftarrow $}}

\put(12,7.0){\makebox(0,0)[l]{$ \cdots $}}

\put(10.5,7.0){\makebox(0,0){$ \hookrightarrow $}}


\put(5.5,6){\vector(3,-2){2.25}} 
\put(12,6){\vector(-3,-2){2.25}}

\put(8.75,6){\vector(0,-1){1.5}}

\put(8,3){\vector(-1,-1){1.5}}
\put(8.5,3){\vector(-1,-3){0.5}}
\put(9,3){\vector(1,-3){0.5}}
\put(9.5,3){\vector(1,-1){1.5}}

\end{picture}
\end{center}
\normalsize
\caption{\label{modelling}
The general modeling approach}
\end{figure}

Representing this kernel language in the formal specification language SAMT \cite{iwsds} the formal foundation of SAMT, i.e., the combination of algebraic type specification and structured
substitution-based module specification, carries over to object-oriented design.
On the other
hand SAMT offers a formally based notion of refinement \cite{iwsds} which
enables the derivation of different implementations in different target
languages. 

Extensibility can be achieved in our approach since additional features of
high-level object-oriented design languages can also be defined by SAMT
representations.
Figure \ref{modelling} gives an overall
picture of our approach. 

In section \ref{features} we describe the
kernel components of object-oriented design and illustrate the formal
representation of the outlined high-level object-oriented design components together with the derived operations
in SAMT. In section \ref{safety} we discuss the problem of value-representability and its relation to the automatic derivation of generic operations. In section \ref{ext} we outline the capability of extending the kernel design language on the basis of SAMT.

\section{Formalization of Object-Oriented Conceptual Design}


\label{features}

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 classified 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{beeri}, objects have to be
encoded by object identifiers regardless of the content, location or
addressability \cite{KC 86}. In our approach each object consists of a unique,
immutable  {\it identifier}, a set of values of different types called the {\em value-types} of the object, {\em references}
to other objects and {\em operations(methods)} associated with the object. This is formally expressed by

\[  o \; \; \; = \; \; \; (i,\{v_j,T_j\},\{o_k\},\{op_l\})  \]

\noindent
for an object $o$ with identifier $i$, values $v_j$ of types $T_j$, references to objects $o_k$ and operations $op_l$.

The class concept provides the classification 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 a {\it type declaration} 
and a {\it class definition}. 

\subsection{Type Declarations}

The high-level type language provides STRING, NAT, INT as {\it basic types}
with the usual operations on them. {\it Enumerated} and {\it subrange} types
can also be defined as usual. 

Basically, only two type constructors, the {\it tagged tuple} constructor denoted
by ($\cdot$) and the {\it set} type constructor denoted by $\{ \cdot \}$, are
allowed. 

\begin{exam}
Both  type constructors are used in the declaration for PERSONNAME:
\end{exam} 

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

\begin{exam}
The definition for a type PERSON uses the type PERSONNAME and a type ADDRESS 
defined elsewhere:
\end{exam}

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

In SAMT a type is given by a triplet $T = (S,F,Ax)$, where $S$ 
denotes the structure of the type $T$, i.e. the generators of $T$ as a set, $F$
denotes the functions on $T$ including algebraic operations, and $Ax$ is a
collection of axioms on $S$ and $F$ \cite{iwsds}. 
This approach is similar to algebraic specifications.

SAMT types can be used for an easy representation of tuple types such as {\em PERSON\-NAME} and {\em PERSON}, the tags in which give the names of selector functions:

\begin{exam}[SAMT representation]

Suppose the data type STRING is defined elsewhere. Then the names of 
persons can be defined by the following type.

\end{exam}

\noindent
{\em PERSONNAME == \\
\indent {\tt BasedOn} STRING;\\
\indent {\tt Constructors} {\sf PName} : FirstName : STRING $\times$ LastName : STRING $\times$ \\
\hspace*{45pt} Titles : {\rm FSETS}(STRING) $\rightarrow$ PERSONNAME ;\\
{\tt End} PERSONNAME} \\

In this example we use the parameterized type FSETS($\alpha$) to represent the type constructor $\{ \cdot \}$ of our high level kernel language and to denote the type
of finite subsets for any type $\alpha$. A SAMT definition of FSETS is given in \cite{iwsds}. The representation of the type {\em PERSON} can be achieved analogously.

\subsection{Subtyping}

Types can be organized in a type hierarchy. The notion of subtype in SAMT is defined
by  the existence of a coercion function mapping the subtype to its supertype. In
the high-level kernel language subtyping on tuples uses canonical projection as the
coercion function. Subtyping of set types depends on the subtyping of the
member types \cite{albano1}. 

In addition, we use concatenation on tuple types denoted by the
$\circ$-operator.

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

{\sl\begin{tabbing}
xxxxx\=PERSONNAME a \= = a \= ( \= Faculty, \=  :, \= NAT, \=\kill
\>STUDENT \> = \>\>PERSON $\circ$ ( StudNo : NAT, Faculty : NAT )
\end{tabbing}}

\begin{exam}[SAMT representation]

The type {\em STUDENT} can be defined as a subtype of the type {\em PERSON}. In this example
we use a function ``student\_proj\_person'' taking the subtype STUDENT to the
supertype PERSON:

\end{exam}

\noindent
{\em STUDENT == \\
\indent {\tt SubtypeOf} PERSON Via student\_proj\_person ;\\
\indent {\tt BasedOn} NAT ; STRING ;\\
\indent {\tt Constructors}  {\sf Student} : PersonIdentityNo : NAT $\times$ Name : PERSONNAME $\times$\\ 
\hspace*{30pt} Address : ADDRESS $\times$ StudNo : NAT $\times$ FacultyNo : NAT $\rightarrow$ STUDENT ; \\ 
\indent {\tt Axioms} With S :: STUDENT : \\
\hspace*{30pt}
student\_proj\_person(S) = {\sf Person}(PersonIdentityNo(S),Name(S),Address(S)) ; \\ 
{\tt End} STUDENT }\\

In \cite{iwsds} we provided examples of more sophisticated subtypes in SAMT 
using non-trivial coercion functions.

\subsection{Class Definitions}

Objects are grouped into classes. Classes denote mutable sets of 
objects with values of the same type and the same set
of operations. 

\noindent
In addition to having values an object may refer to another object. For
instance,  a person may refer to his/her spouse if this person is married.
References can be modelled at the class level. Therefore, we extend the class
definition in accordance to the type definition. This means that instead of
giving a simple value-type expression for a class, we use a structure expression built analogously.
Not only the type names but also class names are allowed in such expressions. Class names occurring in structure expressions are interpreted as references. Tags preceding class names are interpreted as
reference names. The subscript $\bot$ can be used to indicate references that
are only partial.

\begin{exam}

\label{key-exs}
The class {\sc Persons} with an additional 
reference to the spouse of a person -- if it exists -- can be defined as follows:\\

{\rm {\sc Persons} = CLASS  {\em PERSON}  $\circ$ (Spouse : {\sc Persons}$_\bot$)}

\end{exam}

Classes can be represented by state variables of persistent SAMT modules \cite{iwsds}.
The types of these variables are defined as partial functions from a system-provided
unique identifier type {\em ID\_TYPE} either to some other value type, to the identifier type in
case of references, or to type expressions involving both these possibilities.

Value types
have been specified by the type declaration in the kernel language. References to other classes give rise
to additional constraints to be represented by static invariants. The domain of
the reference variable is included in the domain of the class variable in case
of partial references or otherwise even equal. The range of the reference is
included in the domain of the corresponding class.

\begin{exam}[SAMT representation]

The following part of a module {\sc PersonModule} represents the class 
{\sc Persons}:

\end{exam}

\noindent
VARIABLES {\sl Persons} :: PFUN({\em ID\_TYPE,PERSON})\\
\hspace*{40pt} {\sl Spouse} :: PFUN({\em ID\_TYPE,ID\_TYPE})\\
INVARIANT \\ 
\indent STATIC {\em With I :: ID\_TYPE :}\\
\hspace*{30pt} {\em member(I,domain({\sl Spouse})) = true \ $\Rightarrow$ \ member(I,domain({\sl Persons})) = true ;}\\

\subsection{IsA-Relationships}

Classes may overlap allowing objects belonging to several
classes to have values of different types.
Classes may include other classes which is expressed by an IsA-relationship.

\begin{exam}
The class {\sc Students} shows the use of an IsA-relationship:\\

{\rm {\sc Students} \ = \ CLASS \ {\em STUDENT} \ ISA \ {\sc Persons}}

\end{exam}

For the SAMT representation of subclasses we exploit submodules.
Suppose we are given two classes and an IsA-Relation between them. This means
that the objects in the subclass form a subset of the objects of the
superclass.  
Since we assume a uniform identifier type for all objects, this means to require an injection on the corresponding sets of identifiers.

The value type of a subclass need not be a subtype of the superclass' value 
type. However, if it is then an additional invariant appears. We must
guarantee that the value associated with an object in the subclass as a member
of the superclass via the subtyping function is identical to its value as a
member of the superclass via the identifier inclusion. This relates
IsA-relationships on classes with the subtype concept of SAMT.

\begin{exam}[SAMT representation]

For example, the class {\sc Students} will be represented by the following part of a persistent module {\sc StudentModule}:

\end{exam}

\noindent
INHERITS {\sc PersonModule}\\
VARIABLES  {\sl Students} :: {\rm PFUN({\em ID\_TYPE,STUDENT})} \\
INVARIANT \\ 
\indent STATIC \hspace*{20pt} With I :: ID\_TYPE : \\
\hspace*{30pt} member(I,domain({\sl Students})) = true $\; \Rightarrow$
member(I,domain({\sl Persons})) = true $\wedge$ \\
\hspace*{60pt} stud\_proj\_person({\sl Students}(I)) = {\sl Persons}(I) ; \\

\noindent
The representation of the classes {\sc Professors} and {\sc Supervisors} can be achieved analogously.


\subsection{Constraints}

If each object belonging to a class is identifiable by the value it is related 
to in that class we denote this
property by using the keyword UNIQUE in that class definition.

References can be used in the {\em UNIQUE}-construct using the reference
tag. This forces the object-identifier to depend not only on the object's
value, but also on its references to other objects.
Classes with references can be used for the
representation of relationships as shown in example \ref{supervisor}.

\begin{exam}
\label{supervisor}

A supervisor class is 
defined as a relationship between professors and sets of students with the time
interval of the supervisorship as attribute. Therefore we obtain the following
definition: 

\end{exam} 

\noindent
{\sc Supervisor } = CLASS ( {\em Prof : }{\sc Professors},  \\
\hspace*{80pt} Studs : \{ ( {\em Stud : }{\sc Students} ) $\circ$ 
{\em (From : DATE, Till : DATE ) \} ) } \\ 
 \hspace*{80pt} {\em UNIQUE({\rm Studs})}\\

Each UNIQUE constraint defines a substructure $U(exp)$ derived from the structure expression $exp$ used in the class definition. $U(exp)$ can be defined as follows:

\begin{itemize}

\item If none of the tags $t_i$ in some expression $exp$ occurs in the UNIQUE constraint, then we have $U(exp) = ()$, where $()$ denotes the empty tuple type.

\item If $t$ occurs in the UNIQUE constraint, then $ \; U (\, ( t : exp ) \, ) = exp \;$.

\item In all other cases we have $\; U ( ( t_1 : exp_1 , \ldots , t_n : exp_n ) ) = U( ( t_1 : exp_1 ) ) \circ \ldots \circ U ( ( t_n : exp_n ) )\;$, $\; U ( ( t : exp ) ) = ( t : U ( exp ) ) \;$ and $\; U ( \{ exp \} ) = \{ U ( exp ) \} \;$.

\end{itemize}

UNIQUE constraints require the partial function representing the class and its references in SAMT to be injective.

\begin{exam}[SAMT representation]

UNIQUE(Studs) on the class {\sc Supervisors} can be represented as follows:

\end{exam}

\noindent
INVARIANT \\ 
\indent STATIC  {\em With I,J :: ID\_TYPE : \\
\hspace*{30pt} member(I,domain({\sl Supervisors})) = true $\wedge$ 
member(J,domain({\sl Supervisors})) = true $\wedge$ \\
\hspace*{30pt} {\sl Studs}(I) = {\sl Studs}(J) $\; \Rightarrow \; $ I = J } ;\\

Additional semantics can be captured if we can define a key on the set of object 
values belonging to each class. This property is
denoted by VALUE-KEY followed by a sequence of value tags. If a class is unique
and has a value-key, then objects of this class can be identified by their
values of the value-keys.

\begin{exam}

\label{spouse}
Extend the class {\sc Persons} by additional constraints. 

\end{exam}

\noindent
{\sc Persons} = CLASS  {\em PERSON}  $\circ$ (Spouse : {\sc Persons}$_\bot$) \\ 
\hspace*{60pt} {\em UNIQUE(PERSON)} \ {\em VALUE-KEY(PersonIdentityNo)}

VALUE-KEY gives the usual formulation of key on the range of the partial function representing the class.

\begin{exam}[SAMT representation]

VALUE-KEY(PersonIdentityNo) on {\sc Persons} can be expressed in {\sc PersonModule} as follows:

\end{exam}

\noindent
INVARIANT \\ 
\indent STATIC {\em With P$_1$, P$_2$ :: PERSON : \\
\hspace*{30pt} member(P$_1$,range({\sl PersonClass})) = true $\wedge$ member(P$_2$,range({\sl PersonClass})) = true $\wedge$ \\
\hspace*{30pt} PersonIdentityNo(P$_1$) = PersonIdentityNo(P$_2$) $\Rightarrow$
P$_1$ = P$_2$ }; \\


\section{Safety}

\label{safety}

In the tradition of value-based database programming {\em generic
operations} for insertion,  deletion, update and querying have been provided. The benefits of object identification in the object-oriented approach should not
force us to go beyond this capability. Hence the need to provide operations for creating, deleting, updating and querying objects. Queries are per se set-oriented, hence their generalization to object-oriented databases does not cause problems with object identifiers \cite{abiteboul,bk}. Therefore, we concentrate on the other operations. We show that generic operations can only be defined unambigously on classes the objects in which can be uniquely identified by values. Subsequently, we call this property value-representability.

\subsection{Value Representability}

In our approach objects are encoded in the database by their immutable identifiers. 
The concept of object identifiers has the advantage that these can be provided by the system and hidden to the user.
However, problems arise if we allow different objects to share the
same values and references. 

In this case some objects may not be completely updateable and accessible, e.g., if the different objects $o_1$ and $o_2$ with different identifiers $i_1$ and $i_2$ share the same values and references, it is not a priori decidable what is meant by a delete- or update-operation. Shall we delete (update) both objects, none of them or arbitrarily select one of them for deletion (update)? The same applies to insert-operations. If we want to insert an object $o$ with given values and references to existing objects and there exists already an object with the same values and references, shall we introduce another copy and create a new identifier, or reject the insert? Moreover, how shall we detect the objects referred to, if the user provides only values?

\begin{exam}
We can define a class of books the objects in which are not distinguishable by
their values. 
\end{exam}

\noindent
{\sc Books} = CLASS {\em Book : (Author: STRING , Title : STRING , Price : NAT)}\\  
\hspace*{90pt} $\circ$ (Owner : {\sc Persons})\\
   
Objects of the class {\sc Books} can not be uniquely identified. In this case, however, the problem can be resolved if we add the constraint {\em UNIQUE(Book,Owner)}. 

\begin{figure}
\setlength{\unitlength}{0.9cm}
\begin{center}
\begin{picture}(11,4.5)
\thicklines
\put(4.0,4.5){\makebox(0,0)[b]{database}}
\put(0.5,3.0){\makebox(0,0)[b]{value-oriented database}}
\put(7.5,3.0){\makebox(0,0)[b]{object-oriented database}}
\put(3.5,1.5){\makebox(0,0)[b]{value-representable database}}
\put(11.5,1.5){\makebox(0,0)[b]{identifier-based database}}
\put(0.5,0.0){\makebox(0,0)[b]{value-based database}}
\put(6.5,0.0){\makebox(0,0)[b]{non-value-based database}}

\put(4.0,4.4){\line(-3,-1){3.0}}
\put(4.0,4.4){\line(3,-1){3.0}}
\put(7.5,2.9){\line(-3,-1){3.0}}
\put(7.5,2.9){\line(3,-1){3.0}}
\put(3.5,1.4){\line(-3,-1){3.0}}
\put(3.5,1.4){\line(3,-1){3.0}}
                
\end{picture}
\end{center}
\normalsize
\caption{\label{classification}
Classification of databases}
\end{figure}

Several solutions are possible:

\begin{itemize}

\item Abandon generic operations as in \cite{saake},

\item use surrogate-keys to represent object identity as in \cite{albano1,albano2,o2} or

\item characterize those classes which can be represented by values.

\end{itemize}

We follow the third approach. Generally, we distinguish between {\em object-oriented} and {\em value-oriented} databases depending on whether they embody the concept of object identifiers or not. Among object-oriented databases we can distinguish
\cite{AlFedaghi} three different kinds:

\begin{description}

\item[Value-based databases]
All objects are {\em value-identifiable}, i.e. can be identified by values of their value types.

\item[Value-representable databases] 
All objects are {\em reference-identifiable}, where reference-iden\-ti\-fiabi\-li\-ty can be recursively defined as follows:

\begin{itemize}

\item
Each value-identifiable object is also reference-identifiable.

\item
If an object is identified by values of its value-type and references to a set of objects such that each object in this set is reference-identifiable, then the object is itself reference-identifiable.

\end{itemize}

\item[Identifier-based databases]
There are objects which are not reference-identifiable.

\end{description}

\noindent
Figure \ref{classification} illustrates these different classes of databases. 

Now we show how value-representability can be detected for {\em simple schemas} defined in the kernel language.
A {\em simple schema} is a collection of class definitions $\;  C_{1},...,C_{m} \;$ with constraints only defined by UNIQUE, VALUE-KEY and IsA. 

For a given simple schema we construct {\em a value-identification type}
$F(C)$ and a {\em value-representation type} $G(C)$ for all the classes $C$. Then a value-representable class $C$ is characterized
by $F(C) \neq ()$. 

$F(C)$ can be used to identify the objects
in this class by values. $G(C)$ can be used to provide the necessary values for insert- and update-operations.

Now let $exp_C$ denote the expression used to define the class $C$ and let $U(exp_C)$ denote the subexpression defined by a UNIQUE-constraint on $C$ provided it exists, otherwise let $\; U(exp_C) = () \;$.
Then the value-representability of a given schema can be detected using the following algorithm.\\ 

\begin{algorithm} \ \\
\label{alg}
\indent {\sc Input:} A set of class definitions \( \{ C_{1},...,C_{m} \} \).\\
\hspace*{40pt} {\tt Step 0}. Let \( \; \;  F(C_{i}) = () \; \; \) and \( \; \;  G(C_{i}) = exp_{C_i} \; \; \) for \( 1 \leq i \leq m.\)  \\
\hspace*{40pt} {\tt Step 1.} For all classes $C_{i}$ such that $\; U ( exp_{C_i} ) \;$ is a type expression\\
\hspace*{90pt} define $\; U ( exp_{C_i} ) \;$. \\
 \hspace*{40pt} {\tt Step 2.} If $C_{i}$ is a class with \( \; \;
F(C_{i}) = () \; \; \) and $\; F(D_{j}) \neq () \;$\\
\hspace*{100pt} for all classes \( \; D_{j} \; \) occurring in $\; U ( exp_{C_i} ) \;$ let\\
\hspace*{100pt} 
 \( F(C_{i}) \; \; = \; \;  U ( exp_{C_i} ) \; \; \) and replace all occurrences of classes \( \; D_{j} \; \)\\
\hspace*{120pt} in $F(C_i)$ and $G(C_i)$ by $F(D_j)$ and $G(D_j)$ respectively.\\
\hspace*{40pt} {\tt Step 3.} Repeat step 2 until it is no longer applicable.\\
\hspace*{40pt} {\tt Step 4.} For all classes $C_{i}$ such that \( \; \;  F(C_{i}) \neq () \; \; \)\\
\hspace*{90pt} replace each occurence of a class $\; D_{j} \;$ in $G(C_i)$ by $F(D_j)$\\
\indent {\sc Output:} Classes $C_{i}$ with their value-identification type $F(C_i)$ and\\
\hspace*{100pt} their value-representation type $G(C_i)$.\\

\end{algorithm}

\subsection{Definability of Generic Operations}

The requirement that object identifiers are to be hidden from users imposes
restrictions on the definability of generic operations. In case objects can not be distinguished by their values and references to other objects it is not possible to provide all these operations automatically. On the basis of algorithm \ref{alg}, however, we can decide whether generic functions 
are definable. Obviously, the functions {\bf insert\_object}, {\bf delete\_object} and {\bf update\_object} are definable for a class $C$ iff $C$ is value-representable.
In this case we can use the {\em value representation type} of the class $C$ and the {\em value identification type} of $C$ to derive the generic operations.

In general we need operations of the following kind:

\begin{itemize}

\item {\bf insert\_object}:\\
This operation takes a value of the {\em value representation type} of the corresponding 
class as input-parameter. A new identifier for this object is
provided by the system. 

\item {\bf delete\_object}:\\
This operation takes a value of the {\em value identification type} of the 
corresponding class as input-parameter such that the object in question can
be identified.

\item {\bf update\_object}:\\
This operation also takes values of the {\em value identification type} and of the {\em value representation type} of the
corresponding class as input-parameter such that the object in question can
be identified and its value can be changed.

\end{itemize}

The dynamics of SAMT is described by Dijkstra's guarded commands \cite{dij}. Since Dijkstra's calculus is computationally complete,
the representation of generic operations by transactions in persistent SAMT
modules is easy. 

\begin{exam}

Let the class {\sc Persons} be defined without the {\em Spouse} reference.
The insertion of a new person into this class can be expressed as
follows:

\end{exam}

\noindent
TRANSACTIONS \\
\hspace*{20pt} {\sl insert\_Person}(P :: PERSON) =\\
\hspace*{25pt} IF (member(P,range({\sl Persons})) = false $\longrightarrow$\\
\hspace*{30pt} @ I :: {\em  ID\_TYPE} \\
\hspace*{30pt} ($member(I,domain(Persons)$) = false $\longrightarrow$ \\ 
\hspace*{35pt} {\sl Persons} :=
union({\sl Persons},singleton(Pair(I,P)))))
\\

The @-substitution used in this example denotes an arbitrary selection of a
new identifier. A more formal introduction to this construct is given in
\cite{ab-rev}.

In case of integrity
constraints these operations have to be augmented to enforce the constraints.
For instance, IsA-relationships impose the following constraints on generic
operations:

\begin{itemize}

\item

Each insert into a subclass must include an insert into its superclass, e.g.,
an insertion of a student must include also a person insert.
 
\item

Each delete on the superclass must include a delete operation on the subclass.

\item

Update operations on subclasses (superclasses) may enforce updates on
superclasses (subclasses).

\end{itemize}

\noindent
In case of an insert this means to provide as additional
input the required data of the superclass. This can be easily
expressed exploiting the SAMT subtype facility, thus to compute these data via
the subtype coercion function.

\begin{exam}[SAMT representation]

The insertion of a new student into the class {\sc Students} requires the
insertion of a new person in the class {\sc Persons}:

\end{exam}

\noindent
TRANSACTIONS \\
\hspace*{20pt} {\sl insert\_Student}(S :: STUDENT) =\\
\hspace*{25pt} IF (member(stud\_proj\_person(S),range({\sl Persons})) = false $\longrightarrow$\\
\hspace*{30pt} @ I :: {\em  ID\_TYPE} \\
\hspace*{30pt} ($member(I,domain(Persons)$) = false $\longrightarrow$ \\
\hspace*{35pt} {\sl Students} := union({\sl Students},singleton(Pair(I,S))) $\|$\\ 
\hspace*{35pt} {\sl Persons} :=
union({\sl Persons},singleton(Pair(I,stud\_proj\_person(S)))))
\\

In addition there must exist operations to make an existing object in the
superclass also a member of the subclass, e.g. {\em
make\_Person\_a\_Student}, which generalizes the required insert
operations. The same applies in the opposite direction,
e.g., if we want a student in the database, who has finished his/her studies, 
to remain in the database simply as a person.

References also impose constraints on generic operations:

\begin{itemize}

\item

Each insert into a class must include an insert into the referenced class, provided the referenced object does not exist already. It may also include an update on the referenced object. E.g.,
an insertion of a person may include another person insert, the person's spouse. It may also include adding a reference from an already existing (unmarried) person to the inserted person.
 
\item

Each delete on a class must include delete operations on referenced classes. It must also include delete- or update-operations on objects referencing to the deleted object.

\item

Update operations on classes require updates, deletes or inserts on all other
classes referenced by or referencing to the class in question.

\end{itemize}

\noindent
The necessary values to enforce referential integrity are included in the value representation type of a class.

The representation in SAMT can be done in the
same manner as for IsA-relationships. provided there is no cyclic reference. However, if there is one,
generic operations become more complex since the necessary input should be
given as a {\em rational tree}, i.e. a finite or infinite tree which has only
finite number of subtrees. Such data structures can be represented e.g. by
$\psi$-terms \cite{life} or as values of recursive SAMT types.

\subsection{Extensions}

So far, for the detection of value-representability only simple schemas were considered. However, it is possible to enhance the computation of a class' value-representation by using semantic constraints.

\begin{figure}
\setlength{\unitlength}{0.9cm}
\Large
\begin{center}
\begin{picture}(11,4.5)
\thicklines
\put(2.5,3.5){\makebox(0,0)[b]{i}}
\put(7.5,3.5){\makebox(0,0)[b]{i}}
\put(1,1.82){\makebox(0,0)[b]{x}}
\put(2,1.82){\makebox(0,0)[b]{y}}
\put(3,1.82){\makebox(0,0)[b]{z}}
\put(4,1.82){\makebox(0,0)[b]{$\bot$}}
\put(6,1.82){\makebox(0,0)[b]{x}}
\put(7,1.82){\makebox(0,0)[b]{y}}
\put(8,1.82){\makebox(0,0)[b]{z}}
\put(9,1.82){\makebox(0,0)[b]{i'}}
\put(7.5,0.25){\makebox(0,0)[b]{x'}}
\put(8.5,0.25){\makebox(0,0)[b]{y'}}
\put(9.5,0.25){\makebox(0,0)[b]{z'}}
\put(2.5,3.3){\vector(-3,-2){1.5}}                
\put(2.5,3.3){\vector(-1,-2){0.5}}                
\put(2.5,3.3){\vector(1,-2){0.5}}                
\put(2.5,3.3){\vector(3,-2){1.5}}                
\put(7.5,3.3){\vector(-3,-2){1.5}}                
\put(7.5,3.3){\vector(-1,-2){0.5}}                
\put(7.5,3.3){\vector(1,-2){0.5}}                
\put(7.5,3.3){\vector(3,-2){1.5}}                
\put(9,1.75){\vector(-3,-2){1.5}}                
\put(9,1.75){\vector(-1,-2){0.5}}                
\put(9,1.75){\vector(1,-2){0.5}}
\put(9.5,2){\line(1,0){0.5}}
\put(10,2){\line(0,1){1}}
\put(10,3){\vector(-3,1){2}}                
\end{picture}
\end{center}
\normalsize
\caption{\label{identifier}
The graphs of the class {\sc Persons}}
\end{figure}

\begin{exam}
\label{quadrat}

Let the UNIQUE-constraint on the class{\sc Persons} in example \ref{spouse}
be changed to {\em UNIQUE(PERSON,Spouse)}. In this case $F(${\sc Persons}$) =
() $. Using the additional constraint \ {\em Spouse(x) = y $\; \Rightarrow \;$ Spouse(y) = x } \ the class {\sc Persons} gets
value-representable, since each person is either not married and
represented by its value of type {\em PERSON} or is married and represented by
its value of type {\em PERSON} together with the value of his/her spouse. The possible structures of objects in
this class are illustrated in figure \ref{identifier}.

\end{exam}

Generally, if in a schema several semantic constraints are defined, then for
value representability of a class cycles of references need to be
considered. Given a cycle from a class $C$ to itself by the reference
function $f$, we can distinguish several cases:

\begin{itemize} 

\item \( \forall x . \; \; \exists n \neq n' . \; \; \; \; f^{n}(x) \; = \;  f^{n'}(x') \; \vee \; f^{n}(x) \; = \; \bot  \) 

\item \( \exists n . \; \; \forall x . \; \; \; \; f^{n}(x) \; =\;  \bot \; \vee \; f^{n}(x) \; = \; x \) 

\end{itemize}
 
\noindent 
In the second case, the value-representability can be derived as in 
example \ref{quadrat}. In the first case, the
value-representability is based on the finiteness of the database. In this case the value representation type is a {\em rational tree}, i.e. a finite or infinite tree which has only
finite number of subtrees. Such data structures can be represented e.g. by
$\psi$-terms \cite{life} or as values of recursive SAMT types. Consequently the derived generic operations become more complex. 

\section{Extensibility}

\label{ext}

The kernel language can be seen as a short notation of SAMT constructs. Let us
now indicate some extensions to this language by other constructs that are
also expressible in SAMT. This style of extending the kernel language has the
advantage that all new constructs  are well-founded. We show this for some
static and for one dynamic integrity constraint. In the same manner, new types
and complex transactions can be introduced. 

Static constraints in databases can be distinguished according  to their abstraction level and their importance for values and objects \cite{Tha 88}.
Now we show how integrity constraints can be used in an extended kernel language. 

\begin{exam}
Given the two classes {\sc Professors} and {\sc Students}. If objects 
representing professors and objects representing students have to be mutually
different then we express this by the {\em exclusion dependency}:

\[ \mbox{\sc
Professors} \; \| \; \mbox{\sc Students} \; . \] 

\noindent
This integrity constraint is
directly represented in SAMT by the following static invariant:

\end{exam}

\noindent
INVARIANT\\
\hspace*{20pt} STATIC {\em With I :: {\em  ID\_TYPE} :\\
\hspace*{30pt} member(I,domain({\sl Professors})) = true $\Rightarrow$
member(I,domain({\sl Students})) = false ; \\ 
\hspace*{30pt} With I :: {\em  ID\_TYPE} :\\
\hspace*{30pt} member(I,domain({\sl
Students})) = true $\Rightarrow$ member(I,domain({\sl Professors})) =
false ;}\\

\begin{exam}
Given the two classes {\sc Professors} and {\sc Students} which are subclasses
of the class {\sc Persons}. If person represented in the database is a professor
or a student then we can express this by the cover constraint:

\begin{quote}
{\sc Persons}  $ = $ {\sc Professors}  $\bigcup$ {\sc Students},
\end{quote}

which can be represented in SAMT
by the following static constraint:

\end{exam}

\noindent
INVARIANT \\
\hspace*{20pt} STATIC {\em With I :: {\em  ID\_TYPE} :\\
\hspace*{30pt}  member(I,domain({\sl Persons})) = true $\Rightarrow$ \\
\hspace*{40pt} member(I,domain({\sl Students})) = true $\vee$ 
member(I,domain({\sl Professors})) = true ; }\\

\noindent
Let us define another constraint restricting the migration of objects from one
class to another. 

\begin{exam}

Given the two classes {\sc Professors} and {\sc Students} which are subclasses of the class {\sc Persons}. Students can become professors but professors can not become students. Therefore, we restrict the scheme by the integrity constraint \\
\indent {\em ImpossibleMake({\sc Professors, Students})} .\\
This integrity constraint is directly represented in SAMT by the following transition constraint.

\end{exam}

\noindent
INVARIANT\\
\hspace*{20pt} TRANSITION {\em With I :: {\em  ID\_TYPE} :\\
\hspace*{30pt} member(I,domain({\sl Professors})) = true $\; \wedge \;$
member(I,domain({\sl Students})) = false\\
\hspace*{35pt} $\Rightarrow$ 
member(I,domain({\sl Students$^\prime$})) = false ; }\\ 

\section{Conclusion}

In this paper we propose kernel constructs of a high-level strongly-typed
language for object-oriented database design. Schemata written in this
kernel language can be transformed automatically into representations in the
formal specification language SAMT, a strongly-typed modular language
supporting general subtyping and module inheritance within a uniform formal
framework. This transformation process includes the derivation of generic
operations on classes enforcing inclusion dependency and referential integrity.
As a consequence the object-oriented design inherits the formal semantics of
SAMT. Other benefits of the SAMT representation are seen in the possibility to prove
transaction safety and the reification dimension provided by SAMT's refinement
capability that does not depend on a specific target database language or DBMS.

Moreover, we discuss the problems of value representability of
object-oriented designs. The question whether a class can be completely
characterized by values or not is crucial for
avoiding ambiguities in object definitions. On the basis of our kernel language
we describe an algorithm for the detection of value representability. Thus,
safety in our approach is achieved in several ways:

\begin{itemize}

\item by its foundation on a uniform formal framework,

\item by the detection of value representability, and

\item by consistency proof obligations for transaction safety.

\end{itemize}

\noindent
Another advantage of this approach is its extensibility. SAMT can be used to meet
all the requirements for object-oriented databases \cite{oo-manifesto} except
those that can only be solved at the level of implementation. This can be
exploited to extend the outlined kernel language without losing any of its
advantages. We demonstrate this feature by the introduction of additional
static and dynamic constraints. Moreover, we discusse the increase in
operation complexity due to such extensions.

The outlined approach combines functional,
imperative and object-oriented concepts in a uniform formal
framework (see also \cite{paradise}). The specification of operations in SAMT types provides the functional
part, operations in modules support the imperative style, and the
encapsulation feature of modules enables object-orientation.


\begin{thebibliography}{12345678}

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

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

% \bibitem[AbVi89]{abiteboul-vianu} S.~Abiteboul, V.~Vianu: {\it A 
% Transaction-Based Approach to Relational Database Specification}, J.~ACM vol.
% 36 (4), Oct. 1989, pp. 758 -- 789
%
% \bibitem[Ab89]{ab-large}
% J.R. Abrial: {\it A Formal Approach to Large Software Construction}, in 
% J.~L.~A.~van~de~Snepscheut (Ed.), {\it Mathematics of Program Construction}, 
% Springer LNCS 375, 1989

\bibitem[Ait90]{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[Ait90a]{paradise} H.~A\"{\i}t-Kaci: {\it A Glimpse of Paradise}, in J.~W.~Schmidt, A.~A.~Stognij (Eds.): Proc. Next Generation Information 
Systems Technology , Springer LNCS, vol. 504, 1991, pp. 17 -- 25

\bibitem[AGO91]{albano1} A.~Albano, G.~Ghelli, R.~Orsini: {\it Objects and Classes for a Database Programming Language}, FIDE technical report 91/16, 1991

\bibitem[AGO91a]{albano2} 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[AlTh90]{AlFedaghi}
S. Al Fedaghi, B. Thalheim: {\it Fundamentals of databases - The key concept},
submitted for publication, 1990

\bibitem[ABD$^+$90]{oo-manifesto} M.~Atkinson, F.~Bancilhon, D.~DeWitt, K.~Dittrich, S.~Zdonik: {\it The Object-Oriented Database System Manifesto}, SIGMOD 1990

\bibitem[BBB$^+$88]{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[Bee89]{beeri2} C.~Beeri: {\it Formal Models for Object-Oriented 
Databases}, Proc. 1st DOOD 1989, pp. 370 -- 395

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

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

% \bibitem[Bj{\o}78]{vdm}
% D.~Bj{\o}rner: {\it The Vienna Development Method VDM: The Meta Language}, 
% Springer LNCS 61, 1978 
%
% \bibitem[BJM$^+$89]{daida} A.~Borgida, M.~Jarke, J.~Mylopoulos, 
% J.~W.~Schmidt, Y.~Vassiliou: 
% {\it The Software Development Environment as a Knowledge Base Management 
% System}, in J.~W.~Schmidt, C.~Thanos (Eds.):
% {\em Foundations of Knowledge Base Management}, Springer TIS, 1989

\bibitem[BBMR89]{classic} A.~Borgida,  R.~J.~Brachmann, D.~L.~McGuiness, L.~A.~Resnick: {\it CLASSIC: A Structural Data Model for Objects}, Proc. ACM SIGMOD, June 1989, pp. 59 -- 67

\bibitem[BrSc85]{klone} R.~J.~Brachmann, J.~G.~Schmolze: {\it An Overview of the KL-ONE Knowledge Representation System}, Cognitive Science, vol. 9 (2), April 1985, pp. 171 -- 216

\bibitem[BrWe87]{wegner} K.~B.~Bruce,P.~Wegner: {\it An Algebraic Model of
Subtype and Inheritance}, in F.~Bancilhon, P.~Buneman (Eds.): {\it Workshop
on Database Programming Languages}, Roscoff, France, September 1987

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

\bibitem[CaSc87]{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[DiSc89]{dij}
E. W. Dijkstra, C. S. Scholten: {\it Predicate Calculus and Program Semantics}.
Springer-Verlag, 1989.

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

\bibitem[FBC$^+$87]{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[Flo67]{floyd} R.~W.~Floyd: {\it Assigning Meanings to Programs}, in 
% J.~T.~Schwartz (Ed.): Proceedings of the AMS Symposium on Applied Mathematics, % vol. 19, 1967
%
% \bibitem[GTW76]{adj} J.~A.~Goguen, J.~W.~Thatcher, E.~G.~Wagner: {\it An 
% Initial Algebra Approach to the Specification, Correctness and Implementation 
% of Abstract Data Types}, in R.~T.~Yeh (Ed.): Current Trends in Programming 
% Methodology, vol. 4: Data Structuring, Prentice Hall 1978
%
% \bibitem[Gut75]{gut} J.~V.~Guttag: {\it The Specification and Application to 
% Programming of Abstract Data Types}, Ph.D. thesis, University of Toronto, 1975

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

\bibitem[HeSa91]{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[KhCo86]{KC 86} S. Khoshafian, G. Copeland: {\it Object Identity}, 
Proc. 1st Int. Conf. on OOPSLA, Portland, Oregon, 1986

\bibitem[KBB$^+$88]{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[LoSc87]{lockemann} P.~Lockemann, J.~W.~Schmidt: {\it Datenbankhandbuch}, Springer, 1987

\bibitem[LNPS85]{back} K.~v.Luck, B.~Nebel, C.~Peltason, A.~Schmiedel: {\it BACK to Consistency and Incompleteness}, in H.~Stoyan (Ed.): {\it GWAI-85}, Springer IFB 1986, pp. 245 -- 257

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

\bibitem[MBW80]{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[MBJK90]{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[Oho90]{ohori} A. Ohori: {\it Representing Object Identity in a Pure Functional Language}, Proc. ICDT 90, Springer LNCS, pp. 41 -- 55

\bibitem[SaJu91]{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[SSW91]{vdm91}
% 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[SSW$^+$91a]{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

\bibitem[SWS91]{iwsds} K.-D.~Schewe, I.~Wetzel, J.~W.~Schmidt: {\it Towards a Structured Specification Language for Database Applications}, in Proc. Int. Workshop on the Specification of Database Systems, Glasgow, 1991

% \bibitem[Spi88]{z} J.~M.~Spivey: {\it Understanding Z, A Specification
% language and
% its Formal Semantics}, Cambridge University Press, 1988

\bibitem[Su83]{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[Tha88]{Tha 88} B.~Thalheim: {\it Dependencies in Relational Databases}, Teubner Leipzig, 1988

\bibitem[Tha90]{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}
