Abstract for TRCF-97-3:
 Data-Refinement in CSP-OZ, Clemens Fischer and Stefan Hallerstede

Data refinement rules are transformation rules for the development of 
implementations of an abstract data type. In this report we investigate such
rules in the context of CSP-OZ which is a combination of Object-Z and
CSP. Both -- the implementation and the specification -- are written
in CSP-OZ.
We prove the correctness of two data refinement rules --
forward and backwards simulation -- and
show that these rules are complete. Furthermore we present rules for
data refinement when local operations are involved; i.\,e.\
weak refinement rules. 
 
Though some motivations for rules are given, we concentrated on
detailed and complete proofs. Thus this report is not an introduction to CSP-OZ. 
It does not make sense
to read it without detailed knowledge of the definition of CSP-OZ as it is presented
in \cite{fischer97:_csp_oz}, the basic concepts of the CSP
semantics as e.\,g. presented in \cite{roscoe97:_theor_pract_concur} and some knowledge off
data refinement (e.\,g.\ \cite{woodcock96:_using_z}).