\documentstyle[lncs]{article}
%\parindent0em
%\mathindent0.75cm
%\pagestyle{headings}
\renewcommand{\labelenumi}{(\roman{enumi})}
\newtheorem{satz}{Proposition}[section]
\newtheorem{definition}{Definition}[section]
\newtheorem{lemma}{Lemma}[section]
\newtheorem{theorem}{Theorem}[section]
\newtheorem{beispiel}{Example}[section]
\newtheorem{folgerung}{Corollary}[section]
\newtheorem{vermutung}{Conjecture}[section]

\newfont{\itsl}{cmbxsl10 scaled 1000}
\def\parfun{\raisebox{.3ex}{\tiny{$\longrightarrow \!\!\!\!\!\!\! \mid$}} $\;\;\,$}
\def\subst{\raisebox{.3ex}{\tiny{$\mid$}}$\!$\normalsize{$\leftarrow \;$}}
\def\substm{\;\raisebox{.3ex}{\tiny{$\mid$}}\!\normalsize{\leftarrow \;}}

\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{{\itsl each}\ }
\def\OF{{\itsl of}\ }
\def\IN{{\itsl in}\ }
\def\IsIn{\ {\itsl isIn}\ }
\def\SubSetOf{{\itsl subsetOf}\ }
\def\THIS{{\itsl this}}
\def\ALL{ {\itsl all}\ }
\def\AND{ {\itsl and}\ }
\def\NOT{{\itsl not}\ }
\def\OR{{\itsl or}\ }
\def\ADDED{{\itsl Added}\ }
\def\REMOVED{{\itsl Removed}\ }
\def\NEW{{\itsl New}}

\def\fig#1#2{
{ \centerline{{\it Fig. #1:} #2} }}

\renewcommand{\labelenumi}{(\roman{enumi})}
\begin{document}

\title{\Large\bf Specification and Refinment in an\\Integrated Database Application Environment\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{Ingrid Wetzel, Klaus-Dieter Schewe, Joachim W. Schmidt\\ University of
Hamburg, FRG}

\date{{\bf Draft Version}, \today}

\maketitle


\begin{abstract}

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

The DAIDA\footnote[7]{DAIDA (``Development of Advanced Interactive Data-intensive Applications'') is an ESPRIT project funded by the E.E.C under research contract 892.} project developed a layered design architecture for data-intensive applications, in which the transformation of a conceptual design to an efficient implementation is realized by stepwise refinement using Abrial's framework of Abstract Machines. One of the key contributions of DAIDA is the development of a mapping technology from an extended object-oriented, constraint-based specification language to an integrated, efficient database programming language based on sets and first-order predicates. This paper reviews the experiences made with this approach and derives requirements for formal specification languages tailored to data-intensive applications.

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

\end{abstract}


\section{Introduction}


The specification of data-intensive information systems is dominated by the attempt to model
application domains that can be viewed 
in terms of objects and their relationships developing over time and restricted
by numerous constraints. The complexity of the
programs (transactions) may be small but the data upon which they act are 
very large, long lived, sharable by many programs, and subject to
numerous rules of consistency. These requirements result directly from the fact that databases serve as (partial) representations of some organizational unit or physical structure that exist in their own constraining context and on their own time-scale independent of any computer system. Hence, in contrast to applications like numerics or graphics, the emphasis is on consistency preservation.

\par

The DAIDA project developed a three-layer architecture that relates knowledge-based requirements modeling, conceptual software design and efficient database application programming. The highest layer handles requirements modeling followed by a layer for conceptual design an an implementation layer.

\par


For each of these layers we used a specific language:

\begin{itemize}

\item

the knowledge representation language {\bf TELOS} \cite{telos} for requirements modeling,

\item

the semantic data and transaction language {\bf TDL} \cite{tdl} for conceptual design and

\item

the database programming language {\bf DBPL} \cite{dbpl} for implementation.

\end{itemize}

After the elaboration of a satisfiable requirements model, the task is to map those parts that shall be implemented down to a conceptual design. In DAIDA this is done via a goal-driven, dependency-based mapping assistent \cite{map}. This conceptual design must be the object of further refinements that lead to an efficient database implementation. In DAIDA we used a second mapping assistant based on formal specifications and stepwise refinement in Abstract Machines \cite{daida}.
It was the explicit specification of states space and transitions that led us to the decision to use Abstract Machines. The main focus of this paper is to review this mapping from conceptual design to implementation.

\par

In section \ref{languages} we give a short summary of the languages used by DAIDA. In section 3 we describe in detail our formal specification approach based on Abrial's Abstract Machines. Section \ref{refinements} illustrates standard refinement steps that were used in DAIDA and that are based on a computational model tailored to data-intensive applications. We conclude with an outline of the experiences we made in the project with formal method application.

\section{The DAIDA Languages}

\label{languages}
We present an object oriented way of describing the design of a database
application by using the language TDL \cite{tdl} and the main aspects of the implementation language DBPL \cite{dbpl}. 

\subsection{The Conceptual Design Language TDL}


TDL is a language that describes data as classes of objects related by attributes. Database states correspond to the extent of these data classes. 
A variety of different data classes is supported: Basic Classes, Enumerated Classes, Aggregate Classes and Entity Classes. Basic Classes and Enumerated Classes are used to model simple value sets. In general however, the structure of values in TDL can be complex. Values denoting tuples of other values are modelled by {\sl AggregateClasses}. Entities in the application domain 
are modelled by
{\em EntityClasses}. Specific integrity constraints may be assigned to 
the attributes of Entity Classes such as attribute categories, range constraints, initial/final conditions and general invariants.

\par

Attribute categories can be used to characterize the values of an object to be (un)changing during the object's lifetime or unique within the class. Range restrictions require the values of the attribute to belong to some other class. Initial/final conditions specify conditions on new objects or on objects to be deleted.

\par

Atomic state transitions are modelled as instances of {\sl TransactionClasses},
where the input/output of a transaction and its actions is described by
appropriate attributes and logical formulas. The body of a transaction is specified using the familiar precondition/postcondition and used also in the formal specification language 'Z' \cite{z1} \cite{z2} \cite{schu}. Preconditions are given via the keyword $GIVEN$, whereas postconditions require the keyword $GOALS$. In opposite to Z only those changes are expressed that are caused by the transaction, it is implicitly assured that everything else remains unchanged -- the ``frame assuption''. 

\par

{\sl Inheritance} is supported for data classes as well as for
transaction classes, allowing the organization of objects and the reuse
of transaction specifications. 


\par

We give the TDL description for a small database example dealing with project 
management:

\par

{\sl\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill
TDLDESIGN ResearchCompanies IS \\
\> 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 onEmpProj: True IS \\
\>\>\>\>(\ THIS.worksOn \ $\subseteq$ \ 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 $\in$ x.engagedIn\}); \\
\> END Projects; \\ [0.8ex]
\> TRANSACTION CLASS HireEmployee WITH \\
\>\> IN	name : Strings; belongs : Companies; works : \ SetOf Project; \\
\>\>OUT, PRODUCES e: Employees;   \\
\>\> GOALS (e'.name = name) \ AND (e'.worksOn = works) \ AND \\
\>\>\>\>(e'.belongsTo = belongs); \\
\> END HireEmployee; \\
END ResearchCompanies; 
\end{tabbing}}

\par

Briefly summarized, TDL is a language for describing the management of data
maintained as {\it classes of objects related by attributes}.  The state
of the database is reflected by the extents of the classes, and the
values of objects' attributes, which are subject to certain integrity
constraints. {\it Transactions} are atomic state changes. TDL also
introduces   {\it functions} to aid in the expression of assertions,
 {\it scripts} to aid the description of global control  constraints
and {\it communication} facilities to support the frequent needs of
Information Systems for message passing, coordination and timing
constraints.


\subsection{The Implementation Language DBPL}

\par

The database programming language DBPL \cite{dbpl} integrates a set- and
predicate-oriented view of database modelling into the system
programming language Modula-2. Based on integrated programming
language and database technology, it offers a uniform framework
for the efficiency-oriented implementation of data-intensive applications. 

\par

A central design issue of DBPL was the development of abstraction mechanisms
for database application programming. 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. 

\par

The main extensions of DBPL with respect to Modula-2 are the following:
\begin{itemize}
\item DBPL provides a new data type relation which allows to introduce relational database modelling to be coupled with the expressiveness of the programming language.
\item The new datatype is orthogonal to the existing types of Modula-2, hence sets of arrays, arrays of relations, records of relations, etc. can be modelled.
\item Complex access expressions as usual in relational databases allow to abstract from iteration.
\item All modules can be qualified to be database modules, which tunes the variables in them to be persistent and shared.
\item Specific procedures are characterized to be transactions denoting atomic state change on persistent data. Therefore, DBPL provides mechanisms for controlled concurrent access to such data and for redovery.
\end{itemize}
Let us now illustrate the simple TDL-example above in DBPL notation:


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

{\sl\begin{tabbing}            
xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill
DATABASE IMPLEMENTATION MODULE ResearchCompaniesModule; \\ [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.compName = 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}}

\fig{1}{DBPL implementation of the ResearchCompanies example}
                          


\section{The Formal Basis of the Mapping Assistant}

Within the DAIDA project the major effort concentrated on the production of high-quality database application systems. This comprises to guide users in mapping TDL-designs to DBPL-implementations:
\begin{itemize}

\item 

for a given TDL-design there are 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; 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 that should be recorded to support 
overall product consistency and evolution.

\end{itemize}                                   

To meet the above requirements requires formal methods. In DAIDA we have chosen Abrial's Abstract Machines \cite{abrial} as a formal basis for the mapping and the B-Tool for the verification of proof obligations.

\subsection{The Abstract Machine Formalism}

An Abstract
Machine specification consists of two components, namely its  state space
specification, and its state transition specification.

\subsubsection{The Static Component of an Abstract Machine}

The specification of a state space is given 
by a list of variable names, called the {\bf state variables} and by a list of well-founded formulas of a many-sorted first-order language $\cal L$ called the {\bf invariant} and denoted by $\cal I$. Free variables occurring in $\cal I$ must be state variables. Each state variable belongs to a unique basic set which has to be declared in some context. Hence, in order to complete the state space specification we must give a list of {\bf Contexts} that can be seen by the machine.

Such a context is defined by

\begin{itemize}

\item a list of {\bf basic sets},

\item a list of {\bf constant names},

\item and a list of closed formulas over the language $\cal L$ called {\bf properties}.

\end{itemize}

A basic set may be either the set of natural numbers, an abstract set given only by its name, a set given by the enumeration of its elements or a constructed set, where cartesian product, powerset and partial function space are the only allowed constructors. We may then assume to have a fixed preinterpretation of these sorts by sets.


\paragraph{The Language of States} 

The language $\cal L$ associated with an Abstract Machine can then easily be formalized.

The basic sorts of $\cal L$ are NAT and the other non-constructed basic sorts. The set of sorts is recursively defined using the basic sorts and the sort constructors $pow$, $\times$, $\mapsto$ denoting powerset construction, cartesian products and partial functions.

Since we use a fixed preinterpretation of the sorts as sets, one may regard the elements of these sets as constant symbols in $\cal L$ of the corresponding sort. Other function symbols are given by the usual functions +, * on NAT, $\cup$, $\cap$, $\setminus$ on powersets or by the constant declarations in some context. The terms and formulas in $\cal L$ are defined in the usual way. The semantics of $\cal L$ is given by an interpretation (${\cal A}, \sigma$), where $\cal A$ is a structure extending the preinterpretation on sorts and $\sigma$ is a variable binding.

We assume $\cal A$ to be fixed and write $\models_{\sigma}\cal R$, iff $\cal R$ is true under the interpretation (${\cal A}, \sigma$).

Then the state space of an Abstract Machine with state variables $x_1, ..., x_n$ is semantically denoted by the set
\begin{eqnarray*}
\Sigma &=& \{\sigma :\{x_1, ..,x_n\} \rightarrow {\cal D} \mid \sigma(x_i) \in D_{s_i} \;for\;\; all\;\; i\},
\end{eqnarray*}
where each $s_i$ is the sort of the variable $x_i$ and $\cal D$ denotes the union of the sets ${\cal D}_s$.

A wff $\cal R$ of $\cal L$ such that the free variables of $\cal R$ are state variables denotes a subset of $\Sigma$, namely 
\begin{eqnarray*}
\Sigma_{\cal R} &=& \{\sigma \mid \models_{\sigma} {\cal R} \}.
\end{eqnarray*}
Hence the invariant serves as a means to distinguish legal states in $\Sigma_I$ from others.

\paragraph{Preinterpretation $\cal A$ of Sorts}
Since natural numbers and arbitrary denumerable sets are unique (up to isomorphism) there is no loss of generality to assume this preinterpretation ${\cal A}$ of sorts being fixed.

Now let ${\cal A}$ be a preinterpretation of the sorts. ${\cal A}$ assigns to each sort $s$ a set ${\cal A }(s) = {\cal D}_s$ in the following way:
\begin{itemize}
\item ${\cal A}(NAT)$ is the usual set of natural numbers,
\item for each basic sort $s$ ${\cal A}(s)$ is some denumerable set such that the sets assigned to basic sorts are mutually disjoint, and
\item constructed sorts are carried over canonically to the corresponding set construction.
\end{itemize}


The semantics of $\cal L$ is given by an {\bf interpretation} ($\cal
A,\sigma$) consisting of a {\bf structure} $\cal A$ and a {\bf variable binding} $\sigma$.
The structure $\cal A$ gives a denotation of the sorts of the language and of the other
language parameters, i.e. the predicate-, function- and constant-symbols. A
structure  consists of the following: 

\begin{enumerate}

\item 

$\cal A$ assigns to each sort $s$ the set $D_s$. Moreover, it assigns each constant symbol $c^s$ to itself.

\item 

The sort-constructors $pow$, $\times$ and $\mapsto$ are assigned their usual
set-theoretic meaning of powersets, cartesian products and partial functions.\\ 

\item 

The same
holds for the functions $\cup$, $\cap$ and $\setminus$ on $pow(s)$. The function +, *, $\setminus$ are assigned their usual meaning on NAT.
\item 

Each function symbol $f$ of sort $(s_0, \ldots ,s_n)$ is assigned to a function

\begin{displaymath}
f^{\cal A} : D_{s_0} \times \ldots \times D_{s_{n-1}} \rightarrow D_{s_n} \; .
\end{displaymath}

\item 

$\cal A$ assigns to the predicate symbols $\in , \subseteq $ their usual set-theoretic
meaning, and $=$ denotes equality.

\end{enumerate}


In order to define the truth of a well-formed formula we have to introduce the concept of
variable-assignment.
A typed variable-assignment $\sigma $ in a structure $\cal A$ is defined as follows:
For each sort $s$ a function $\sigma_s$ on the variable set $V_s$ is defined assigning 
for each $v^s \in V_s$ a domain element
in $D_s$: $\sigma_s : V_s \rightarrow D_s$. Then $\sigma$ is the collection of all
$\sigma_s$. A structure $\cal A$ together with a variable-assignment $\sigma$ is called an
{\bf interpretation} ($\cal A$,$\sigma$) of the language $\cal L$.
Given an interpretation $({\cal A}, \sigma )$, we may extend $\sigma$ in the usual way to
terms and well-formed formulas. We write $\models_{(\cal A, \sigma)}\cal R$, iff the formula $\cal R$ is true in the interpretation $(\cal A,\sigma)$.

\subsubsection{The Dynamic Component of an Abstract Machine}

The specification of state transitions is given through substitutions over the language $\cal L$. We distinguish two kinds of transitions:

\begin{itemize}

\item

The {\bf initialization} assigns initial values to each of the state variables.

\item

{\bf Transactions} update the state space.

\end{itemize}

Both kinds of state transitions are specified using the
substitutions introduced by Dijkstra \cite{dij-old} \cite{dij} with the additional possiblity of unbounded choice:

\begin{quote}

$ @ z \bullet ( P \rightarrow  S ) $ used as an
abbreviation for an IF with an infinite list of guarded commands of the form
$P(z) \rightarrow S(z)$, i.e. select any value for $z$ such that $P$ is true
and execute the operation $S^\prime$  resulting from $S$ by replacement of all
free occurrences of $z$ in $S$ by the selected value. Clearly, if such a
value for $z$ does not exist, the @-substitution fails to terminate.

\end{quote}

\par

The semantics of substitutions $S$ is given by means of two specific
predicate transformers\footnote{By abuse of notation, wffs in $\cal L$ are simply called predicates.} $wlp(S)$ and $wp(S)$\footnote{Note that we use different interpretations than J.-R.~Abrial, P.~Gardiner and
C.~Morgan \cite{abrial} \cite{cm} for the pure guarded command
and for the @-substitution, since we do not want to dispense with Dijkstra's
Law of excluded miracles \cite{dij}.}, which satisfy the {\it pairing condition}, i.e. for all predicates $\cal R$

\begin{displaymath}
wp(S)({\cal R}) \; \equiv \; wlp(S)({\cal R}) \, \wedge \, wp(S)(true)
\end{displaymath}

and the {\it conjunctivity condition}, which states for any family ${(R_i)}_{i \in I}$ of predicates

\begin{displaymath}
wlp(S)(\forall i \in I . \, R_i) \; \equiv \; \forall i \in I . \, wlp(S)(R_i) \; .
\end{displaymath}

These conditions imply the conjunctivity of $wp(S)$ over non-empty families of predicates. As usual $wlp(S)$ will be called the {\bf weakest liberal precondition} of $S$, and $wp(S)$ will be called the {\bf weakest precondition} of $S$. The notation $f^*$, which we shall use later, denotes the {\bf conjugate predicate transformer} of $f$. It is defined by 

\[ f^*({\cal R}) \; \equiv \; \neg \, f(\neg {\cal R}) \; . \]

The definitions of $wlp(S)$ and $wp(S)$ for all the substitutions
that we allow are given in \cite{dij} or can be easily derived from there. For more details see \cite{pisa}.

\par

In addition to the properties stated above we have for any substitution $S$

\[ wp(S)(false) \; \equiv \; false \; .\]

This is the hard discussed {\bf Law of Excluded Miracles}. The related work by the PRG group \cite{cm} and by J.-R.~Abrial dispenses with this law. The main reason not to follow them is that we do not see any need for miracles. A more detailed discussion on the consequences implied by the introduction of miracles can be found in \cite{struct}.

\paragraph{Semantics of Substitutions}

Now we may associate a set-theoretic meaning to the substitutions of an Abstract Machine in terms of the state space.

For this purpose we introduce the {\bf characteristic predicate} $P_{\sigma}$ of a state $\sigma \in \Sigma$ as 
\begin{eqnarray*}
P_{\sigma} &\equiv& x_1 = \sigma(x_a) \wedge \cdots \wedge x_n = \sigma(x_n).
\end{eqnarray*}
Characteristic predicates have only one model, i.e.
\begin{eqnarray*}
\Sigma_{P_{\sigma}} &=& \{\sigma\}.
\end{eqnarray*}
Then we may associate with a substitution $S$ the following set of state pairs
\begin{eqnarray*}
\Delta(S) &=& \{(\sigma_1,\sigma_2) \in \Sigma \times \Sigma \mid \models_{\sigma_1} wlp(S)*(P_{\sigma_2})\}.
\end{eqnarray*}
Since $wlp(S)*(P{\sigma_2})$ characterizes the states $\sigma_1$ such that there exists a computation of $S$ in $\sigma_1$ leading to $\sigma_2$, $\Delta(S)$ describes the set of possible state transitions on $\Sigma$ under control of $S$.

In addition, we need to know the subset of $\Sigma$ that allows some computation of $S$ not to terminate, this is given by

\begin{eqnarray*}
\Sigma(S) &=& \{\sigma \in \Sigma \mid \models_{\sigma} wp(S)*(false)\}.
\end{eqnarray*}

Summarizing, the set-theoretic semantics for substitutions is captured by a pair of assignement functions $(\Delta, \Sigma_{trm})$, with signature 

\begin{eqnarray*}
\Delta &:& S \rightarrow pow(\Sigma \times \Sigma)\;\; and\\
\Sigma_0 &:& S \rightarrow pow(\Sigma).
\end{eqnarray*}

Then the global semantics of an Abstract Machine can be given in terms of traces on $\Sigma$, i.e. a set of finite of infinite sequences $\sigma = \sigma_o, \sigma_1, \sigma_2, \cdots$ of states $\sigma_i \in \Sigma$ such that the following conditions are satisfied:

\begin{enumerate}

\item 

for all $\sigma_{-1} \in \Sigma$ we have $(\sigma_{-1},\sigma_0) \in \Delta(S_0)$, where $S_0$ is the initialization,

\item 

for each $i > 0$ there is a transaction in $S$ with $(\sigma_{i-1},\sigma_i) \in \Delta(S)$,

\item if $t = \sigma_0, \sigma_1, \cdots, \sigma_n$ is finite, then there is a transaction $S$ with $\sigma_n \in \Sigma_0(S)$.

\end{enumerate}

\subsection{Verification}

In the following we describe which properties must be verified to assure thransaction consistency and correct refinement. Then we indicate how to use a mechanical theorem proving assistant to guide the proofs.

\subsubsection{Transaction Consistency Proof Obligation}

The invariant component of an Abstract
Machine states properties defining the set of legal states.
Therefore, it is necessary to check that the
transactions of the
Abstract Machine always preserve the
invariant.

\par

In fact, if $S$ is a transaction, it should be sufficient to require
each terminating execution starting from a state satisfying the invariant $\cal I$ to result
also in a state satisfying $\cal I$. As to the initialization $S_0$, we should
require that any computation results in a state satisfying $\cal I$ no
matter which was the initial state. Hence the following formal definition.


\begin{definition}[Consistency]

\label{cons}

Let $M$ be an Abstract Machine with invariant $\cal I$. 

\begin{enumerate}

\item

A substitution $S$ in $M$ is {\bf consistent} $\cal I$ iff
${\cal I} \; \Rightarrow \; wlp(S)({\cal I}) \;$ .

\item

$M$ is {\bf consistent} iff all transactions $S$ in $M$ are consistent with respect to $\cal I$ and the initialization 
$S_0 $ satisfies $wp(S_0)({\cal I})$.

\end{enumerate}

\end{definition}


\subsubsection{Refinement}

Refinement is used as a means to map specifications down
to implementations. This includes refining the operations
as well as transforming the state space into a more
suitable form. We shall first address operational refinement.

\par

The intention behind refinement of an operation {\it S} is
to eliminate step by step all non-terminating computations
 under control of {\it S} and to cancel some of the non-deterministic computations. Moreover, the remaining
computations of {\it S} should establish
at least the same final states.

\par

These considerations lead to the
following formal definition:

\begin{definition}[Operational Refinement]

\label{Ref-Def}

 Let {\it S} and {\it T} be two
substitutions on the same state variables. Then {\it T}
{\bf refines} {\it S} iff the following three conditions
hold for all predicates $\cal R$:

\begin{enumerate}

\item

$wlp(S)^*(true) \Longrightarrow wlp(T)^*(true) $

\item

 $wlp(S)^*(true) \Longrightarrow ( wlp(S)({\cal R})
\Rightarrow wlp(T)({\cal R} )) $

\item

 $wp(S)({\cal R}) \Longrightarrow wp(T)({\cal R}) $

\end{enumerate}

\end{definition}

We shall now give another form of these proof
obligations that do not require a universal quantification over predicates.

\begin{satz}[Normal Form Proof Obligation]

\label{nf-ref}

Let $S$ and $T$ be substitutions with state variables $x_1 , \ldots ,x_n$.
Let $z_1 , \ldots ,z_n$ be another bunch of variable names such that the $x_i$
and the $z_j$ are mutually different. Let $x$ and $z$ be the usual
abbreviations for these bunches of variables. Then $T$ refines $S$ iff:

\begin{enumerate}

\item

$(z = x) \, \wedge \, wlp(S)^*(true) \Longrightarrow wlp(T)^*(true) \wedge
wlp(\{ x/z \}.T)(wlp(S)^*(z = x)) $ and

\item

$(z = x) \, \wedge \, wp(S)(true) \Longrightarrow wp(T)(true) $

\end{enumerate}

\end{satz}

\par

As to data refinement, the usual approach taken by \cite{abrial} \cite{cm} is to use an abstract predicate $\cal A$ involving the
state variables of both the substitutions of $S$ and $T$. Assume that these
state variables are mutually different. According to proposition
\ref{nf-ref} we define in this spirit:

\begin{definition}

Let $M$, $N$ be Abstract Machines with mutually different state variables $x$
and $z$. Let $\cal A$ be some predicate on $x$ and $z$. Then $N$ {\bf refines}
$M$ iff there is a bijection $\sigma$ from the transactions of $M$ to those of
$N$ such that for all pairs $S$, $T = \sigma (S) $ of transactions we have:

\begin{enumerate}

\item

$ {\cal A} \, \wedge \, wlp(S)^*(true) \; \Longrightarrow \; wlp(T)^*(true)
\, \wedge \, wlp(T)(wlp(S)^*({\cal A})) $ and

\item

${\cal A} \; \wedge \; wp(S)(true) \; \Longrightarrow \; wp(T)(true) $.

\end{enumerate}

\end{definition}

Syntactically, the abstraction predicate $\cal A $ is used in data refinement is added to the specification of the refined machine $N$ using the additional keyword $CHANGE$.

\subsubsection{The B Proof Assistent}

The B-Tool is a general proof assistant and uses a goal-oriented proof 
technique based on Gentzen's calculi.  The built-in logic performs simple and 
multiple substitution and is designed to suit best the
calculus of substitutions.

\par


For the practical work with the B-Tool it is essential that proofs can be 
organized such that any unreducable goals (e.g., in lack of appropriate 
theories or in case of not provable predicates) are generated as lemmata. The 
proof of a lemma can be postponed, and the initial proof can go on. Typical 
examples of such  delayed proof obligations refer to lemmata that express 
type assertions or arithmetic properties. Therefore, as a result of 
a proof, some lemmata may be left over which, in a further step,  may be 
proven by the tool using additional theories (or by a less formal but 
convincing argument).

\par

In DAIDA the B-tool has been used for two purposes:

\begin{itemize}

\item

We used the built-in rewriting capability for a purely syntactical transformation of the TDL design into a first Abstract Machine. By this we exploited the fact that pre-post-specifications as they are used in TDL are equivalent to substitutions.

\item

We used B's capability as a theorem prover in order to prove the consistency of a machine and the refinement relation between two machines.

\end{itemize}

\section{Refinement in DAIDA}

\label{refinements}
 
The purpose of designs is the exact representation of application semantics without taking care of efficiency criteria. For this purpose the DAIDA project used the design language TDL. 

The purpose of implementations is to represent applications such that they can be executed efficiently. DBPL is a database programming language satisfying this requirement. The goal of the mapping process is to close the conceptual gap between these two layers by the exploitation of standard refinement steps.          

In order to use the Abstract Machines for this purpose we have to address three problems:

\begin{itemize}

\item 

represent designs in Abstract Machines, i.e. transform a TDL-description into an Abstract Machine,

\item

identify final specifications in Abstract Machines that can be transformed automatically into DBPL-programs, and

\item 

identify standard refinement steps within Abstract Machines that are directed towards such final specifications.

\end{itemize}




\subsection{Standard Refinement Steps}

Let us now describe a bunch of different standard refinement steps that turned out to be sufficient for the mapping task from TDL to DBPL.
                                                        
\subsubsection{Data Identification}
   
The {\sl first refinement} step in our example addresses the basic issues of {\em data identification}.
In our example it is a rather specific decision to utilize the uniqueness
constraints on properties for companies and projects for data identification.
For employees, where the application does not provide such a constraint,
we introduce an additional property, {\em empId}, for which the implementation
assures uniqueness.
The specification of the source for {\em empId} is left open, however its type
predicate guarantees already a new value each time the
operation is invoked.

For our refined Abstract Machine, 
 the above decisions
imply an additional basic set, {\em EmpIds}, and an extended 
{\sl\begin{tabbing}
xx\=xx\=xx\=xx\= \kill
CONTEXT\\ 
\>\> Companies = CompNames; Employees = EmpIds; Projects = ProjNames   
  $\times$ Agencies;  \dots 
\end{tabbing}}
The following definitions contribute to the refinement predicate and 
relate the refined representations to
the previous ones:
{\sl\begin{tabbing}
DEFINITIONS compName =   $\lambda$x. (x   $\in$ companies $\mid$ x);
  empId =   $\lambda$x. (x   $\in$ employees $\mid$ x);  \dots 
\end{tabbing}}
%there is no difference between these two functions yet they are
%different forms of identification; is there something wrong?
These definitions determine the function {\em compName} to be the identity 
function over the new representation
of companies and the newly defined function, {\em empId}, to be represented
by the elements in employees. 

In general, data identification implies the introduction of identifiers, 
the replacement of id-based references with value-based references, and 
the introduction of referential integrity 
constraints as preconditions of the operations.


\subsubsection{Operational Refinement}

Due to the change in the data representation, the operation {\em hireEmployee},
becomes less non-deterministic: the arbitrary ANY-substitution is replaced
by some operation {\em newEmpId}, that provides a new {\em EmpId}-value, 
which is then 
associated with the required properties by means of function extension:

          
{\sl\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill                

 	OPERATIONS 
    	hireEmployee (name, belongs, works)  =  \\
 \>      	PRE 
                        name   $\in$ EmpNames    $\wedge$  
                        belongs   $\in$ companies    $\wedge$  
                	works   $\in$   $pow$ (engagedIn(belongs)) \\
 \>       	THEN \\
 \> \>       (empName(newEmpId),worksOn(newEmpId),belongsTo(newEmpId))
$\mid$$\leftarrow$ (name,works,belongs) $\mid$$\mid$  \\
  \> \>        employees   $\mid$$\leftarrow$ employees   $\cup$ \{newEmpId\} 
$\mid$$\mid$
hireEmployees   $\mid$$\leftarrow$ newEmpId \\
  \>       	END hireEmployee; \\[0.8ex]
     	OTHER newEmpId $\in$ ($\rightarrow$ EmpIds - employees);
\end{tabbing}}

Our refined data and procedure representation can be proven to meet all
the invariants layed down within the initial Abstract Machine. 



\subsubsection{Data Reification}

Having decided upon the identification, we are now ready for another
step that designs the central {\em data structures} of our implementation. 
While our previous Abstract Machines have a purely functional view of the
data. We now refine to 
a representation that is 
based on Cartesian products. The newly introduced variable, e.g., {\em
empClass}, 
becomes a total function that associates employees with structured data
defined over {\em EmpNames, companies}, and sets of {\em projects}.
{\sl\begin{tabbing}
INVARIANTS empClass   $\in$ (employees   $\rightarrow$ 
     	EmpNames   $\times$ companies   $\times$   $pow$ (projects)); \dots
\end{tabbing}}
The following definitions determine the three functions from above to be
represented by the
three corresponding components returned by the single function {\em empClass}.
{\sl\begin{tabbing}
DEFINITIONS (empName, belongsTo, worksOn) 
= $\lambda$x. (x   $\in$ employees $\mid$ empClass(x)); \dots
\end{tabbing}}                                                

Another change of the representation comes from the introduction of a 
variable, {\em tEmpId}, that allows us to replace the parallel substitutions in the 
operation {\em hireEmployee} by serial ones.

An 
alternative refinement could introduce ``flat variables'':
{\sl\begin{tabbing}
VARIABLES flatCompClass, flatEmpClass, flatProjClass, empProjClass,  \dots;
\end{tabbing}}
with constraints like 
{\sl\begin{tabbing}
xx\=xx\=xx\=xx\= \kill
INVARIANTS flatEmpClass   $\in$ (employees   $\rightarrow$ 
  EmpNames   $\times$ companies); \dots\\   
\> empProjClass   $\in$ (employees $\leftrightarrow$ projects); \dots;
\end{tabbing}}
The flat representation has, of course, consequences for the 
operation, {\em hireEmployee}, which has to contain substitutions on both variables, 
{\em flatEmpClass} and {\em empProjClass}:
{\sl\begin{tabbing}
xx\=xx\=xx\=xx\= \kill
OPERATIONS hireEmployee(name,belongs,works) =  \dots;\\
\> flatEmpClass   $\mid$$\leftarrow$ flatEmpClass $\oplus$ 
  \{( tEmpId, name, belongs)\} $\mid$$\mid$\\
\> empProjClass   $\mid$$\leftarrow$ empProjClass $\oplus$ 
  inverse($\lambda$x.(x $\in$ works $\mid$ (tEmpId))) \dots
\end{tabbing}}   


The decisions for value-based identification and for sets and Cartesian products
as basic data structures were motivated by a relational 
implementation language.




   
\subsubsection{Data Typing}
      
On our way down to a relational implementation there is another 
step left that deals with {\em data typing}. Since DBPL is a strongly and 
statically
typed database programming language we want to refine the variables to become
partial functions over the {\it Basic Sets} instead of total functions
over other variables of time-varying cardinality.
This refinement step leads to a machine
with the following context, variables and invariants:
{\sl\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill
\>      CONTEXT \\
\>\>  ProjIdRecType = ProjNames $\times$ Agencies;  \\
\>\>  ProjIdRelType = $pow$ (ProjIdRecType);\\
\>\>  CompRelType = (CompNames   +$\rightarrow$ ProjIdRelType);\\
\>\>  EmpRelType = (EmpIds  +$\rightarrow$ EmpNames $\times$ 
        CompNames $\times$ ProjIdRelType);\\
\>\>  ProjRelType = (ProjIdRecType +$\rightarrow$   
        $pow$ (CompNames));\dots \\
\>	VARIABLES \\
\>\>  compRel, empRel, projRel \\
\> 	INVARIANTS    \\
\>\> compRel   $\in$ CompRelType; compRel =  compClass ; \\
\>\> empRel   $\in$ EmpRelType;   empRel  =  empClass ;\\
\>\> projRel   $\in$ ProjRelType; projRel =  projClass ;  \dots
\end{tabbing}}
In the subsequent section we will see how the context information can be transformed
into the type definitions (or schema) of a DBPL database module.

Similarly, the precondition of the {\em hire} operation is weakened to a static
constraint that will finally become the parameter types of the {\em
hireEmployee}
transaction. However, in order to imply the inherited specification we 
have to strengthen our constraints by a {\em conditional} substitution:
{\sl\begin{tabbing}                                      
xx\=xx\=xx\=xx\=xx\ \kill
IF belongs   $\in$ companies   $\wedge$
works   $\in$    $pow$ (engagedIn(belongs)) 
THEN  \dots ELSE  \dots
\end{tabbing}}
Due to the semantics of the generalized substitution, the condition will
finally result in a first-order predicate on the variables that represent
database states and transaction parameters.

Our example also demonstrates that a refined version may 
have a weaker precondition than the initial one:
{\em 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 a specific value, {\em nilEmpId}, as an exception.

Invariants and definitions of the Abstract Machine variable {\em empRel}
translate one-to-one into the type definitions of the corresponding 
DBPL variable {\em empRel}.


\subsubsection{Adding Run-Time Semantics}

In the final refinement step of {\em 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 the following first-order 
database query expression:
{\sl\begin{tabbing}
xx\=xx\=xx\=xx\=xx\= \kill
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{tabbing}}

We can see how the DBPL query expressions based on first-order predicates
nicely corresponds with substitutions.

\section{Conclusion}

\label{sum}
Within the layered DAIDA architecture formal specification and verification come into play as a means for mapping step-by-step  from conceptual designs down to  implementations. We use the formalism of Abstract Machines, since they allow to capture at the same time the semantics of TDL-designs and to introduce via refinement the procedurality required by efficiency-oriented database programs.

\par

Database applications require the conceptual specification of highly structured and interrelated data. It is the complexity of data that makes database application development a hard task, whereas most operations on the data are rather easy such as simple insert, delete and update operations. Integrity constraints on the data are normally expressed by first-order predicates. Thus, the possibility to explicitly represent  such constraints via invariants makes Abstract Machines a good choice for database application specification -- much more natural than e.g. algebraic specifications. 


\par

Moreover, most commercial database systems do not offer any sophisticated mechanism in order to prove consistency. Integrity checking is done at run-time before transaction commit. In Abstract Machines, however, we were able to prove the consistency already at specification time. Transactions are modeled via operations in Abstract Machines, and consistency is semi-automatically verified using the B proof assistent. In addition, it can be shown that most lemmata resulting during a B-tool proof can be classified into only very few classes such that in most proof situations generic proofs may be reused.

\par

Another positive experience we made with Abstract Machines is the possibility to refine a specification within one and the same language. This poses the strong requirement on formal specification languages to capture at the same time the semantics of a high-level conceptual design language and of an efficient implementation language. However, one big problem arises. Refinement in Abstract Machines as it is usually defined does only preserve the semantics of the operations, but not of the data, for which it is much too liberal. This is not better in other specification styles, since database application have not yet been the focal point of the formal specification community. Most of the work that has been done follows the line of abstract data types ignoring the fact that in database application systems the data live longer than the operations on them.

\par

Our current work is built upon the DAIDA experience preserving the style of transaction specifications.
\section*{Acknowledment}

We should like to thank J.~R.~Abrial and our colleagues in DAIDA, especially Alex Borgida, Michael Mertikas and the researchers at BP research centre, for many fruitful discussions and comments. We also want to thank Paul Gardiner from the Programming Research Group at Oxford University for interesting discussions and his contribution to the set-theoretic semantics of substitutions. 

\begin{thebibliography}{12345678}

\bibitem[Ab89]{abrial}
J.R. Abrial: {\it A Formal Approach to Large Software Construction}, in
J.L.A. van de Snepscheut (ed.): {\it Mathematics of Program Construction},
International Conference Groningen, The Netherlands, June 89, Proceedings,
LNCS 375, Springer-Verlag, 1989.

\bibitem[BMS87]{tdl} A.~Borgida, J.~Mylopoulos, J.~W.~Schmidt: {\it Final Version on
TDL Design}, DAIDA deliverable

\bibitem[BKMS89]{telos} A.~Borgida, M.~Koubarakis, J.~Mylopoulos, M.~Stanley: {\it TELOS: A Knowledge Representation Language for Requirements Modeling}, Technical Report KRR-TR-89-4, Dept. of Comp. Sci., University of Toronto, 1989

\bibitem[BMSW89]{daida} A.~Borgida, J.~Mylopoulos, J.~W.~Schmidt, I.~Wetzel: 
Support for Data-Intensive Applications: Conceptual Design and Software Development,
in {\it Proceedings of the 2nd Workshop on Database Programming Languages, Salishan
Lodge, Oregon}, june 1989

\bibitem[CKM$^+$89]{map} L.~Chung, P.~Katalagarianos, M.~Marakakis, M.~Mertikas, J.~Mylopoulos, Y.~Vassiliou: {\it From Requirements to Design: A Mapping Framework for Information Systems}, to appear in Information Systems

\bibitem[Dij76]{dij-old} E.W. Dijkstra. {\it A Discipline of Programming}.
Prentice Hall, 1976.

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

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

\bibitem[Hay87]{hayes} I. Hayes. {\it Specification Case Studies}.
Prentice Hall, 1987.

\bibitem[Heh84]{hehner} E.C.R. Hehner. {\it The Logic of Programming}.
Prentice Hall, 1984.

\bibitem[HGM86]{heh-ref} E.C.R. Hehner, L.E. Gupta und A.H. Malton, {\it
Predicative Methodology}. Lecture Outline, Marktoberdorf Summer
School, August 1986.

\bibitem[Jon86]{vdm} C.B. Jones: {\it Systematic Software Development 
using VDM}, Prentice-Hall International, London 1986.

\bibitem[MRG88]{cm} C. Morgan, K. Robinson, P. Gardiner.
{\it On the Refinement Calculus},
Technical Monograph PRG-70, Oxford University Computing Labaratory,
Oktober 1988.

\bibitem[SEM88]{dbpl} J.~W.~Schmidt, H.~Eckhardt, F.~Matthes: {\it DBPL Report},
DBPL-Memo 111-88, University of Frankfurt, 1988

\bibitem[ScPi87]{schu}
S.A. Schuman und D.H. Pitt: {\it Object--Oriented Subsystem Specification}, in
L. Meertens, (ed.): {\it Program Specifiation and Transformation,
The IFIP TC2/WG2.1 Working Conference, Bad T\"olz, FRG, April
15-17, 1986}, North Holland Publishing Co, Amsterdam, 1987.

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

\bibitem[Spi89]{z2} J.M. Spivey. {\it The Z Notation, A Reference
Manual}, Prentice
Hall, 1989.

\bibitem[Wir85]{wirsing} M. Wirsing: {\it Structured Algebraic Specifications -- A
Kernel Language}, Passau University Reports, MIP 8511, 1985

\end{thebibliography}

\appendix
\section{From TDL Designs through Abstract Machines to  
                   DBPL Implementations}
{\sl\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill
TDLDESIGN ResearchCompanies IS \\ [0.8ex]
\> BASIC CLASS CompNames, EmpNames, ProjNames = Strings; \\
\> ENUMERATED CLASS Agencies = \{`ESPRIT, `DFG, `NSF, \dots\}; \\ [0.8ex]
\> ENTITY CLASS Companies WITH \\
\>\> UNIQUE, UNCHANGING compName : CompNames; \\
\>\> CHANGING engagedIn : \SetOf Projects; \\
\> END Companies; \\   [0.8ex]
\> ENTITY CLASS Employees WITH \\
\>\>  UNCHANGING empName : EmpNames; \\
\>\>   CHANGING belongsTo : Companies; worksOn : \SetOf Projects; \\
\>\> INVARIANTS onEmpProj: True IS (\THIS.worksOn \SubSetOf \THIS.belongsTo.engagedIn); \\
\> END Employees; \\   [0.8ex]
\> ENTITY CLASS Projects WITH \\
\>\> UNIQUE, UNCHANGING projName : ProjNames; 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 : EmpNames; belongs : Companies; works : \SetOf Projects; \\
\>\>OUT, PRODUCES e: Employee;   \\
\>\> GOALS (e$'$.empName$'$ = name) \AND (e$'$.worksOn$'$ = works) \AND 
(e$'$.belongsTo$'$ = belongs); \\
\> END HireEmployee; \\ [0.8ex]
END ResearchCompanies; 
\end{tabbing}}
\nobreak                                  
\fig{1}{TDL Design of ResearchCompanies Example}
 
\newpage
          
{\sl\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill                
MACHINE researchCompanies.1\\[0.8ex]
\> BASIC SETS 
 Agencies, Companies, Employees, Projects, CompNames, 
 EmpNames, ProjNames\\[0.8ex]
\>CONTEXT 
 Agencies = \{ ESPRIT, DFG, NSF, \dots \}; \\
\>\>CompNames, EmpNames, 
 ProjNames = Strings \\[0.8ex]
\>VARIABLES companies, compName, engagedIn, \\
\>\>	employees, empName, belongsTo, worksOn, \\ 
\>\>      projects, projName, getsGrantFrom, consortium \\[0.8ex]
\>INVARIANTS companies $\in$ $\wp$(Companies);
    compName   $\in$ (companies $\rightarrow$ CompNames);\\
\>\>	engagedIn $\in$ (companies $\rightarrow$ $\wp$(projects));\\[0.8ex]
\>\>	employees   $\in$   $\wp$ (Employees); 
    empName   $\in$ (employees   $\rightarrow$ EmpNames); \\ 
\>\>	belongsTo   $\in$ (employees   $\rightarrow$ companies);
    worksOn   $\in$ (employees   $\rightarrow$   $\wp$ (projects));\\[0.8ex]
\>\>      projects $\in$ $\wp$(Projects);
   projName   $\in$ (projects $\rightarrow$ ProjNames); \\
\>\>	getsGrantFrom $\in$ (projects $\rightarrow$ Agencies);
   consortium $\in$ (projects $\rightarrow$ $\wp$(companies));\\[0.8ex]
\>\>	$\forall$x,y. x,y $\in$ companies $\Rightarrow$ (compName(x) = 
        compName(y) $\Rightarrow$ x = y);\\
\>\>	$\forall$x. x $\in$ employees $\Rightarrow$ (worksOn(x) $\subseteq$ 
engagedIn(belongsTo(x));\\
\>\>	$\forall$x,y. x,y $\in$ projects $\Rightarrow$  \\
\>\>\>  (projName(x) 
        = projName(y) $\wedge$ getsGrantFrom(x) = getsGrantFrom(y) 
         $\Rightarrow$ x = y);\\
\>\>	$\forall$x. x $\in$ projects $\Rightarrow$ (consortium(x) 
        = \{y $\mid$ y $\in$ companies $\wedge$ x $\in$ engagedIn(y)\});\\[0.8ex]
\>OPERATIONS hireEmployee (name, belongs, works)  =  \\
\>\>PRE name   $\in$ EmpNames    $\wedge$ belongs   $\in$ companies    $\wedge$ 
      works   $\in$   $\wp$ (engagedIn(belongs)) \\ 
\>\>THEN ANY e IN (e $\in$ (Employees - employees)) \\
\>\> \> THEN (empName(e), worksOn(e), belongsTo(e)) 
      \subst (name, works, belongs)  $\mid$$\mid$  \\
\>\>\>\> employees  \subst employees   $\cup$ \{e\} $\mid$$\mid$
  hireEmployee   \subst e \\
\>\>\> END \\ 
\>\> END hireEmployee;\\[0.8ex]
End researchCompanies.1;\\
\end{tabbing}}

\fig{2}{Initial Abstract Machine}

\bigskip

{\sl\begin{tabbing}
xx\=xx\=xx\=xx\= \kill
MACHINE researchCompanies.2\\[0.8ex]
\>   	IMPLY researchCompanies.1\\[0.8ex]
\>	BASIC SETS
EmpIds\\[0.8ex]
\>   	CONTEXT
Companies = CompNames;
Employees = EmpIds;
Projects = ProjNames   $\times$ Agencies\\[0.8ex]
\> 	VARIABLES 
empId, projId, tEmpId, \dots\\[0.8ex]
\> 	INVARIANTS 
empId   $\in$ (employees   $\rightarrow$ EmpIds); tEmpId $\in$ EmpIds;  \dots\\[0.8ex]
\>	DEFINITIONS
compName =   $\lambda$x.(x   $\in$ companies $\mid$ x);\\
\>\> empId =   $\lambda$x.(x   $\in$ employees $\mid$ x);\\
\>\> (projName, getsGrantFrom) = projId =  $\lambda$x.(x   $\in$ projects 
$\mid$ x); \dots\\[0.8ex]
\>  	OPERATIONS 
    	hireEmployee (name, belongs, works)  =  \\
 \> \>      	PRE 
                        name   $\in$ EmpNames    $\wedge$  
                        belongs   $\in$ companies    $\wedge$  
                	works   $\in$   $\wp$ (engagedIn(belongs)) \\
 \> \>       	THEN \\
\>\>\> tEmpId \subst newEmpId;\\
 \> \> \>        (empName(tEmpId),worksOn(tEmpId),belongsTo(tEmpId))
\subst (name,works,belongs) $\mid$$\mid$  \\
 \> \> \>        employees  \subst employees   $\cup$ \{tEmpId\} 
$\mid$$\mid$
hireEmployees   \subst tEmpId \\
 \> \>       	END hireEmployee; \\[0.8ex]
\>     	OTHER newEmpId $\in$ ($\rightarrow$ EmpIds - employees);\\[0.8ex]
END researchCompany.2;\\
\end{tabbing}}

\fig{3}{Abstract Machine with Identification Refinement}

\newpage
{\sl\begin{tabbing}
xx\=xx\=xx\=xx\=xx\= \kill                                               
MACHINE researchCompanies.3\\[0.8ex]
\>   	IMPLY researchCompanies.2\\[0.8ex]
\>  	VARIABLES 
compClass, empClass, projClass, tEmpId\\[0.8ex]
\>     	INVARIANTS compClass   $\in$ (companies   $\rightarrow$   $\wp$ 
                (projects));\\
\>\> empClass   $\in$ (employees   $\rightarrow$ 
     	EmpNames   $\times$ companies   $\times$   $\wp$ (projects));\\
\>\> projClass   $\in$ (projects   $\rightarrow$   $\wp$ (companies));\\
\>\> tEmpId $\in$ EmpIds;  \dots\\[0.8ex]
\> DEFINITIONS engagedIn =   $\lambda$x. (x
    $\in$ companies $\mid$ compClass(x));\\
\>\> (empName, belongsTo, worksOn) 
=   $\lambda$x. (x   $\in$ employees $\mid$ empClass(x));\\
\>\> consortium =   $\lambda$x. (x  
     $\in$ projects $\mid$ projClass(x));\\[0.8ex]
\> 	OPERATIONS 	hireEmployee (name, belongs, works)  =  \\
 \> \>       		PRE 
		      	      	name   $\in$ EmpNames    $\wedge$  
		      		belongs   $\in$ companies    $\wedge$  
				works   $\in$   $\wp$ (engagedIn(belongs)) \\
 \> \>        	THEN 
tEmpId \subst newEmpId;\\
\>\>\> empClass  \subst empClass $\cup$ 
	   		\{(tEmpId, name, belongs, works)\}; \\
\>\>\> hireEmployee   \subst tEmpId \\
 \> \> 			END\\
 \>       	   	END hireEmployee; \\[0.8ex]
\>  OTHER newEmpId  $\in$ ( $\rightarrow$ (EmpIds - employees));\\[0.8ex]
END researchCompany.3;\\
\end{tabbing}}

\fig{4}{Abstract Machine with Data Structure Refinement}

\bigskip

{\sl\begin{tabbing}
xx\=xx\=xx\=xx\=xx\=xx\=xx\= \kill                               
MACHINE researchCompanies.4\\[0.8ex]
\>   	IMPLY researchCompanies.3\\[0.8ex]
\>      CONTEXT 
        ProjIdRecType = ProjNames $\times$ Agencies;
        ProjIdRelType = $\wp$ (ProjIdRecType);\\
\>\>    CompRelType = (CompNames   \parfun ProjIdRelType);\\
\>\>    EmpRelType = (EmpIds  \parfun EmpNames $\times$ 
        CompNames $\times$ ProjIdRelType);\\
\>\>    ProjRelType = (ProjIdRecType \parfun   
        $\wp$ (CompNames));\dots \\[0.8ex]
\>	VARIABLES 
compRel, empRel, projRel \\[0.8ex]
\> 	INVARIANTS
compRel   $\in$ CompRelType; compRel    = compClass ; \\
\>\>     		empRel   $\in$ EmpRelType; empRel   = empClass ;\\
\>\>     		projRel   $\in$ ProjRelType;
projRel =   projClass ;  \dots  \\[0.8ex]
\>  	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));\\[0.8ex]
END researchCompany.4; \\
\end{tabbing}}

\fig{5}{Final Abstract Machine with Type Refinement}



\newpage              

{\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 
		projName : ProjNames; getsGrantFrom : Agencies
		END;\\
\> \> ProjIdRelType = RELATION OF ProjIdRecType; \\[0.8ex]
\>\> CompRelType = RELATION 
               compName OF \\
\>\>\>\>\>\>\> RECORD 
                    compName : CompNames;
                    engagedIn : ProjIdRelType
                   END;   \\
\> \> EmpRelType = RELATION employee OF \\
\>\>\>\>\>\>\> RECORD 
employee : EmpIds; empName : EmpNames;\\
\>\>\>\>\>\>\>\>\> belongsTo : CompNames; worksOn : ProjIdRelType
END;\\
\> \> ProjRelType = RELATION projId OF \\
\>\>\>\>\>\>\> RECORD projId : ProjIdRecType; 
   consortium : RELATION OF CompNames END;\\ [0.8ex]  
END ResearchCompaniesTypes. \\    
\\
DATABASE DEFINITION MODULE ResearchCompaniesOps; \\[0.8ex]   
\> FROM ResearchCompaniesTypes IMPORT EmpNames, CompNames, ProjIdRelType, 
   EmpIds;\\  [0.8ex]  
\> TRANSACTION hireEmployee(empName: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.compName = 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}}

\fig{6}{DBPL implementation of the ResearchCompanies example}
                          
                          


\end{document}



