% File: finaldb.tex
% Date: 12-JUL-1989 copied from Frankfurt 
%       DU1:[DBIS.FUEHLER.VERWALTUNG.JWS..]FINALDB.LATEX
% Date: 20-NOV-1989 adapted to HH Latex
%			    changed FFM address to HH

\documentstyle[a4]{article}                          

\setlength{\topskip}{0truecm}
\setlength{\textwidth}{16.5truecm}
\setlength{\textheight}{22.9truecm}
\setlength{\parskip}{8pt}
\setlength{\parindent}{0cm}

% ##\pagestyle{empty}

\newcommand{\comment}[1]{} 
                  
\newfont{\bfsl}{cmbxsl10 scaled 1000}

\def\ISA{IS-A\ }
\def\IsA{IS-A\ }
\def\WHERE{WHERE\ }
\def\IS{IS\ }
\def\COUNT{Count}
\def\SetOf{SetOf\ }
\def\ANYTHING{Anything}
\def\EACH{{\bfsl each}\ }
\def\OF{{\bfsl of}\ }
\def\IN{{\bfsl in}\ }
\def\IsIn{\ {\bfsl isIn}\ }
\def\SubSetOf{{\bfsl subsetOf}\ }
\def\THIS{{\bfsl this}}
\def\ALL{ {\bfsl all}\ }
\def\AND{ {\bfsl and}\ }
\def\NOT{{\bfsl not}\ }
\def\OR{{\bfsl or}\ }
\def\ADDED{{\bfsl Added}\ }
\def\REMOVED{{\bfsl Removed}\ }
\def\NEW{{\bfsl New}}

           
\def\fig#1#2{

{ \centerline{{\bf Fig. #1:} #2} }}
\begin{document}


\begin{center}
\vspace{5cm}            
                            
{\Large\bf Database Programming by Formal Refinement of \\
Conceptual Designs}

\medskip

\bigskip
\bigskip
\begin{tabular}{ccc}

Alexander Borgida
&
John Mylopoulos
&
Joachim W. Schmidt, Ingrid Wetzel\\
Dept. Comp. Science
&
Dept. Comp. Science
&
Fachbereich  Informatik\\                                              
Rutgers University
&
University of Toronto
&
Universit\"at Hamburg\\
New Brunswick, NJ08904
&
Toronto M5S 1A4, Ont.
&
D-2000 Hamburg 13\\
USA
&                         
Canada
&
F.R. Germany\\
{\scriptsize borgida@aramis.rutgers.edu}                                 
&
{\scriptsize jm\%utai\%toronto.csnet@relay.cs.net}
&
{\scriptsize schmidt@rz.informatik.uni-hamburg.dbp.de}\\
\end{tabular}
\\
\medskip
\end{center}
\vspace{3em}
                                      


\begin{abstract}
In the process of developing an Information System, one passes through 
stages that include requirements gathering, design specification, and,
last but not least, the implementation and maintenance of large database 
application programs. With an evolutionary view on the application domain 
and its requirements, captured by the knowledge representation language 
Telos, we first discuss the conceptual design of an information system 
by the TDL language  and then concentrate on the iterative  refinement 
of TDL designs into database programs. Our target language is DBPL, a 
procedural database programming language with persistent values of a 
wide variety of types and with database transactions as first-class 
language constructs. DBPL was designed with particular emphasis on 
database and program modularity. The refinement of TDL designs into 
DBPL implementations is  formalized in  J.-R.~Abrial's framework of 
Abstract Machines and Generalized Substitutions.
\end{abstract}


\section{Motivation and Setting}

The authors and their collaborators, are involved in project DAIDA, whose 
goal is to build a novel software engineering environment for developing 
and maintaining Information Systems \cite{software}. It is generally agreed that the 
development of software systems, including Information Systems, involves 
stages such as requirements definition, design and implementation/testing.

One of the key features of the DAIDA project are the use of three specific 
(kinds of) languages for the description of the software at each stage:

\begin{itemize}
\item a knowledge representation language for domain analysis;
\item a semantic data model for the conceptual design of states 
      and transitions; and 
\item an imperative programming language for efficient management 
      of large, shared data sets.
\end{itemize}

Among the expected contributions of the project will be a better 
understanding of the problems and tools/techniques for moving 
from a problem specification to the implementation of an 
Information System with data management components of significant 
complexity but relatively straight-forward procedural requirements.

For determining the user's requirements, we have argued that it is 
important to arrive at, and capture, an understanding of the application 
domain \cite{Knowledge}.  For this purpose, we have progressed through a series of  
languages, the latest called Telos, which allows one to represent a 
temporal model of the application domain in an assertional knowledge 
representation language \cite{AKnowledge}. Telos uses the paradigm of objects 
related by temporally qualified relationships to describe the entities 
and activities (both generic and specific) that occur in a particular 
world. The crucial fact about Telos is that {\em every aspect} of the 
description is associated with {\em time intervals}: the occurrence of 
activities, the membership of objects in classes, the relationships 
between objects, activities, etc.; in fact, in a recursive process, not 
only is the domain viewed temporally, but also the description itself is 
temporally indexed.

There are several problems with jumping from the user's conceptual 
requirements directly to the code of a database program :
\begin{itemize}
\item not everything seen by the user in the world needs to be part of 
      the final software system - much of it is contextual information; 
\item Telos is meant to capture the ontology of the user domain (so a 
      project is viewed as an activity) while a database usually captures 
      information {\em about} the domain (so there may be a {\em data} class 
      corresponding to some activities in the world); 
\item in most environments there are multiple needs/goals that are being 
      achieved, and these need to be integrated; 
\item finally, the descriptions in Telos and DBPL are just too widely 
      different in style.
\end{itemize}

TDL therefore is concerned with the intermediate stage of {\em conceptual 
design}: identifying, specifying, and relating the data and procedural  
{\em components}  of an information system, which itself is to be implemented 
in DBPL. 

In this paper we shall briefly discuss the rationale behind DAIDA's 
languages, concentrating on the two activities of conceptual design in 
TDL [13 ]  -- backed by the knowledge representation language Telos \cite{AKnowledge} --, 
and of software development in the database programming language DBPL \cite{DBPL}.
Furthermore, we shall outline certain innovative tools and techniques 
that are used to iteratively  map TDL designs into DBPL programs by 
successive formal refinements within the framework of Abrial's Abstract 
Machines and Generalized Substitutions \cite{Abstract}, \cite{Formal}.


\section{TDL:   A Language for Conceptual Designs}
TDL is based on our experience with  Taxis \cite{Alanguage} with set extensions for 
attributes and constraints motivated by  DBPL as a mapping target and 
Abrial's Abstract Machines \cite{Set}, \cite{AZ} as a mapping technology. 

For data design, a number of different kinds of data classes can be 
defined in TDL. Besides Base Classes and Enumerated Classes, TDL 
distinguishes

\begin{itemize}
\item Aggregate Classes, which are essentially labeled Cartesian 
      products, and whose instances have quality decided structurally; and
\item Entity Classes, which have an associated extent: a set of objects 
      with intrinsic, unchanging identity. The definition  of entity 
      classes specifies, among others, the attributes applicable to 
      their instances, as  well as their  ranges.
\end{itemize}

Moreover, TDL has a small set of built-in primitive attribute {\em qualifiers}, 
which allow constraints to be placed on attribute values, and their 
evolution over time:

\begin{itemize}
\item UNCHANGING attributes cannot be modified, once assigned a value;
\item CHANGING attributes, in contrast, may get different values as states 
      change;
\item UNIQUE attributes are required to have different values for all 
      instances of the class (i.e., can act as "keys" in relational terms).
\end{itemize}

These qualifiers  correspond  to constraints that are frequently useful in 
the practice of data base system design. (Note also the contrast with 
Telos, where a user of the language may create arbitrary new attribute 
qualifiers in order to  abbreviate constraints -- this, because attributes
are first class citizens in Telos.)

For {\em state change and evaluation} , TDL provides for the definition of 
two kinds of procedures: 

\begin{itemize}
\item functions, which are evaluated with respect to a single database state, 
      and leave it unchanged while returning a value; and 
\item transactions, that specify atomic state transitions, where the final 
      state is supposed to be free of inconsistencies. 
\end{itemize}

Transactions specify state transitions, and their parameters appear as 
attributes  with the property categories IN and OUT indicating whether the 
parameter is used to communicate information into or out of the transaction. 

A specification is intended to associate with every transaction a set of 
acceptable state transitions. One standard approach is that of constraint 
assertion  on the values of the state variables (attribute functions, 
parameters and class extents) . For transactions this is the familiar 
precondition/postcondition notation 
introduced by Hoare relating the initial and final states which is widely 
used in such specification languages as Z \cite{Z}, \cite{Specification} and the Larch language 
families  \cite{Larch}. In TDL those assertions are expressed in the usual 
Taxis-like notation, under two attribute categories:

\begin{itemize}
\item GIVEN: conditions required to hold in the initial state when the 
      transaction is  invoked;
\item GOALS: conditions required to hold in the final state.
\end{itemize}


Both conditions are logical assertions, with goals able to relate values in 
both the initial and final state. For this purpose, we use the standard 
technique of distinguishing initial and final state values of variables  
by marking with the suffix ' the values to be evaluated in the final state. 

The insertion and removal of objects from the extents of classes is 
expressed through two attribute categories, PRODUCES and CONSUMES, that 
assert that the attribute value finally is (is not, resp.) an instance 
of the class specifying its range. An example of a TDL design is given 
in the Appendix, Fig. 1. Additional conditions for  ``normal-case first''
 abstraction and exception handling are discussed in \cite{Language}.

Transactions describe atomic state transitions. Especially in business 
and administrative environments, it is often necessary to present more 
global constraints on sequences of actions (e.g., an employee needs 
to have a physical examination before completing the pay form). In order 
to support such sequencing specifications, we introduce scripts, which 
are composed of {\em locations/states}, and {\em transitions}  connecting 
the states, where each transition contains an atomic transaction. A detailed 
discussion of scripts and communication facilities between them can be 
found in \cite{DAIDA}, \cite{Dialogue}, \cite{Extended}. 

It should come as no surprise that subclass hierarchies are supported 
and their use is encouraged throughout the design, according to the 
methodology described in \cite{General}. Note that as a specification language, TDL 
makes no commitment on how such attributes are to be stored (arrays, 
records, relations) in the final system,  nor in fact whether the 
information provided by the attribute will be obtained by look-up or 
computed by a function. It is the prime goal of DAIDA to provide an 
environment that supports the systems implementor in making and 
justifying decisions required to map TDL designs into DBPL 
implementations.  


\section{DBPL: A Type-Complete Database Programming Language}

At the other end -- implementation -- we have available the database 
programming language DBPL \cite{DBPL},  a successor of Pascal/R \cite{Some}. DBPL 
integrates a set- and predicate-oriented view of database modeling into 
the system programming language Modula-2 \cite{Specandver}. Based on integrated 
programming language and database technology, it offers a uniform 
framework for the efficiency-oriented implementation of data-intensive 
applications. 

DBPL is a strongly and statically typed language equipped with a rich 
set of base types (Integer, Real, Boolean, Character, \dots) which can 
be combined by a variety of type constructors (array, record, variants, 
set/relation). DBPL is {\em type-complete} in the sense that its type 
constructors can be applied to any base type and can be combined freely 
(e.g., to define nested sets). Furthermore, any type can be used in any 
context, e.g., in local scopes or in parameter positions. 

A central design issue of DBPL was the development of abstraction mechanisms 
for database application programming \cite{Abstraction}, \cite{Data}. DBPL's bulk data types are 
based on the notion of (nested) sets, and first-order predicates are 
provided for set evaluation and program control. Particular emphasis 
had been put on the interaction between these extensions and the type system 
of Modula-2. DBPL extends Modula-2 {\em orthogonally} into three dimensions: 

\begin{itemize}
\item bulk data management through a data type {\em set/relation};
\item abstraction from bulk iteration through  {\em first order} predicates , 
      iterators and set expressions; 
\item {\em database modules}  for sharing and persistence of DBPL objects and 
      {\em transactions}  for failure recovery and concurrency  control.
\end{itemize}

DBPL programs can be structured into sets of modules with well-controlled 
interfaces through which DBPL objects are exported and imported. Since 
data-intensive applications require the persistence of states between and 
the sharing of states across program executions, DBPL has the notion of 
{\em database modules} that make all its variables persistent. Persistent 
variables are protected by disallowing any access from outside a transaction. A 
first impression of the overall software engineering quality of DBPL 
implementations is given by the complete DBPL example presented in the 
Appendix, Fig. 2.

\section{From TDL Designs to DBPL Implementations}

A major effort of the DAIDA project concentrates on the production of 
high-quality database application software. DAIDA  makes the following 
assumptions about this software production process:

\begin{itemize}
\item for a given TDL-design there may be many substantially different DBPL 
      implementations, and it needs human interaction to make and justify 
      decisions that lead to efficient implementations;
\item the decisions are too complex to be made all at once -- let alone 
      automatically; it needs a series of refinement steps referring to 
      both data and procedural objects;
\item the objects and decisions relevant for the refinement process need 
      to have formally assured properties;
\item these properties should be recorded to support overall product 
      consistency and evolution.
\end{itemize}
          
To meet the above requirements, DAIDA relies heavily on current work of 
J.-R.~Abrial \cite{Abstract}, \cite{Formal}:

\begin{itemize}
\item TDL designs are translated into Abstract Machines with states 
      represented by  mathematical objects like functions and sets, 
      and state transitions defined by Generalized Substitutions;
\item the formal properties of Machines and Substitutions are assured and 
      organized by Abrial's interactive proof assistant, the B-Tool \cite{B}. 
\end{itemize}

In the remainder of the paper we report on our first experience with 
a rule-based Mapping Assistant that helps refining TDL designs into 
DBPL implementations via Abstract Machines. First we outline the formal 
framework, and then we discuss in some detail the refinement process itself.  

For an example we use part of the TDL-design given in the Appendix, 
Fig.1. ResearchCompanies consists of three entity class definitions 
(Companies, Employees, Projects) and one transaction definition 
(HireEmployee). One of the invariants asserts that the projects a 
company is engaged in are exactly those which have this company as 
a consortium member. Another invariant enforces the projects on which an 
employee works to be a subset of the projects his company is engaged in. 
For some of the classes UNIQUE attributes are specified, for the class 
employees there is no such attribute.

\subsection{Abstract Machines and Generalized Substitutions}

Abrial's framework for specifying and developing software systems is based 
on the notion of Abstract Machines, a concept for organizing large 
specifications into independent parts with well defined interfaces 
\cite{Abstract}. An Abstract Machine is a general model for software systems and
is defined by a state (the statics of the system) and a set of 
operations modifying the state (the dynamics). 

The {\em statics of a system}  includes the definition of three main Abstract 
Machine components: Basic Sets, Variables, and system Invariants. 
{\em Basic Sets}
define time-invariant repositories of objects (types) that may  occur in 
our application. In a first version of an refinement, they may be 
completely abstract, defined only by their name. The {\em Context}  allows us 
to freeze the definition of basic sets as soon as we made a decision on 
their properties. {\em Variables}  are either time-dependent subsets of the 
Basic Sets and model the state of an Abstract Machine, or they are 
binary relations that associate elements of Basic Sets (viewed as 
functions from the domain to the range). Finally, the {\em Invariants}
express the static relationships within the system. They are defined 
in terms of predicates and sets (with a rich choice of operators for set, 
relation, and function (re-) definition). 

The {\em dynamics of a system}  are defined by the Operations of an Abstract 
Machine. The definition of an operation, for example, HireEmployee,  
reads as follows:

{\sl\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill
xx\=xx\=xx\=xx\= \kill
OPERATIONS HireEmployee (name, belongs, works)  =  \\
\>	     	PRE name   $\in$ EmpNames    $\wedge$ 
			belongs   $\in$ companies    $\wedge$ 
			works   $\in$   $\wp$ (engagedIn(belongs)) \\ 
\>		THEN ANY e IN (Employees - employees) \\
\> \> 			THEN (empName(e), worksOn(e)), belongsTo(e)
                        $\mid$$\leftarrow$ (name, works, belongs) 
                        $\mid$$\mid$ \\ 
\> \> \> 	  	employees   $\mid$$\leftarrow$ employees   $\cup$ \{e\} 
	 	$\mid\mid$    % Test: $$ entfernt
 		HireEmployee   $\mid$$\leftarrow$ e \\
\> \> 			END \\ 
\>		END HireEmployee;
\end{tabbing}}

Operations are specified by the constructs of the Generalized Substitution 
Calculus with semantics defined by the weakest precondition under which 
a construct fulfils a given postcondition. In our example operation, the 
ANY-substitution expresses an unbounded non-deterministic substitution. 
It chooses an arbitrary fresh member from (Employees -- employees), i.e., 
from the set of non-instantiated elements considered for employee 
representation. Next, the (attribute-) functions for that new employee 
element are redefined in parallel. The ``type conditions'' on the input 
parameters are expressed by the preconditions of the Generalized Substitution. 

\subsection{Consistency of Designs}

With Abstract Machines we are in a position to prove the consistency of 
specifications, a task that is of particular importance for heavily 
constrained database applications \cite{Specandver}. In general, we have to 
prove for each operation that it preserves the invariants of the 
Machine. If, for any reason, the designer of our TDL transaction had 
forgotten the GIVEN clause, this would result in  the following 
lemma (simplified version):    

{\sl
belongs $\in$ companies $\wedge$ works $\in\wp$ (projects) $\Rightarrow$
works $\in\wp$ (engagedIn ( belongs )).
}

By realizing that this lemma is not provable the designer learns that the 
precondition of the transaction HireEmployee  is too weak; the reason is 
the dependency between the new employee, his company, the projects he is 
supposed to work on and the projects that his company is engaged has not 
been taken into account.

\subsection{On Data and Procedure Refinement}

In our setting, refinement is defined between Abstract Machines having the 
same signature, i.e., the same number of operations and parameters. A 
Machine, A (the more abstract one) is said to be refined by a Machine C 
(the more concrete one) iff the refinement predicate, P$_{AC}$, that relates 
the state variables of both machines is proven to be an invariant under 
all operations, S$_{A}$ and S$_{C}$, of both machines, A and C. The proof 
obligation also considers the case of a non-deterministic operation in 
machine A and a less non-deterministic one in machine C. A mapping process 
usually consists of a series of procedure- and data-oriented refinement 
steps from one Abstract Machine into another. The refinement process can 
be directed interactively by the user and controlled formally by the proof 
assistant.              
                  
{\em Data refinement}  is defined in two steps:

\begin{itemize}
\item a data representation has to be chosen that is "closer" to the concrete 
      data structures being offered by the target programming language used 
      to implement the specification;
\item the relationship between the more concrete state space and the more 
      abstract one has to be expressed by a refinement predicate that 
      involves variables of both machines.
\end{itemize}      

Usually, changes in data representations imply refinements of operations. 
An operation S$_{A}$ is refined by an operation S$_{C}$ ``if S$_{C}$ can be 
used instead of S$_{A}$ without the 'user' noticing it'' \cite{Abstract}. This means 
more formally: all postconditions R that are established by S$_{A}$ are also 
established by S$_{C}$. Within the framework of Generalized Substitutions, 
algorithmic refinement is formally defined as a partial order relation 
between substitutions \cite{Abstract}.

Currently, we are experimenting with a standard refinement strategy 
consisting basically out of  three steps \cite{Conceptual}. In each step  we decide 
upon one  major task in database modeling: 

\begin{enumerate}
\item identification of data objects in extents of varying cardinalities; 
\item alternative ways of clustering data into a variety of data 
      structures; and 
\item introduction of those constraints for variables, parameters, etc. that 
      can be checked efficiently and at appropriate times (static typing).
\end{enumerate}

After these three refinement steps we are in a position to automatically 
transform the final Abstract Machine into an equivalent DBPL program.

For the {\em first refinement} step of our example, we make the rather 
specific but common decision to utilize the uniqueness constraints on 
properties for companies and projects for data identification. For 
employees, where the application doesn't provide such a constraint, our 
refinement introduces an additional property, empId, for which the 
implementation assures uniqueness. Due to the change in the data 
representation, the operation HireEmployee, becomes less non-deterministic: 
the arbitrary ANY-substitution is replaced by some operation, newEmpId, 
that provides a fresh EmpId-value, which is then associated with the 
required properties through function extension. Our refined data and 
procedure representation can be proven to meet all the invariants layed 
down in the initial Abstract Machine. 

Having decided upon identification, we are now ready for the 
{\em second refinement}  step that designs the central  data structures 
of our implementation. While our first Abstract Machine has a 
purely functional view on data, we now refine into a representation that 
is based on Cartesian products. It is on this level where we have to 
decide whether our data structures have set-valued attributes (i.e., 
will finally be mapped into nested DBPL relations) or will be flattened. 
In our example we decide for the first alternative.


On our way down to implementation there is a {\em third refinement}
 step left that deals with data typing. Since DBPL is a strongly and 
statically typed language we want to refine the variables to become partial 
functions over the Basic Sets instead of total functions that range over 
other variables with time-varying cardinalities. With the same arguments, 
the precondition of the hire operation is weakened into a static 
constraint that will finally become the parameter types of the 
HireEmployee transaction. However, to meet the inherited specification we 
have to strengthen our constraints by introducing a 
{\em conditional substitution} which, due to the semantics of Generalized 
Substitutions, will finally result in a first-order query predicate on 
the variables that represent database states and transaction parameters 
(compare DBPL transaction, HireEmployee, Appendix, Fig. 2):

{\sl\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill                               
\>  	OPERATIONS  HireEmployee (name, belongs, works) =\\
 \> \> PRE         
 	 name   $\in$ EmpNames $\wedge$
 	 belongs   $\in$ CompNames $\wedge$
 	 works   $\in$   ProjIdRelType\\
 \> \> THEN IF
	    	belongs   $\in$ companies   $\wedge$
		works   $\in$    $\wp$ (engagedIn(belongs)) \\
\>\>\> THEN
tEmpId   $\mid$$\leftarrow$ newEmpId;\\
\>\>\>\> empRel   $\mid$$\leftarrow$ empRel   $\cup$
 		\{(tEmpId, name, belongs, works)\}; \\
\>\>\>\> HireEmployee   $\mid$$\leftarrow$ tEmpId \\
\>\>\> ELSE HireEmployee   $\mid$$\leftarrow$ 
nilEmpId \\
\>\>\> END\\
\> \> 	    	END HireEmployee;\\[0.8ex]
\> OTHER newEmpId $\in$ ( $\rightarrow$ (EmpIds - employees));\\
\end{tabbing}}

Our example demonstrates that a refined operation  may have a weaker 
precondition than the initial one: HireEmployee  is now defined in all 
cases in which the static type predicate holds (a condition which can 
already be verified at compile time). It either performs the required 
state transition or it returns as an exception a specific value, nilEmpId.


\subsection{Final Mapping into DBPL Programs}

A language like DBPL with a rich typing system and with first-order calculus 
expressions for set evaluation and control turns out to be an appropriate 
target for the implementation of sufficiently refined Abstract Machines. 
Informally speaking, we can compile those machines into equivalent DBPL 
programs which are based on variables constrained by static type predicates 
and on operations defined by deterministic and sequential Generalized 
Substitutions.

In the final refinement step of HireEmployee  the state-dependent 
precondition is transformed into a static one plus a conditional 
substitution. The static condition is transformed into DBPL parameter 
types, and the conditional substitution results in a database update 
statement controlled by a first-order database query expression (Appendix, 
Fig. 2).


\section{Summary}

We have presented, rather sketchily, some of the highlights of two 
languages, TDL and DBPL for the conceptual design and the implementation 
of an information systems. 

TDL is based  on the language Taxis, but it has been refurbished to permit 
the predicative  description of procedures (transactions, functions, 
script transitions), integrity constraints and coordinated transaction 
groups (scripts). TDL's expression language, unlike Taxis,  is based on
 set theoretic notions. TDL maintains an object-oriented approach, thus 
allowing  designers who map Telos requirements into TDL designs to concern 
themselves  mostly with global issues such as  view integration and 
the elimination of omni-present temporal indices.

On the other hand, TDL adopts the standard (destructive) state based model 
of computation of most procedural languages, and thus the mapping to DBPL 
programs can concentrate on the appropriate choices for data identification, 
structuring and typing and corresponding refinement steps on transactions 
and functions.
                    
As argued in the previous section, Abrial's methodology of refining 
abstract machines appears to be a promising direction in which to 
study the issue of this implementation in a provably correct manner. In 
this setting, a language like DBPL with a set- and predicate-oriented 
approach to data modelling, a rich typing system, and abstract support 
for concurrency, recovery and persistence, turns out to be an appropriate 
target for the refinement of TDL designs into database application software.   

Acknowledgement: We would like to thank our DAIDA colleagues, in particular  
M. Jarke, F. Matthes, and M. Mertikas, for their contributions to this 
research.

\section*{Appendix}

%TDLDESIGN ResearchCompanies IS   
%	ENUMERATED CLASS Agencies = {'ESPRIT, 'DFG, 'NSF, ...};    
%	ENTITY CLASS Companies WITH 
%		UNIQUE, UNCHANGING name : Strings; 
%		CHANGING engagedIn : SetOf Projects; 
%	END Companies;    
%	ENTITY CLASS Employees WITH 
%		UNCHANGING  name : Strings; 
%		CHANGING  belongsTo : Companies;  worksOn : SetOf Projects; 
%		INVARIANTS onEmpComp: True Is (THIS.worksOn SubSetOf THIS.belongsTo.engagedIn); 
%	END Employees;    
%	ENTITY CLASS Projects WITH 
%		UNIQUE, UNCHANGING name : Strings; getsGrantFrom : Agencies;                        
%		CHANGING consortium : SetOf Companies; 
%		INVARIANTS onProjComp:  True Is 
%			( THIS.consortium = { EACH x IN Companies : THIS IsIn x.engagedIn } ); 
%	END Projects;    
%	TRANSACTION HireEmployee WITH 
%		IN name : Strings; belongs : Companies; works : SetOf Project; 
%		OUT, PRODUCES e : Employee;     
%		GIVEN works  SubSetOf  belongs.engagedIn;
%		GOALS  (e.name« = name) AND (e.worksOn« = works) AND (e.belongsTo« = belongs) 
%	END HireEmployee ;   
%END ResearchCompanies; 
%
{\sl\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill
TDLDESIGN ResearchCompanies IS \\[0.8ex]
\> ENUMERATED CLASS Agencies = \{`ESPRIT, `DFG, `NSF, \dots\}; \\[0.8ex]
\> ENTITY CLASS Companies WITH \\
\>\> UNIQUE, UNCHANGING 
name : Strings; \\
\>\> CHANGING
engagedIn : \SetOf Projects; \\
\> END Companies; \\[0.8ex]
\> ENTITY CLASS Employees WITH \\
\>\>  UNCHANGING 
name : Strings; \\
\>\>   CHANGING   
belongsTo : Companies; 
worksOn : \SetOf Projects; \\
\>\> INVARIANTS onEmpComp: True IS (\THIS.worksOn \SubSetOf \THIS.belongsTo.engagedIn); \\
\> END Employees; \\[0.8ex]
\> ENTITY CLASS Projects WITH \\
\>\> UNIQUE, UNCHANGING 
name : Strings; 
getsGrantFrom : Agencies; \\                       
\>\> CHANGING   
consortium : \SetOf Companies; \\
\>\> INVARIANTS onProjComp: \\
\>\>\>True Is (\THIS.consortium = 
\{\EACH x \IN Companies :  \THIS \IsIn x.engagedIn\}); \\
\> END Projects; \\[0.8ex]
\> TRANSACTION HireEmployee WITH \\
\>\> IN	name : Strings; 
belongs : Companies; 
works : \SetOf Project; \\
\>\>OUT, PRODUCES 
e : Employees; \\    
\> \> GIVEN 
works \SubSetOf belongs.engagedIn;\\
\>\> GOALS 
(e.name' = name) \AND (e.worksOn' = works) \AND (e.belongsTo' = belongs) \\
\> END HireEmployee \\[0.8ex]
END ResearchCompanies;\\ 
\end{tabbing}}
\nobreak
\fig{1}{TDL Design of the ResearchCompanies Example}

\bigbreak

{\sl\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\=\kill
DEFINITION MODULE ResearchCompaniesTypes; \\ [0.8ex]  
\> IMPORT Identifier,String;\\[0.8ex]
\> TYPE\\
\> \> Agencies = (ESPRIT, DFG, NSF, ..);\\
\> \> CompNames, EmpNames,ProjNames = String.Type;\\
\> \> EmpIds = Identifier.Type;\\
\> \> ProjIdRecType = RECORD 
		name : ProjNames; getsGrantFrom : Agencies
		END;\\
\> \> ProjIdRelType = RELATION OF ProjIdRecType; \\[0.8ex]
\>\> CompRelType = RELATION 
               name OF \\
\>\>\>\>\>\>\> RECORD 
                     name : CompNames;
                    engagedIn : ProjIdRelType
                   END;   \\
\> \> EmpRelType = RELATION employee OF \\
\>\>\>\>\>\>\> RECORD 
employee : EmpIds; name : EmpNames;\\
\>\>\>\>\>\>\>\>\> belongsTo : CompNames; worksOn : ProjIdRelType
END;\\
\> \> ProjRelType = RELATION projId OF \\
\>\>\>\>\>\>\> RECORD projId : ProjIdRecType; 
   consortium : RELATION OF CompNames END;\\ [0.8ex]  
END ResearchCompaniesTypes. \\    
\\
DEFINITION MODULE ResearchCompaniesOps; \\[0.8ex]   
\> FROM ResearchCompaniesTypes IMPORT EmpNames, CompNames, ProjIdRelType, 
   EmpIds;\\  [0.8ex]  
\> TRANSACTION HireEmployee(name:EmpNames;belongs:CompNames;
 works:ProjIdRelType) : EmpIds;\\ [0.8ex]  
END ResearchCompaniesOps. 
\end{tabbing}}


{\sl\begin{tabbing}            
xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill
DATABASE IMPLEMENTATION MODULE ResearchCompaniesOps; \\ [0.8ex]
\> FROM ResearchCompaniesTypes IMPORT 
CompRelType; EmpRelType; ProjRelType; \\[0.8ex]  
\> IMPORT Identifier;\\[0.8ex]
\> VAR  compRel : CompRelType;\\
\> \>\> empRel : EmpRelType; \\
\> \>\> projRel : ProjRelType;\\[0.8ex]
\> TRANSACTION HireEmployee
(name:EmpNames;belongs:CompNames; works:ProjIdRelType) : EmpIds;\\
\>\> VAR tEmpId : EmpIds;\\
\>\> BEGIN\\
\>\>\>IF SOME c IN compRel (c.name = belongs) AND\\
\>\>\>\> ALL w IN works 
  (SOME p IN compRel[belongs].engagedIn (w = p))\\
\> \> \> 	THEN  tEmpId := Identifier.New; \\
\> \>\>\>     	empRel :+ 				
			EmpRelType\{\{tEmpId,name,belongs,works\}\};\\
\> \>\>\>		RETURN tEmpId    \\
\> \> \>	ELSE RETURN Identifier.Nil\\
\> \> \>  	END \\
\> \>END HireEmployee;\\[0.8ex]
END ResearchCompaniesOps.\\
\end{tabbing}}
%
% DEFINITION MODULE ResearchCompaniesTypes;     
%	IMPORT Identifier,String;   
%	TYPE Agencies = (ESPRIT, DFG, NSF, ..);
%		CompNames, EmpNames,ProjNames = String.Type;
%		EmpIds = Identifier.Type;
%		ProjIdRecType = RECORD name : ProjNames; getsGrantFrom : Agencies END;
%		ProjIdRelType = RELATION OF ProjIdRecType;    
%		CompRelType = RELATION  name OF 
%						RECORD name : CompNames; engagedIn : ProjIdRelType END;   
%		EmpRelType = RELATION employee OF RECORD employee : EmpIds; name : EmpNames; 		
%								belongsTo : CompNames; worksOn : ProjIdRelType END;
%		ProjRelType = RELATION projId OF RECORD projId : ProjIdRecType; 
%									consortium : RELATION OF CompNames END;
%END ResearchCompaniesTypes.
%
%DEFINITION MODULE ResearchCompaniesOps;  
%	FROM ResearchCompaniesTypes IMPORT EmpNames, CompNames, ProjIdRelType, EmpIds;  
%	TRANSACTION HireEmployee(name: EmpNames; belongs: CompNames; 
%							works: ProjIdRelType) : EmpIds;
%END ResearchCompaniesOps.
%
%DATABASE IMPLEMENTATION MODULE ResearchCompaniesOps;     
%	FROM ResearchCompaniesTypes IMPORT CompRelType; EmpRelType; ProjRelType; 
%	IMPORT Identifier;   
%	VAR  compRel : CompRelType; empRel : EmpRelType; projRel : ProjRelType;   
%	TRANSACTION HireEmployee(name:EmpNames; belongs:CompNames; 
%					works:ProjIdRelType) : EmpIds;
%		VAR tEmpId : EmpIds;
%	BEGIN
%		IF SOME c IN compRel (c.name = belongs) AND 
%				ALL w IN works(SOME p IN compRel[belongs].engagedIn (w = p))
%		THEN  tEmpId := Identifier.New; 
%				empRel :+ EmpRelType{{tEmpId,name,belongs,works}};
%				RETURN tEmpId    
%		ELSE  RETURN Identifier.Nil
%		END 
%	END HireEmployee;   
%END ResearchCompaniesOps.
%
\fig{2}{DBPL Implementation of the ResearchCompanies Example}


\begin{thebibliography}{99.}

\bibitem{Formal}
Abrial, J. R.,
{\em Formal Construction of an Order System}, 
26 Rue des Plantes, Paris 75014, 
May 1988.

\bibitem{Set}
Abrial, J. R.,
{\em Introduction to Set Notations},
Parts 1,2, 26 Rue des Plantes, Paris 75014, 
June 1988.                         

%[3]
\bibitem{Abstract}
Abrial, J. R., P. Gardiner, C. Morgan, and M. Spivey,
{\em Abstract Machines}, 
Part1 - Part4, 26 Rue des Plantes, Paris 75014, 
June 1988.

%[4]
\bibitem{B}
Abrial, J. R.,  C. Morgan, M. Spivey, and T.N. Vickers,
{\em The Logic of  `B' },
26 Rue des Plantes, Paris 75014, 
September 1988.      

%[5]
\bibitem{Dialogue}
J. Barron, 
{\em Dialogue and process design for Interactive Information Systems},
ACM SIGOA Conf. Proc., Philadelphia, 
June 1982.

%[6]
\bibitem{Language}
Borgida, A., 
{\em Language Features for Flexible Handling of  Exceptions},
ACM Trans. on Database Systems 10(4), pp.565-603.

%[7]
\bibitem{software}
Borgida, A., Jarke, M., Mylopoulos, J., Schmidt, J., and Vassiliou, Y.,
{\em The software development environment as a knowledge base management 
system},
In: Schmidt, J.W., Thanos, C. (eds).,
{\em  Foundations of Knowledge Base Management}, 
Springer  Verlag, 
(to appear 1989).

%[8]
\bibitem{Knowledge}
Borgida, A.,  Greenspan, S., and Mylopoulos, J.,
{\em Knowledge  representation as a basis for requirements},
IEEE Computer Vol.18, No.4, pp.82-103,
April 1985.

%[9]
\bibitem{General}
Borgida, A., J.Mylopoulos, and H.K.T.Wong,
{\em Generalization/Specialization as a basis for software specification},
In: Brodie, M.L., Mylopoulos, J. and J.W. Schmidt, (eds). 
{\em On Conceptual Modelling, Springer-Verlag},
1984.


%[10]
\bibitem{Conceptual}
Borgida, A., Mylopoulos, J., Schmidt, J.W., and Wetzel, I.
{\em Support for Data-Intensive Applications: Conceptual Design and Software 
Development},
Proc. 2nd Intl. Workshop on Database Programming Languages, 
Morgan Kaufmann 
(to appear in 1989).
                   
%[11]
\bibitem{AKnowledge}
Borgida, A., M. Koubarakis, J. Mylopoulos, and M. Stanley,Telos:
{\em A Knowledge Representation Language for Requirements Modeling},
Technical Report KRR-TR-89-4, Dept. of Computer Science, University of Toronto, 
February 1989.

%[12]
\bibitem{Extended}
K.L.Chung, 
{\em An Extended Taxis Compiler},
M.Sc thesis, Dept. of  Computer Science, University of Toronto, 
January 1984.

%[13]
\bibitem{DAIDA}
DAIDA, 
{\em Final Version on TDL Design}, 
ESPRIT Project 892,  DAIDA, Deliverable DES1.2,
1987.
     
%[14]
\bibitem{Larch}
Guttag, J., J.J. Horning, and J.W. Wing, 
{\em Larch in five easy pieces}, 
TR 5, DEC Systems Research Center, 
1985.

%[15]
\bibitem{Specification}
Hayes, I. (editor), 
{\em Specification Case Studies}, 
Prentice Hall  International, Englewood Cliffs NJ, 
1987.

%[16]
\bibitem{Data}
Matthes, F., A. Rudloff, and J.W. Schmidt.
{\em Data- and Rule-Based Database Programming in DBPL},
Esprit Project 892, DAIDA, Deliverable IMP 3.b, 
March 1989.

%[17]
\bibitem{Alanguage}
Mylopoulos, J., P. Bernstein, and H. Wong,
{\em A language facility for designing data-intensive applications},  
ACM TODS 5(2),  
June 1980.

%[18]
\bibitem{Some}
Schmidt, J.W.,
{\em Some High Level Language Constructs for Data of Type Relation},
ACM Transactions on Database Systems, 2(3), 
September 1977.

%[19]
\bibitem{DBPL}
Schmidt, J.W., H. Eckhardt, and F. Matthes,
{\em DBPL Report},
DBPL-Memo 111-88, Fachb. Informatik, Johann Wolfgang Goethe-Universität, 
Frankfurt, West Germany, 
1988.
        
%[20]
\bibitem{Abstraction}
Schmidt, J.W. and M. Mall,
{\em Abstraction mechanisms for database programming},
Proc. ACM SIGPLAN Notices, 18:6, pp. 83-93, 
1983.

%[21]
\bibitem{Z}
Spivey, J.M., 
{\em The Z Notation Reference Manual}, 
Prog. Res. Group, Oxford University, 
1987.

%[22]
\bibitem{Specandver}
Stemple, D. and T. Sheard,
{\em Specification and verification of abstract database types}, 
ACM PODS Conference, Waterloo, Ontario, pp.248-257, 
April 1984.

%[23]
\bibitem{Modula2}
Wirth, N.,
{\em Programming in Modula-2},
Springer-Verlag, 
1983.

%[24]
\bibitem{AZ}
Wordsworth, J.B.,
{\em A Z Development Method},
IBM UK Lab Ltd., Winchester,
1987.

\end{thebibliography}

\end{document}
